Theorems · Definition · category theory

CategoryTheory.CatEnrichedOrdinary.Hom.noConfusionType

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} →
            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'} → CategoryTheory.CatEnrichedOrdinary.Hom f' g' → Sort u_1

Defined in: Mathlib.CategoryTheory.Bicategory.CatEnriched
Cited by: 0 results in Mathlib
Foundations: Depth 49 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Category CategoryTheory.EnrichedOrdinaryCategory

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Catstatement and proof · cited by 884
CategoryTheory.EnrichedOrdinaryCategorystatement and proof · cited by 109
CategoryTheory.CatEnrichedOrdinarystatement and proof · cited by 24
CategoryTheory.CatEnrichedOrdinary.homEquivproof · cited by 18
CategoryTheory.CatEnrichedOrdinary.Homstatement and proof · cited by 3
CategoryTheory.CatEnrichedOrdinary.Hom.casesOnproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

CategoryTheory.CatEnrichedOrdinary.Hom.noConfusionstatement · cited by 0