English
Uncurry' is injective: if uncurry' f = uncurry' g then f = g.
Русский
Uncurry' инъективен: если uncurry' f = uncurry' g, то f = g.
LaTeX
$$$ \\forall X [Closed X],\\forall f,g: 𝟙_ C \\to (\\mathrm{ihom} X).obj Y,\\ uncurry' f = uncurry' g \\Rightarrow f = g. $$$
Lean4
/-- Associativity of the enriched structure -/
@[reassoc]
theorem assoc (w x y z : C) [Closed w] [Closed x] [Closed y] :
(α_ _ _ _).inv ≫ comp w x y ▷ _ ≫ comp w y z = _ ◁ comp x y z ≫ comp w x z :=
by
apply uncurry_injective
simp only [uncurry_natural_left, comp_eq]
rw [uncurry_curry, uncurry_curry]; simp only [compTranspose_eq]
rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc]; dsimp
rw [← uncurry_eq, uncurry_curry, associator_inv_naturality_right_assoc, whisker_exchange_assoc, ← uncurry_eq,
uncurry_curry]
simp
