Definition horizontal_square_weq_invertible_2cell (HB : horizontally_saturated B) {x y : B} (h₁ h₂ : x --> y) : invertible_horizontal_square h₁ h₂ ≃ invertible_2cell h₁ h₂. Proof. use weq_iso. - exact (horizontal_square_to_invertible_2cell HB). - exact invertible_2cell_to_horizontal_square. - abstract (intro s ; use subtypePath ; [ intro ; apply isaprop_invertible_horizontal_square_laws | ] ; use dirprodeq ; apply square_to_horizontal_cell_to_square). - abstract (intro τ ; use subtypePath ; [ intro ; apply isaprop_is_invertible_2cell | ] ; apply horizontal_cell_to_square_to_horizontal_cell). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws.