proposition: Lemma univalent_bicategory_0_cell_hlevel_4 (C : bicat) (HC : is_univalent_2 C) : isofhlevel 4 C.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.TransportLaws UniMath.Bicategories.Core.EquivToAdjequiv