Theorems · Definition · category theory

CategoryTheory.PrelaxFunctorStruct.comp

{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)] →
            {D : Type u₃} →
              [inst_4 : Quiver D] →
                [inst_5 : (a b : D) → Quiver (a ⟶ b)] →
                  CategoryTheory.PrelaxFunctorStruct B C →
                    CategoryTheory.PrelaxFunctorStruct C D → CategoryTheory.PrelaxFunctorStruct B D

Composition of lax prefunctors.

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Cited by

3 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

QuiverQuiverQuiverQuiverQuiverQuiver