open import Algebra.Prelude open import Algebra.Group open import Cat.Prelude module Algebra.Group.Cat.Base where

# The category of Groups🔗

The category of groups, as the name implies, has its objects the Groups, with the morphisms between them the group homomorphisms.

Groups : ∀ ℓ → Precategory (lsuc ℓ) ℓ Groups ℓ = c where open Precategory open Group-hom open Group-on c : Precategory _ _ c .Ob = Group ℓ c .Hom A B = Group[ A ⇒ B ] c .Hom-set _ (B , bg) = hlevel 2 where open Group-on bg

We must show that the identity is a group homomorphisms, and group homs are closed under composition, but this follows immediately from the properties of equality:

c .id .fst = λ x → x c .id .snd = record { pres-⋆ = λ _ _ → refl } c ._∘_ {x} {y} {z} (f , fh) (g , gh) = (λ x → f (g x)) , fogh where abstract fogh : Group-hom x z (λ x → f (g x)) fogh .pres-⋆ x y = ap f (gh .pres-⋆ x y) ∙ fh .pres-⋆ _ _ c .idr f = Σ-prop-path (λ _ → Group-hom-is-prop) refl c .idl f = Σ-prop-path (λ _ → Group-hom-is-prop) refl c .assoc f g h = Σ-prop-path (λ _ → Group-hom-is-prop) refl module Groups {ℓ} = Cat (Groups ℓ)

## The underlying set🔗

The category of groups admits a faithful functor into the category of sets, written $U : \id{Groups} \to \sets$, which projects out the underlying set of the group. Faithfulness of this functor says, in more specific words, that equality of group homomorphisms can be tested by comparing the underlying morphisms of sets.

Forget : Functor (Groups ℓ) (Sets ℓ) Forget .F₀ (G , ggroup) = G , ggroup .Group-on.has-is-set Forget .F₁ = fst Forget .F-id = refl Forget .F-∘ _ _ = refl Forget-is-faithful : is-faithful (Forget {ℓ}) Forget-is-faithful = Σ-prop-path λ _ → Group-hom-is-prop

## Univalence🔗

The structure identity principle already implies that identification of groups is equivalent to isomorphism of groups. We now extend this to proving that the category of groups is univalent, but first we take a detour by showing that isomorphisms in the category of groups are the same thing as homomorphic equivalences of the groups’ underlying types.

Group-equiv≃Groups-iso : ∀ {A B : Group ℓ} → (Σ (Group≃ A B)) ≃ (A Groups.≅ B) Group-equiv≃Groups-iso {A = A} {B = B} .fst ((f , eqv) , grh) = Groups.make-iso (f , grh) (equiv→inverse eqv , inv-group-hom) (Forget-is-faithful (funext (equiv→section eqv))) (Forget-is-faithful (funext (equiv→retraction eqv)))

To build an isomorphism given a homomorphic equivalence, we use Forget-is-faithful, reducing equality of morphisms in Groups to equality of morphisms in Sets. But then, the data of an equivalence guarantees that it has a two-sided inverse, so the only thing left to establish is that the inverse of a homomorphic equivalence is also homomorphic:

where module A = Group-on (A .snd) module B = Group-on (B .snd) open Group-hom g : B .fst → A .fst g = equiv→inverse eqv abstract inv-group-hom : Group-hom B A g inv-group-hom .pres-⋆ x y = g (x B.⋆ y) ≡˘⟨ ap₂ (λ x y → g (x B.⋆ y)) (equiv→section eqv _) (equiv→section eqv _) ⟩≡˘ g (f (g x) B.⋆ f (g y)) ≡˘⟨ ap g (grh .pres-⋆ _ _) ⟩≡˘ g (f (g x A.⋆ g y)) ≡⟨ equiv→retraction eqv _ ⟩≡ g x A.⋆ g y ∎

With this equivalence in hands, we can establish that the category of groups is indeed univalent.

Groups-is-category : is-category (Groups ℓ) Groups-is-category = iso≃path→is-category _ eqv where open is-iso eqv : ∀ {A B} → (A ≡ B) ≃ (A Groups.≅ B) eqv {A} {B} = (A ≡ B) ≃⟨ SIP Group-univalent e⁻¹ ⟩≃ Σ (Group≃ A B) ≃⟨ Group-equiv≃Groups-iso ⟩≃ (A Groups.≅ B) ≃∎