Theorems · Theorem · category theory

CategoryTheory.FreeBicategory.Hom.brecOn.eq

∀ {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)
  (F_1 :
    (a a_2 : B) →
      (t : CategoryTheory.FreeBicategory.Hom a a_2) → CategoryTheory.FreeBicategory.Hom.below t → motive a a_2 t),
  CategoryTheory.FreeBicategory.Hom.brecOn t F_1 = F_1 a a_1 t (CategoryTheory.FreeBicategory.Hom.brecOn.go t F_1).2

Defined in

Mathlib.CategoryTheory.Bicategory.Free

Cited by

3 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

Quiver