# Groupoids

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.

Created on 2022-09-21.
Last modified on 2024-03-14.

module category-theory.groupoids where

Imports
open import category-theory.categories
open import category-theory.functors-categories
open import category-theory.isomorphisms-in-categories
open import category-theory.isomorphisms-in-precategories
open import category-theory.precategories
open import category-theory.pregroupoids

open import foundation.1-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.iterated-dependent-pair-types
open import foundation.propositions
open import foundation.sets
open import foundation.strictly-involutive-identity-types
open import foundation.torsorial-type-families
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels


## Idea

A groupoid is a category in which every morphism is an isomorphism.

## Definition

is-groupoid-prop-Category :
{l1 l2 : Level} (C : Category l1 l2) → Prop (l1 ⊔ l2)
is-groupoid-prop-Category C =
is-pregroupoid-prop-Precategory (precategory-Category C)

is-groupoid-Category :
{l1 l2 : Level} (C : Category l1 l2) → UU (l1 ⊔ l2)
is-groupoid-Category C =
is-pregroupoid-Precategory (precategory-Category C)

Groupoid : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Groupoid l1 l2 = Σ (Category l1 l2) is-groupoid-Category

module _
{l1 l2 : Level} (G : Groupoid l1 l2)
where

category-Groupoid : Category l1 l2
category-Groupoid = pr1 G

precategory-Groupoid : Precategory l1 l2
precategory-Groupoid = precategory-Category category-Groupoid

obj-Groupoid : UU l1
obj-Groupoid = obj-Category category-Groupoid

hom-set-Groupoid : obj-Groupoid → obj-Groupoid → Set l2
hom-set-Groupoid = hom-set-Category category-Groupoid

hom-Groupoid : obj-Groupoid → obj-Groupoid → UU l2
hom-Groupoid = hom-Category category-Groupoid

id-hom-Groupoid :
{x : obj-Groupoid} → hom-Groupoid x x
id-hom-Groupoid = id-hom-Category category-Groupoid

comp-hom-Groupoid :
{x y z : obj-Groupoid} →
hom-Groupoid y z → hom-Groupoid x y → hom-Groupoid x z
comp-hom-Groupoid = comp-hom-Category category-Groupoid

associative-comp-hom-Groupoid :
{x y z w : obj-Groupoid}
(h : hom-Groupoid z w) (g : hom-Groupoid y z) (f : hom-Groupoid x y) →
comp-hom-Groupoid (comp-hom-Groupoid h g) f ＝
comp-hom-Groupoid h (comp-hom-Groupoid g f)
associative-comp-hom-Groupoid =
associative-comp-hom-Category category-Groupoid

involutive-eq-associative-comp-hom-Groupoid :
{x y z w : obj-Groupoid}
(h : hom-Groupoid z w) (g : hom-Groupoid y z) (f : hom-Groupoid x y) →
comp-hom-Groupoid (comp-hom-Groupoid h g) f ＝ⁱ
comp-hom-Groupoid h (comp-hom-Groupoid g f)
involutive-eq-associative-comp-hom-Groupoid =
involutive-eq-associative-comp-hom-Category category-Groupoid

left-unit-law-comp-hom-Groupoid :
{x y : obj-Groupoid} (f : hom-Groupoid x y) →
( comp-hom-Groupoid id-hom-Groupoid f) ＝ f
left-unit-law-comp-hom-Groupoid =
left-unit-law-comp-hom-Category category-Groupoid

right-unit-law-comp-hom-Groupoid :
{x y : obj-Groupoid} (f : hom-Groupoid x y) →
( comp-hom-Groupoid f id-hom-Groupoid) ＝ f
right-unit-law-comp-hom-Groupoid =
right-unit-law-comp-hom-Category category-Groupoid

iso-Groupoid : (x y : obj-Groupoid) → UU l2
iso-Groupoid = iso-Category category-Groupoid

is-groupoid-Groupoid : is-groupoid-Category category-Groupoid
is-groupoid-Groupoid = pr2 G


## Property

### The type of groupoids with respect to universe levels l1 and l2 is equivalent to the type of 1-types in l1

#### The groupoid associated to a 1-type

module _
{l : Level} (X : 1-Type l)
where

obj-groupoid-1-Type : UU l
obj-groupoid-1-Type = type-1-Type X

precategory-Groupoid-1-Type : Precategory l l
precategory-Groupoid-1-Type =
make-Precategory
( obj-groupoid-1-Type)
( Id-Set X)
( λ q p → p ∙ q)
( λ x → refl)
( λ r q p → inv (assoc p q r))
( λ p → right-unit)
( λ p → left-unit)

is-category-groupoid-1-Type :
is-category-Precategory precategory-Groupoid-1-Type
is-category-groupoid-1-Type x =
fundamental-theorem-id
( is-contr-equiv'
( Σ ( Σ (type-1-Type X) (λ y → x ＝ y))
( λ (y , p) →
Σ ( Σ (y ＝ x) (λ q → q ∙ p ＝ refl))
( λ (q , l) → p ∙ q ＝ refl)))
( ( equiv-tot
( λ y →
equiv-tot
( λ p →
associative-Σ
( y ＝ x)
( λ q → q ∙ p ＝ refl)
( λ (q , r) → p ∙ q ＝ refl)))) ∘e
( associative-Σ
( type-1-Type X)
( λ y → x ＝ y)
( λ (y , p) →
Σ ( Σ (y ＝ x) (λ q → q ∙ p ＝ refl))
( λ (q , l) → p ∙ q ＝ refl))))
( is-contr-iterated-Σ 2
( is-torsorial-Id x ,
( x , refl) ,
( is-contr-equiv
( Σ (x ＝ x) (λ q → q ＝ refl))
( equiv-tot (λ q → equiv-concat (inv right-unit) refl))
( is-torsorial-Id' refl)) ,
( refl , refl) ,
( is-proof-irrelevant-is-prop
( is-1-type-type-1-Type X x x refl refl)
( refl)))))
( iso-eq-Precategory precategory-Groupoid-1-Type x)

is-groupoid-groupoid-1-Type :
is-pregroupoid-Precategory precategory-Groupoid-1-Type
pr1 (is-groupoid-groupoid-1-Type x y p) = inv p
pr1 (pr2 (is-groupoid-groupoid-1-Type x y p)) = left-inv p
pr2 (pr2 (is-groupoid-groupoid-1-Type x y p)) = right-inv p

groupoid-1-Type : Groupoid l l
pr1 (pr1 groupoid-1-Type) = precategory-Groupoid-1-Type
pr2 (pr1 groupoid-1-Type) = is-category-groupoid-1-Type
pr2 groupoid-1-Type = is-groupoid-groupoid-1-Type


#### The 1-type associated to a groupoid

module _
{l1 l2 : Level} (G : Groupoid l1 l2)
where

1-type-Groupoid : 1-Type l1
1-type-Groupoid = obj-1-type-Category (category-Groupoid G)


#### The groupoid obtained from the 1-type induced by a groupoid G is G itself

module _
{l1 l2 : Level} (G : Groupoid l1 l2)
where

functor-equiv-groupoid-1-type-Groupoid :
functor-Category
( category-Groupoid (groupoid-1-Type (1-type-Groupoid G)))
( category-Groupoid G)
pr1 functor-equiv-groupoid-1-type-Groupoid = id
pr1 (pr2 functor-equiv-groupoid-1-type-Groupoid) {x} {.x} refl =
id-hom-Groupoid G
pr1 (pr2 (pr2 functor-equiv-groupoid-1-type-Groupoid)) {x} refl refl =
inv (right-unit-law-comp-hom-Groupoid G (id-hom-Groupoid G))
pr2 (pr2 (pr2 functor-equiv-groupoid-1-type-Groupoid)) x = refl


#### The 1-type obtained from the groupoid induced by a 1-type X is X itself

module _
{l : Level} (X : 1-Type l)
where

equiv-1-type-groupoid-1-Type :
type-equiv-1-Type (1-type-Groupoid (groupoid-1-Type X)) X
equiv-1-type-groupoid-1-Type = id-equiv