Theorems · Definition · category theory

CategoryTheory.InducedWideCategory.Hom.casesOn

{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} →
              {motive : X.Hom Y → Sort u} →
                (t : X.Hom Y) →
                  ((hom : F X ⟶ F Y) → (property : P hom) → motive { hom := hom, property := property }) → motive t

Defined in

Mathlib.CategoryTheory.Widesubcategory

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicative