counitBackward_counitForward — Mathlib

English

The backward and forward counits compose to the identity: counitBackward F s ∘ counitForward F s = id.

Русский

Обратные и прямые калибровки композиционно дают тождественный морфизм: counitBackward F s ∘ counitForward F s = id.

LaTeX

$$$$ counitBackward\ F\ s \circ counitForward\ F\ s = \mathrm{id} $$$$

Lean4

theorem counitBackward_counitForward (F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) (s : CostructuredArrow yoneda A) :
    counitBackward F s ∘ counitForward F s = id :=
  funext fun x => by simp [counitBackward]

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