Proposition iso_two_cat_arrow_to_z_iso_inverses : is_inverse_in_precat (C := hom_cat x y) θ θi. Proof. split. - unfold θ, θi ; cbn. unfold two_cat_rinvunitor, two_cat_lunitor. pose (inv_after_iso_twosided_disp τ) as p. cbn in p. rewrite transportb_disp_mor2_two_cat_arrow in p. unfold two_cat_runitor, two_cat_linvunitor in p. rewrite idto2mor_lwhisker in p. rewrite idto2mor_rwhisker in p. rewrite !idto2mor_comp in p. assert (f = f · (identity y · identity y)) as q₁. { rewrite !id_right. apply idpath. } assert (identity x · identity x · f = f) as q₂. { rewrite !id_left. apply idpath. } simple refine (_ @ maponpaths (λ z, idto2mor q₁ • z • idto2mor q₂) p @ _) ; clear p. + unfold two_cat_lassociator, two_cat_rassociator. etrans. { rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite idto2mor_comp. apply idpath. } refine (!_). rewrite !vassocr. rewrite idto2mor_comp. rewrite !vassocl. rewrite idto2mor_comp. etrans. { etrans. { apply maponpaths. apply maponpaths_2. apply rwhisker_id1. } unfold two_cat_runitor, two_cat_rinvunitor. rewrite !vassocr. rewrite idto2mor_comp. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite idto2mor_comp. rewrite !vassocl. etrans. { apply maponpaths. apply maponpaths_2. apply id1_lwhisker. } unfold two_cat_lunitor, two_cat_linvunitor. rewrite !vassocr. rewrite idto2mor_comp. rewrite !vassocl. rewrite idto2mor_comp. apply idpath. } rewrite !vassocr. use arr_idto2mor_eq2 ; apply idpath. + rewrite !idto2mor_comp. rewrite idto2mor_id. apply idpath. - unfold θ, θi ; cbn. unfold two_cat_rinvunitor, two_cat_lunitor. pose (iso_after_inv_twosided_disp τ) as p. cbn in p. rewrite transportb_disp_mor2_two_cat_arrow in p. unfold two_cat_runitor, two_cat_linvunitor in p. rewrite idto2mor_lwhisker in p. rewrite idto2mor_rwhisker in p. rewrite !idto2mor_comp in p. assert (g = g · (identity y · identity y)) as q₁. { rewrite !id_right. apply idpath. } assert (identity x · identity x · g = g) as q₂. { rewrite !id_left. apply idpath. } simple refine (_ @ maponpaths (λ z, idto2mor q₁ • z • idto2mor q₂) p @ _) ; clear p. + unfold two_cat_lassociator, two_cat_rassociator. etrans. { rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite idto2mor_comp. apply idpath. } refine (!_). rewrite !vassocr. rewrite idto2mor_comp. rewrite !vassocl. rewrite idto2mor_comp. etrans. { etrans. { apply maponpaths. apply maponpaths_2. apply rwhisker_id1. } unfold two_cat_runitor, two_cat_rinvunitor. rewrite !vassocr. rewrite idto2mor_comp. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite idto2mor_comp. rewrite !vassocl. etrans. { apply maponpaths. apply maponpaths_2. apply id1_lwhisker. } unfold two_cat_lunitor, two_cat_linvunitor. rewrite !vassocr. rewrite idto2mor_comp. rewrite !vassocl. rewrite idto2mor_comp. apply idpath. } rewrite !vassocr. use arr_idto2mor_eq2 ; apply idpath. + rewrite !idto2mor_comp. rewrite idto2mor_id. apply idpath. 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.