Definition fundamental_bigroupoid_is_univalent_2_0 : is_univalent_2_0 fundamental_bigroupoid. Proof. intros x y. use isweq_iso. - intros p. apply p. - intros p ; cbn in *. induction p ; cbn. apply idpath. - intros p ; cbn in *. apply path_internal_adjoint_equivalence. + apply fundamental_bigroupoid_is_univalent_2_1. + cbn in *. induction (pr1 p) ; cbn. apply idpath. Defined.
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.Univalence. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique.