Proposition z_iso_to_iso_two_cat_arrow_right : θi ;;2 θ = transportb_disp_mor2 (id_left _) (id_left _) (id_two_disp g). Proof. unfold θ, θi. rewrite transportb_disp_mor2_two_cat_arrow ; cbn. unfold two_cat_lassociator, two_cat_rassociator, two_cat_runitor, two_cat_linvunitor. rewrite <- !rwhisker_vcomp. rewrite <- !lwhisker_vcomp. rewrite !idto2mor_lwhisker. rewrite !idto2mor_rwhisker. rewrite !vassocl. rewrite !idto2mor_comp. rewrite !vassocr. rewrite !idto2mor_comp. etrans. { etrans. { apply maponpaths_2. apply maponpaths. apply id1_lwhisker. } unfold two_cat_linvunitor, two_cat_lunitor. rewrite !vassocl. rewrite !idto2mor_comp. rewrite !vassocr. do 2 apply maponpaths_2. rewrite !vassocl. rewrite !idto2mor_comp. etrans. { apply maponpaths. apply maponpaths_2. apply rwhisker_id1. } unfold two_cat_runitor, two_cat_rinvunitor. rewrite !vassocl. rewrite idto2mor_comp. rewrite !vassocr. rewrite idto2mor_comp. apply idpath. } rewrite idto2mor_id. rewrite id2_right. rewrite !vassocl. etrans. { apply maponpaths. rewrite !vassocr. etrans. { apply maponpaths_2. apply (z_iso_after_z_iso_inv τ). } apply id2_left. } rewrite idto2mor_comp. apply maponpaths. apply (homset_property C). 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.