pathComposition_naturality — Mathlib

English

Naturality of pathComposition: the natural transformation forgetful functor commutes with Cat.free.

Русский

Естественность pathComposition: естественный переход совместим с Cat.free.

LaTeX

$$$Cat.freeMap (F.toPrefunctor) \circ pathComposition D = pathComposition C \circ F$$$

Lean4

/-- Naturality of `pathComposition`, which defines a natural transformation
`Quiv.forget ⋙ Cat.free ⟶ 𝟭 _`. -/
theorem pathComposition_naturality {C : Type u} {D : Type u₁} [Category.{v} C] [Category.{v₁} D] (F : C ⥤ D) :
    Cat.freeMap (F.toPrefunctor) ⋙ pathComposition D = pathComposition C ⋙ F :=
  Paths.ext_functor rfl (by simp)

Похожие утверждения