proposition: Lemma pregroupoid_hom_weq_iso {pgpd : pregroupoid} (a b : pgpd) : (a --> b) ≃ z_iso a b.
proof: Proof. use weq_iso. - intros f; refine (f,, _); apply pregroupoid_is_pregroupoid. - apply pr1. - reflexivity. - intro; apply z_iso_eq; reflexivity. Defined.
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