proposition: Lemma univalent_groupoid_arrow_weq_path {ugpd : univalent_groupoid} {a b : ob ugpd} : (a --> b) ≃ a = b.
proof: Proof. intermediate_weq (z_iso a b). - apply (@pregroupoid_hom_weq_iso ugpd). - apply invweq; use make_weq. + exact idtoiso. + apply univalent_category_is_univalent. 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