Definition hom_v_to_hom_v_sq_z_iso (τ : z_iso (C := hom_v B x y) v₁ v₂) : z_iso (C := hom_v_sq B x y) v₁ v₂. Proof. use make_z_iso ; cbn. - exact (vertical_cell_to_square (pr1 τ)). - exact (vertical_cell_to_square (inv_from_z_iso τ)). - split. + abstract (cbn -[vertical_cell_to_square comp_ver_globular_square] ; rewrite <- vertical_cell_to_square_comp ; refine (_ @ vertical_cell_to_square_id _) ; apply maponpaths ; apply (z_iso_inv_after_z_iso τ)). + abstract (cbn -[vertical_cell_to_square comp_ver_globular_square] ; rewrite <- vertical_cell_to_square_comp ; refine (_ @ vertical_cell_to_square_id _) ; apply maponpaths ; apply (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.