English
Any equivalence between types in the same universe yields a categorical isomorphism between those types. Specifically, given e: X ≃ Y, one obtains an isomorphism X ≅ Y with hom = e and inv = e^{-1}.
Русский
Любое эквивалентность между типами X и Y в той же вселенной порождает категориальный изоморфизм X ≅ Y, причем гомоморфизмом является сама эквивалентность e, а об inversе — обратная.
LaTeX
$$$$ \text{toIso}(e) : X \cong Y \quad\text{with } \mathrm{hom} = e, \; \mathrm{inv} = e^{-1}, \; \mathrm{hom\_inv\_id} = \mathrm{funext}(e.left\_inv), \; \mathrm{inv\_hom\_id} = \mathrm{funext}(e.right\_inv). $$$$
Lean4
/-- Any equivalence between types in the same universe gives
a categorical isomorphism between those types.
-/
def toIso (e : X ≃ Y) : X ≅ Y where
hom := e.toFun
inv := e.invFun
hom_inv_id := funext e.left_inv
inv_hom_id := funext e.right_inv
