ev_coev — Mathlib

English

In a cartesian closed category, the evaluation and coevaluation satisfy the usual snake identity: (A ▷ (coev A).app B) ≫ (ev A).app (A ⊗ B) = id_{A ⊗ B}.

Русский

В категории замкнутой по декартову произведению тождественный хвостовой треугольник: (A ▷ coev_A.app B) ≫ (ev_A).app (A ⊗ B) = id_{A ⊗ B}.

LaTeX

$$$ (A \triangleleft (\mathrm{coev}\, A)_{\mathrm{app}\, B}) \gg (\mathrm{ev}\, A)_{\mathrm{app}\,(A \otimes B)} = \mathrm{Id}_{A \otimes B}$$$

Lean4

@[reassoc]
theorem ev_coev : (A ◁ (coev A).app B) ≫ (ev A).app (A ⊗ B) = 𝟙 (A ⊗ B : C) :=
  ihom.ev_coev A B

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