Definition is_univalent_2_1_if_hom_is_univ {C : bicat} (C_local_univalent : ∏ (X Y : C), is_univalent (hom X Y)) : is_univalent_2_1 C. Proof. intros a b f g. use weqhomot. - exact (invweq (inv2cell_to_z_iso_weq f g) ∘ make_weq idtoiso (C_local_univalent _ _ _ _))%weq. - intro p. induction p. use subtypePath. { intro ; apply isaprop_is_invertible_2cell. } apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.BicategoryLaws.