Definition prod_idtoiso_2_1 {a b : C} {f : a --> b} {g : a --> b} (p : f = g) {aa : disp_dirprod_bicat a} {bb : disp_dirprod_bicat b} (ff : aa -->[f] bb) (gg : aa -->[g] bb) (HD1 : disp_univalent_2_1 D1) (HD2 : disp_univalent_2_1 D2) : (transportf (λ z : C ⟦ a, b ⟧, aa -->[ z] bb) p ff = gg) ≃ disp_invertible_2cell (idtoiso_2_1 f g p) ff gg. Proof. refine (pair_disp_invertible_2cell_weq (idtoiso_2_1 _ _ p) ff gg ∘ _)%weq. refine (weqdirprodf (_ ,, HD1 a b f g p (pr1 aa) (pr1 bb) (pr1 ff) (pr1 gg)) (_ ,, HD2 a b f g p (pr2 aa) (pr2 bb) (pr2 ff) (pr2 gg)) ∘ _)%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.