Theorems · Definition · category theory

CategoryTheory.FreeBicategory.Hom.casesOn

{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 b : B} → (f : a ⟶ b) → motive a b (CategoryTheory.FreeBicategory.Hom.of f)) →
            ((a : B) → motive a a (CategoryTheory.FreeBicategory.Hom.id a)) →
              ({a b c : B} →
                  (f : CategoryTheory.FreeBicategory.Hom a b) →
                    (g : CategoryTheory.FreeBicategory.Hom b c) → motive a c (f.comp g)) →
                motive a a_1 t

Defined in

Mathlib.CategoryTheory.Bicategory.Free

Cited by

1 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

Quiver