coev_app_π — Mathlib

English

Coevaluation and π-structure interact to express curry in the Closed structure

Русский

Сопоставление ко-оценки и π-структура выражает карри-структуру в замкнутой структуре.

LaTeX

$$$\\mathcal{H}.coev_{app} \\circ \\pi = \\mathrm{MonoidalClosed. curry}(\\mathcal{H}.\\pi)$$$

Lean4

@[reassoc (attr := simp)]
theorem coev_app_π (c j : C) :
    ℌ.coev_app.app c ≫ ℌ.π c j = MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) :=
  by
  dsimp [coev_app]
  rw [← Wedge.mk_ι (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c) (H.obj c) (ℌ.π c) (ℌ.hπ c),
    Wedge.IsLimit.lift_ι]

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