coev_ev — Mathlib

English

In a cartesian closed category, the coevaluation followed by the mapped evaluation is the identity: (coev A).app (A ⟹ B) ≫ (exp A).map ((ev A).app B) = id_{A ⟹ B}.

Русский

В замкнутой по декартову произведению категории сочетание кооценника и отображения (ev A) даёт тождество: (coev A).app (A ⟹ B) ≫ (exp A).map ((ev A).app B) = id.

LaTeX

$$$(\mathrm{coev}\, A)_{\mathrm{app}\,(A \Rightarrow B)} \; \circ \; (\exp A).map((\mathrm{ev}\, A)_{\mathrm{app} B}) = \mathrm{Id}_{A \Rightarrow B}$$$

Lean4

@[reassoc]
theorem coev_ev : (coev A).app (A ⟹ B) ≫ (exp A).map ((ev A).app B) = 𝟙 (A ⟹ B) :=
  ihom.coev_ev A B

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