Definition psfunctor_data_is_univalent_2_0 (HD : is_univalent_2 D) : is_univalent_2_0 psfunctor_data_bicat. Proof. pose (HD_2_1 := pr2 HD). apply is_univalent_2_0_total_dirprod. - apply map1cells_is_univalent_2; assumption. - apply map2cells_is_disp_univalent_2; assumption. - apply is_univalent_2_dirprod_bicat. + apply map1cells_is_univalent_2_1; assumption. + apply identitor_is_disp_univalent_2; assumption. + apply compositor_is_disp_univalent_2; assumption. 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.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map2Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Identitor. Require Import UniMath.Bicategories.PseudoFunctors.Display.Compositor. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sigma. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub.