Definition maximal_subgroupoid {C : category} : pregroupoid. Proof. use make_pregroupoid. - use make_category. + use make_precategory; use tpair. * use tpair. -- exact (ob C). -- exact (λ a b, ∑ f : a --> b, is_z_isomorphism f). * unfold precategory_id_comp; cbn. use make_dirprod. -- exact (λ a, identity a,, identity_is_z_iso _). -- intros ? ? ? f g; exact (z_iso_comp f g). * use make_dirprod; intros; apply z_iso_eq. -- apply id_left. -- apply id_right. * use make_dirprod; intros; apply z_iso_eq. -- apply assoc. -- apply assoc'. + cbn. intros a b. cbn. apply isaset_z_iso. - intros ? ? f. exists (z_iso_inv_from_z_iso f). use make_dirprod; apply z_iso_eq. + apply z_iso_inv_after_z_iso. + apply z_iso_after_z_iso_inv. 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.