Theorems · Definition · category theory

CategoryTheory.MorphismProperty.FunctorialFactorizationData.recOn

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      {motive : W₁.FunctorialFactorizationData W₂ → Sort u} →
        (t : W₁.FunctorialFactorizationData W₂) →
          ((Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C) →
              (i : CategoryTheory.Arrow.leftFunc ⟶ Z) →
                (p : Z ⟶ CategoryTheory.Arrow.rightFunc) →
                  (fac : CategoryTheory.CategoryStruct.comp i p = CategoryTheory.Arrow.leftToRight) →
                    (hi : ∀ (f : CategoryTheory.Arrow C), W₁ (i.app f)) →
                      (hp : ∀ (f : CategoryTheory.Arrow C), W₂ (p.app f)) →
                        motive { Z := Z, i := i, p := p, fac := fac, hi := hi, hp := hp }) →
            motive t

Defined in

Mathlib.CategoryTheory.MorphismProperty.Factorization

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category