uncurry_obj_curry_obj — Mathlib

English

The uncurrying of the curry of F recovers F: uncurry.obj (curry.obj F) = F.

Русский

Раскурривание каррирования F восстанавливает F: uncurry.obj (curry.obj F) = F.

LaTeX

$$$\operatorname{uncurry.obj}(\operatorname{curry.obj} F) = F$$$

Lean4

theorem uncurry_obj_curry_obj (F : B × C ⥤ D) : uncurry.obj (curry.obj F) = F :=
  Functor.ext (by simp)
    (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
      dsimp
      simp only [← F.map_comp, Category.id_comp, Category.comp_id, prod_comp])

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