English
In a square of functors where the top and bottom are equivalences, there is an equivalence between the 2-commutative structures given by taking hInv on the left-right swapped square and hInv on the original square. This yields a correspondence between 2-commutative squares under the transformation of taking inverses.
Русский
В квадрате из эквивалентностей, где верхний и нижний квадраты являются эквивалентностями, существует эквивалентность двухобразной 2-коэрентности между квадратами и их обратными сторонами. Получается соответствие между 2‑коммутативными квадратами при переходе к обратным странам.
LaTeX
$$$ hInvEquiv : CatCommSq T.functor L R B.functor ≃ CatCommSq T.inverse R L B.inverse $$$
Lean4
theorem hInv_hInv (h : CatCommSq T.functor L R B.functor) : hInv T.symm R L B.symm (hInv T L R B h) = h :=
by
ext X
rw [← cancel_mono (B.functor.map (L.map (T.unitIso.hom.app X)))]
rw [← Functor.comp_map]
erw [← h.iso.hom.naturality (T.unitIso.hom.app X)]
rw [hInv_iso_hom_app]
simp only [Equivalence.symm_functor]
rw [hInv_iso_inv_app]
dsimp
simp only [Functor.comp_obj, assoc, ← Functor.map_comp, Iso.inv_hom_id_app, Equivalence.counitInv_app_functor,
Functor.map_id]
simp only [Functor.map_comp, Equivalence.fun_inv_map, assoc, Equivalence.counitInv_functor_comp, comp_id,
Iso.inv_hom_id_app_assoc]
