English
The left unit law for the enriched structure asserts that a certain composite involving the left unitor and the curry/Pre maps equals the identity on the hom-object.
Русский
Левый единичный закон для обогащённой структуры утверждает, что некоторый композиционный оператор, включающий левый юнитор и сопряжения curry/Pre, равен тождественному преобразованию на соответствующем объекте Hom.
LaTeX
$$$ (\\lambda\\_ ((ihom x).obj y)).inv \\circ id\\,x \\triangleright _ \\circ comp\\,x\\,x\\,y = 𝟙 _. $$$
Lean4
/-- Left unitality of the enriched structure -/
@[reassoc (attr := simp)]
theorem id_comp (x y : C) [Closed x] : (λ_ ((ihom x).obj y)).inv ≫ id x ▷ _ ≫ comp x x y = 𝟙 _ :=
by
apply uncurry_injective
rw [uncurry_natural_left, uncurry_natural_left, comp_eq, uncurry_curry, id_eq, compTranspose_eq,
associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ← uncurry_eq, uncurry_curry,
triangle_assoc_comp_right_assoc, whiskerLeft_inv_hom_assoc, uncurry_id_eq_ev _ _]
