curryObjCompIso — Mathlib

English

Equality between two expressions involving uncurry, curry and flip with prod and G

Русский

Равенство между двумя выражениями, содержащими раскурривание, каррирование и flip с Prod и G

LaTeX

$$$\operatorname{uncurry.obj}(\text{F1. ...}) = \text{(F1.prod F2)} \cdot G$$$

Lean4

/-- Natural isomorphism witnessing `comp_flip_curry_eq`. -/
@[simps!]
def curryObjCompIso (F : C × B ⥤ D) (G : D ⥤ E) :
    (curry.obj (F ⋙ G)).flip ≅ (curry.obj F).flip ⋙ (whiskeringRight _ _ _).obj G :=
  .refl _

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