Definition weq_disp_left_adjequiv_hor_id_inv_iso (x : pr11 CD) : is_iso_twosided_disp (identity_is_z_iso x) (identity_is_z_iso x) ((pr11 τ) x). Proof. simple refine (_ ,, _). - exact (pr1 (pr112 τ) x). - split. + abstract (cbn ; pose (p := pr2 (pr212 τ) x) ; cbn in p ; rewrite id_two_disp_right in p ; rewrite double_id_mor_id in p ; rewrite id_two_disp_left in p ; unfold transportb_disp_mor2 in p ; rewrite !transport_f_f_disp_mor2 in p ; refine (!(transportbf_disp_mor2 _ _ _) @ maponpaths _ p @ _) ; unfold transportb_disp_mor2 ; rewrite transport_f_f_disp_mor2 ; use transportf_disp_mor2_eq ; apply idpath). + abstract (pose (p := pr1 (pr212 τ) x) ; cbn in p ; rewrite id_two_disp_left in p ; rewrite double_id_mor_id in p ; rewrite id_two_disp_left in p ; unfold transportb_disp_mor2 in p ; rewrite !transport_f_f_disp_mor2 in p ; refine (!(transportbf_disp_mor2 _ _ _) @ maponpaths _ (!p) @ _) ; unfold transportb_disp_mor2 ; rewrite transport_f_f_disp_mor2 ; use transportf_disp_mor2_eq ; apply idpath). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOfDispCats. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOfTwoSidedDispCat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleFunctor. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleTransformation. Section FromAdjEquivHorId. End FromAdjEquivHorId. Section FromAdjEquivHorComp. End FromAdjEquivHorComp.