curry_id_eq_coev — Mathlib

English

Let C be a cartesian closed category and A an exponentiable object. For every X in C, the canonical curry of the identity morphism on A ⊗ X coincides with the coevaluation of A evaluated at X; that is, curry(id_{A ⊗ X}) = (exp.coev A).app X.

Русский

Пусть C — картизианно замкнутая категория, A — экспоненцируемый объект. Для любого X из C каноническое карриение тождества на A ⊗ X равно применению коэв A к X: curry(id_{A ⊗ X}) = (exp.coev A).app X.

LaTeX

$$$\operatorname{curry}(\operatorname{id}_{A \otimes X}) = (\mathrm{exp.coev}\,A).\mathrm{app}\,X$$$

Lean4

theorem curry_id_eq_coev (A X : C) [Exponentiable A] : curry (𝟙 _) = (exp.coev A).app X := by
  rw [curry_eq, (exp A).map_id (A ⊗ _)]; apply comp_id

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