Theorems · Definition · category theory

CategoryTheory.PrelaxFunctorStruct.casesOn

{B : Type u₁} →
  [inst : Quiver B] →
    [inst_1 : (a b : B) → Quiver (a ⟶ b)] →
      {C : Type u₂} →
        [inst_2 : Quiver C] →
          [inst_3 : (a b : C) → Quiver (a ⟶ b)] →
            {motive : CategoryTheory.PrelaxFunctorStruct B C → Sort u} →
              (t : CategoryTheory.PrelaxFunctorStruct B C) →
                ((toPrefunctor : B ⥤q C) →
                    (map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (toPrefunctor.map f ⟶ toPrefunctor.map g)) →
                      motive { toPrefunctor := toPrefunctor, map₂ := map₂ }) →
                  motive t

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

QuiverQuiverQuiverQuiver