Definition prod_idtoiso_2_0 (HC : is_univalent_2_1 C) (HD1 : disp_univalent_2 D1) (HD2 : disp_univalent_2 D2) {a b : C} (p : a = b) (aa : disp_dirprod_bicat a) (bb : disp_dirprod_bicat b) : (transportf (λ z : C, disp_dirprod_bicat z) p aa = bb) ≃ disp_adjoint_equivalence (idtoiso_2_0 a b p) aa bb. Proof. refine (pair_adjoint_equivalence_weq HC (pr2 HD1) (pr2 HD2) (idtoiso_2_0 _ _ p) aa bb ∘ _)%weq. refine (weqdirprodf (_ ,, pr1 HD1 a b p (pr1 aa) (pr1 bb)) (_ ,, pr1 HD2 a b p (pr2 aa) (pr2 bb)) ∘ _)%weq. induction p ; cbn. apply WeakEquivalences.pathsdirprodweq. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. 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.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.