pathsOf_pathComposition_toPrefunctor

English

For any category C, the path construction composed with path composition yields the identity on C (in the unbundled sense): Paths.of C ⋙q (pathComposition C).toPrefunctor = 𝟭q C.

Русский

Для любой категории C построение путей, затем композиция путей, даёт тождество на C (в развернутом виде): Paths.of C ⋙q (pathComposition C).toPrefunctor = 𝟭q C.

LaTeX

$$$Paths.of C \;⋙q\; (pathComposition C).toPrefunctor = 𝟭q C$$$

Lean4

/-- An unbundled version of the right triangle equality. -/
theorem pathsOf_pathComposition_toPrefunctor (C : Type u) [Category.{v} C] :
    Paths.of C ⋙q (pathComposition C).toPrefunctor = 𝟭q C :=
  by
  dsimp only [Prefunctor.comp]
  congr
  funext X Y f
  exact Category.id_comp _

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