Definition disp_univalent_2_0_along_iso (HD₂' : disp_univalent_2_0 D₂) : disp_univalent_2_0 D₁. Proof. use fiberwise_univalent_2_0_to_disp_univalent_2_0. intros x xx yy. use weqhomot. - exact (disp_adjequiv_along_iso_weq xx yy ∘ make_weq _ (HD₂' _ _ (idpath _) _ _) ∘ make_weq _ (isweqonpathsincl _ (isinclweq _ _ _ (pr2 (disp_psfunctor_iso_ob_weq HF x))) xx yy))%weq. - abstract (intro p ; cbn in p ; induction p ; use subtypePath ; [ intro ; exact (isaprop_disp_left_adjoint_equivalence _ _ HB₁ disp_univalent_2_1_along_iso) | ] ; cbn -[disp_psfunctor_iso_id_mor_weq disp_psfunctor_invmap_1] ; exact (disp_psfunctor_invmap_1_id_eq HF HB₂ HD₂ xx)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.Initial. Require Import UniMath.Bicategories.Core.Examples.Final. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.TransportLaws. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor. Require Import UniMath.Bicategories.DisplayedBicats.DispTransportLaws.