Definition hom_h_sq_to_hom_h_z_iso (τ : z_iso (C := hom_h_sq B x y) h₁ h₂) : z_iso (C := hom_h B x y) h₁ h₂. Proof. use make_z_iso ; cbn. - exact (square_to_horizontal_cell H (pr1 τ)). - exact (square_to_horizontal_cell H (inv_from_z_iso τ)). - split. + abstract (cbn ; refine (!(square_to_horizontal_cell_comp _ _ _) @ _) ; refine (_ @ square_to_horizontal_cell_id H _) ; apply maponpaths ; exact (z_iso_inv_after_z_iso τ)). + abstract (cbn ; refine (!(square_to_horizontal_cell_comp _ _ _) @ _) ; refine (_ @ square_to_horizontal_cell_id H _) ; apply maponpaths ; exact (z_iso_after_z_iso_inv τ)). 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.Univalence. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.UnderlyingCats. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.CellsAndSquares.