curry_obj_uncurry_obj — Mathlib

English

The curry and uncurry operations are inverse equivalences between bifunctors and their curried form: curry_obj_uncurry_obj F = F and uncurry_obj_curry_obj F = F.

Русский

Операции каррирования и раскуррирования образуют взаимно обратные эквивалентности между бифунктором и его каррированной формой.

LaTeX

$$$\operatorname{curry.obj}^{-1} = \operatorname{uncurry.obj}$ and $\operatorname{uncurry.obj}^{-1} = \operatorname{curry.obj}$$$

Lean4

theorem curry_obj_uncurry_obj (F : B ⥤ C ⥤ D) : curry.obj (uncurry.obj F) = F :=
  Functor.ext (fun _ => Functor.ext (by simp) (by simp)) (by cat_disch)

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