Lemma total_is_univalent_2 {C : bicat} {D: disp_bicat C} : disp_univalent_2 D → is_univalent_2 C → is_univalent_2 (total_bicat D). Proof. intros UD UC. split. - apply total_is_univalent_2_0. { apply UC. } apply disp_univalent_2_0_of_2. assumption. - apply total_is_univalent_2_1. { apply UC. } apply disp_univalent_2_1_of_2. assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.