Definition gr_precategory_isweq (X Y : ob gr_category) : isweq (λ p : X = Y, idtoiso p). Proof. use (@isweqhomot (X = Y) (z_iso X Y) (pr1weq (weqcomp (gr_univalence X Y) (gr_equiv_weq_iso X Y))) _ _ (weqproperty (weqcomp (gr_univalence X Y) (gr_equiv_weq_iso X Y)))). intros e. induction e. use (pathscomp0 weqcomp_to_funcomp_app). use total2_paths_f. - use idpath. - use proofirrelevance. use isaprop_is_z_isomorphism. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors.