Theorems · Definition · category theory

CategoryTheory.MorphismProperty.CodescendsAlong.casesOn

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P Q : CategoryTheory.MorphismProperty C} →
      {motive : P.CodescendsAlong Q → Sort u} →
        (t : P.CodescendsAlong Q) →
          ((of_isPushout :
                ∀ {Z X Y A : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ A} {inr : Y ⟶ A},
                  CategoryTheory.IsPushout f g inl inr → Q f → P inl → P g) →
              motive ⋯) →
            motive t

Defined in

Mathlib.CategoryTheory.MorphismProperty.Descent

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CategoryTheory.Category