Theorems · Definition · category theory

CategoryTheory.CatEnrichedOrdinary.Hom.noConfusion

{P : Sort u_1} →
  {C : Type u} →
    {inst : CategoryTheory.Category.{v, u} C} →
      {inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C} →
        {X Y : CategoryTheory.CatEnrichedOrdinary C} →
          {f g : X ⟶ Y} →
            {t : CategoryTheory.CatEnrichedOrdinary.Hom f g} →
              {C' : Type u} →
                {inst' : CategoryTheory.Category.{v, u} C'} →
                  {inst'_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C'} →
                    {X' Y' : CategoryTheory.CatEnrichedOrdinary C'} →
                      {f' g' : X' ⟶ Y'} →
                        {t' : CategoryTheory.CatEnrichedOrdinary.Hom f' g'} →
                          C = C' →
                            inst ≍ inst' →
                              inst_1 ≍ inst'_1 →
                                X ≍ X' →
                                  Y ≍ Y' →
                                    f ≍ f' →
                                      g ≍ g' → t ≍ t' → CategoryTheory.CatEnrichedOrdinary.Hom.noConfusionType P t t'

Defined in

Mathlib.CategoryTheory.Bicategory.CatEnriched

Cited by

0 results in Mathlib

Foundations

Depth 50 from the axioms · uses propext, Classical.choice, Quot.sound