English
The vInvEquiv construction provides an equivalence between CatCommSq structures when replacing a square by its inverse square via left-right inverses, i.e., a correspondence between squares and their vInv images.
Русский
Конструкция vInvEquiv даёт эквивалентность структур CatCommSq при замене квадрата на его обратный через левое–правое обращение, то есть корреспонденция между квадратами и их изображениями по vInv.
LaTeX
$$def vInvEquiv : CatCommSq T L.functor R.functor B ≃ CatCommSq B L.inverse R.inverse T$$
Lean4
/-- In a square of categories, when the left and right 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 vInvEquiv : CatCommSq T L.functor R.functor B ≃ CatCommSq B L.inverse R.inverse T
where
toFun := vInv T L R B
invFun := vInv B L.symm R.symm T
left_inv := vInv_vInv T L R B
right_inv := vInv_vInv B L.symm R.symm T
