proposition: Lemma is_univalent_pregroupoid_is_univalent {pgpd : groupoid} : is_univalent_pregroupoid pgpd -> is_univalent pgpd.
proof: Proof. intros ig. intros a b. use (isofhlevelff 0 idtoiso (morphism_from_z_iso _ _)). + use (isweqhomot (idtomor _ _)). * intro p; destruct p; reflexivity. * apply ig. + apply (morphism_from_iso_is_incl pgpd). Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.opp_precat