Lemma univalent_bicategory_0_cell_hlevel_4 (C : bicat) (HC : is_univalent_2 C) : isofhlevel 4 C. Proof. change (isofhlevel 4 C) with (∏ a b : C, isofhlevel 3 (a = b)). intros a b. apply (isofhlevelweqb _ (idtoiso_2_0 a b,, pr1 HC a b)). apply (isofhleveltotal2 3). - apply univalent_bicategory_1_cell_hlevel_3, HC. - intros f. do 2 apply hlevelntosn. apply isaprop_left_adjoint_equivalence, HC. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. 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.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.TransportLaws. Require Import UniMath.Bicategories.Core.EquivToAdjequiv.