# Groupoids

Author: Langston Barrett (@siddharthist), March 2018

## Contents

• Definitions
• Pregroupoid
• Groupoid
• Univalent groupoid
• An alternative characterization of univalence for groupoids
• Lemmas
• Subgroupoids
• Discrete categories

## Definitions

A precategory is a pregroupoid when all of its arrows are isos.
Definition is_pregroupoid (C : precategory) :=
(x y : C) (f : x --> y), is_iso f.

Lemma isaprop_is_pregroupoid (C : precategory) : isaprop (is_pregroupoid C).
Proof.
do 3 (apply impred; intro).
apply isaprop_is_iso.
Defined.

Definition pregroupoid : UU := C : precategory, is_pregroupoid C.

Constructors, accessors, and coersions
A category is a groupoid when all of its arrows are isos.
Definition groupoid : UU := C : category, is_pregroupoid C.

Constructors, accessors, and coersions
Constructors, accessors, and coersions
An alternative characterization of univalence for groupoids
Definition is_univalent_pregroupoid (pgpd : pregroupoid) :=
( a b : ob pgpd, isweq (fun path : a = bidtomor a b path)) ×
has_homsets pgpd.

The morphism part of an isomorphism is an inclusion.
Lemma morphism_from_iso_is_incl (C : category) (a b : ob C) :
isincl (@morphism_from_iso C a b).
Proof.
intro g.
apply (isofhlevelweqf _ (ezweqpr1 _ _)).
apply isaprop_is_iso.
Qed.

The alternative characterization implies the normal one. Note that the other implication is missing, it should be completed if possible.
Lemma is_univalent_pregroupoid_is_univalent {pgpd : pregroupoid} :
is_univalent_pregroupoid pgpd is_univalent pgpd.
Proof.
intros ig.
split.
- intros a b.
use (isofhlevelff 0 idtoiso morphism_from_iso).
+ use (isweqhomot (idtomor _ _)).
× intro p; destruct p; reflexivity.
× apply ig.
+ apply (morphism_from_iso_is_incl (pr1 pgpd,, pr2 ig)).
- exact (pr2 ig).
Qed.

## Lemmas

In a pregroupoid, the hom-types are equivalent to the type of isomorphisms.
Lemma pregroupoid_hom_weq_iso {pgpd : pregroupoid} (a b : pgpd) : (a --> b) iso a b.
Proof.
use weq_iso.
- intros f; refine (f,, _); apply pregroupoid_is_pregroupoid.
- apply pr1.
- reflexivity.
- intro; apply eq_iso; reflexivity.
Defined.

Lemma pregroupoid_hom_weq_iso_idtoiso {pgpd : pregroupoid} (a : pgpd) :
pregroupoid_hom_weq_iso a a (identity a) = idtoiso (idpath a).
Proof.
apply eq_iso; reflexivity.
Defined.

Lemma pregroupoid_hom_weq_iso_comp {pgpd : pregroupoid} {a b c : ob pgpd}
(f : a --> b) (g : b --> c) :
iso_comp (pregroupoid_hom_weq_iso _ _ f) (pregroupoid_hom_weq_iso _ _ g) =
(pregroupoid_hom_weq_iso _ _ (f · g)).
Proof.
apply eq_iso; reflexivity.
Defined.

If D is a groupoid, then a functor category into it is as well.
Lemma is_pregroupoid_functor_cat {C : precategory} {D : category}
(gr_D : is_pregroupoid D)
: is_pregroupoid (functor_category C D).
Proof.
intros F G α; apply functor_iso_if_pointwise_iso.
intros c; apply gr_D.
Defined.

In a univalent groupoid, arrows are equivalent to paths
Lemma univalent_groupoid_arrow_weq_path {ugpd : univalent_groupoid} {a b : ob ugpd} :
(a --> b) a = b.
Proof.
intermediate_weq (iso a b).
- apply (@pregroupoid_hom_weq_iso ugpd).
- apply invweq; use make_weq.
+ exact idtoiso.
+ apply univalent_category_is_univalent.
Defined.

## Subgroupoids

Every category has a subgroupoid of all the objects and only the isos.
Definition maximal_subgroupoid {C : precategory} : pregroupoid.
Proof.
use make_pregroupoid.
- use make_precategory; use tpair.
+ use tpair.
× exact (ob C).
× exact (λ a b, f : a --> b, is_iso f).
+ unfold precategory_id_comp; cbn.
use make_dirprod.
× exact (λ a, identity a,, identity_is_iso _ _).
× intros ? ? ? f g; exact (pr1 g pr1 f,, is_iso_comp_of_isos f g).
+ use make_dirprod;
intros;
apply eq_iso.
× apply id_left.
× apply id_right.
+ use make_dirprod; intros; apply eq_iso.
× apply assoc.
× apply assoc'.
- intros ? ? f; use (is_iso_qinv f).
+ exact (iso_inv_from_iso f).
+ use make_dirprod; apply eq_iso.
× apply iso_inv_after_iso.
× apply iso_after_iso_inv.
Defined.

Goal C:precategory, pregroupoid_to_precategory (@maximal_subgroupoid (C^op))
= (@maximal_subgroupoid C)^op.
Proof.
Fail reflexivity.
Abort.
Goal (C:precategory) (a b:C) (f : C b, a ), @is_iso C^op a b f = @is_iso C b a f.
Proof.
Fail reflexivity.
Abort.
Goal (C:precategory) (a b:C) (f : C b, a ),
@is_z_isomorphism C^op a b f = @is_z_isomorphism C b a f.
Proof.
Fail reflexivity.
Abort.

## Discrete categories

See Categories.categories.StandardCategories for a proof that any discrete category is equivalent to the path groupoid of its objects.
A discrete category is a univalent pregroupoid with an underlying setcategory. Why? In this case, all arrows must be identities: every arrow has an inverse, and isos induce equality (by univalence).
In a discrete category, hom-types are propositions.
Lemma discrete_category_hom_prop {disc : discrete_category} {a b : ob disc} :
isaprop (a --> b).
Proof.
apply (@isofhlevelweqf _ (a = b)).
- apply invweq, (@univalent_groupoid_arrow_weq_path disc).
- apply (isaset_ob (_ ,, discrete_category_is_setcategory _)).
Defined.

A functor between discrete categories is given by a function on their objects.
Lemma discrete_functor {C D : discrete_category} (f : ob C ob D) :
functor C D.
Proof.
use make_functor.
- use make_functor_data.
+ apply f.
+ intros a b atob.
pose (aeqb := @univalent_groupoid_arrow_weq_path C _ _ atob).
exact (transportf (λ z, _ f a, z ) (maponpaths f aeqb) (identity _)).
- split.
+ intro; apply discrete_category_hom_prop.
+ intros ? ? ? ? ?; apply discrete_category_hom_prop.
Defined.

Definition discrete_cat_nat_trans {C : precategory} {D : discrete_category}
{F G : functor C D} (t : x : ob C, F x --> G x) : is_nat_trans F G t.
Proof.
intros ? ? ?; apply discrete_category_hom_prop.
Defined.