counitForward_counitBackward — Mathlib

English

The counit forward and counit backward assemble into the identity: counitForward F s ∘ counitBackward F s = id.

Русский

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

LaTeX

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

Lean4

theorem counitForward_counitBackward (F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) (s : CostructuredArrow yoneda A) :
    counitForward F s ∘ counitBackward F s = id :=
  funext fun p => OverArrows.ext <| YonedaCollection.ext (by simp) (by simp [counitBackward])

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