Proposition iso_twosided_disp_two_cat_arrow_weq_left {x y : C} (f g : two_cat_arrow_twosided_disp_cat x y) (τ : z_iso (C := hom_cat x y) f g) : iso_two_cat_arrow_to_z_iso (z_iso_to_iso_two_cat_arrow τ) = τ. Proof. use z_iso_eq. cbn. rewrite !vassocr. etrans. { do 3 apply maponpaths_2. apply two_cat_rinvunitor_runitor. } rewrite id2_left. rewrite !vassocl. etrans. { apply maponpaths. apply two_cat_linvunitor_lunitor. } apply id2_right. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.TwoCategories. Import TwoCategories.Notations. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete.