English
The hInvEquiv construction provides an equivalence between squares built from an equivalence T: C1 ≌ C2 and a square built from the inverse equivalence T^{-1}: C2 ≌ C1, together with the corresponding left/right components inverted and swapped.
Русский
Конструкция hInvEquiv задаёт эквивалентность между квадратами, построенными из эквивалентности T: C1 ≌ C2 и квадрата, построенного из обратной эквивалентности T^{-1}: C2 ≌ C1, вместе с соответствующими инвертированными компонентами слева и справа и переставленными сторонами.
LaTeX
$$$ hInvEquiv : CatCommSq T.functor L.functor R.functor B.functor ≃ CatCommSq T.inverse R L B.inverse $$$
Lean4
/-- In a square of categories, when the top and bottom functors are part
of equivalence of categories, it is equivalent to show 2-commutativity for
the functors of these equivalences or for their inverses. -/
def hInvEquiv : CatCommSq T.functor L R B.functor ≃ CatCommSq T.inverse R L B.inverse
where
toFun := hInv T L R B
invFun := hInv T.symm R L B.symm
left_inv := hInv_hInv T L R B
right_inv := hInv_hInv T.symm R L B.symm
