Theorems · Definition · category theory

CategoryTheory.FreeBicategory.Hom.brecOn

{B : Type u} →
  [inst : Quiver B] →
    {motive : (a a_1 : B) → CategoryTheory.FreeBicategory.Hom a a_1 → Sort u_1} →
      {a a_1 : B} →
        (t : CategoryTheory.FreeBicategory.Hom a a_1) →
          ((a a_2 : B) →
              (t : CategoryTheory.FreeBicategory.Hom a a_2) →
                CategoryTheory.FreeBicategory.Hom.below t → motive a a_2 t) →
            motive a a_1 t

Defined in: Mathlib.CategoryTheory.Bicategory.Free
Cited by: 1 results in Mathlib
Foundations: Depth 6 from the axioms · uses no axioms
Assumes: Quiver

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites4

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

Quiverstatement and proof · cited by 405
CategoryTheory.FreeBicategory.Homstatement and proof · cited by 20
CategoryTheory.FreeBicategory.Hom.belowstatement and proof · cited by 4
CategoryTheory.FreeBicategory.Hom.brecOn.goproof · cited by 4

Cited by4

Results whose statement or proof uses this declaration.

CategoryTheory.FreeBicategory.normalizeAuxproof · cited by 9
CategoryTheory.FreeBicategory.liftHomproof · cited by 8
CategoryTheory.FreeBicategory.normalizeIsoproof · cited by 4
CategoryTheory.FreeBicategory.Hom.brecOn.eqstatement and proof · cited by 3