Theorems · Definition · category theory

CategoryTheory.InducedWideCategory.Hom.noConfusion

{P : Sort u} →
  {C : Type u₁} →
    {D : Type u₂} →
      {inst : CategoryTheory.Category.{v₁, u₂} D} →
        {F : C → D} →
          {P_1 : CategoryTheory.MorphismProperty D} →
            {inst_1 : P_1.IsMultiplicative} →
              {X Y : CategoryTheory.InducedWideCategory D F P_1} →
                {t : X.Hom Y} →
                  {C' : Type u₁} →
                    {D' : Type u₂} →
                      {inst' : CategoryTheory.Category.{v₁, u₂} D'} →
                        {F' : C' → D'} →
                          {P' : CategoryTheory.MorphismProperty D'} →
                            {inst'_1 : P'.IsMultiplicative} →
                              {X' Y' : CategoryTheory.InducedWideCategory D' F' P'} →
                                {t' : X'.Hom Y'} →
                                  C = C' →
                                    D = D' →
                                      inst ≍ inst' →
                                        F ≍ F' →
                                          P_1 ≍ P' →
                                            inst_1 ≍ inst'_1 →
                                              X ≍ X' →
                                                Y ≍ Y' →
                                                  t ≍ t' → CategoryTheory.InducedWideCategory.Hom.noConfusionType P t t'

Defined in

Mathlib.CategoryTheory.Widesubcategory

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms