Lemma univalent_groupoid_arrow_weq_path {ugpd : univalent_groupoid} {a b : ob ugpd} : (a --> b) ≃ a = b. 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.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.opp_precat.