Theorems · Definition · category theory

CategoryTheory.Cat.freeMapCompIso

{V₁ : Type u₁} →
  {V₂ : Type u₂} →
    {V₃ : Type u₃} →
      [inst : Quiver V₁] →
        [inst_1 : Quiver V₂] →
          [inst_2 : Quiver V₃] →
            (F : V₁ ⥤q V₂) →
              (G : V₂ ⥤q V₃) →
                CategoryTheory.Cat.freeMap (F ⋙q G) ≅ (CategoryTheory.Cat.freeMap F).comp (CategoryTheory.Cat.freeMap G)

The functor free : Quiv ⥤ Cat preserves composition up to natural isomorphism and in fact up to equality.

Defined in

Mathlib.CategoryTheory.Category.Quiv

Cited by

3 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

QuiverQuiverQuiver