Theorems · Definition · category theory

CategoryTheory.InducedWideCategory.Hom.mk.noConfusion

{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} →
              {P_1 : Sort u} →
                {hom : F X ⟶ F Y} →
                  {property : P hom} →
                    {hom' : F X ⟶ F Y} →
                      {property' : P hom'} →
                        { hom := hom, property := property } = { hom := hom', property := property' } →
                          (hom ≍ hom' → P_1) → P_1

Defined in

Mathlib.CategoryTheory.Widesubcategory

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms