open import Algebra.Group.Cat.Base open import Algebra.Group open import Cat.Diagram.Initial open import Cat.Functor.Adjoint open import Cat.Instances.Comma open import Cat.Prelude module Algebra.Group.Free where

# Free Groupsπ

We give a direct, higher-inductive constructor of the **free group $F(A)$ on a type $A$ of generators**. While we allow the parameter to be any type, these are best behaved in the case where $A$ is a set; In this case, $F$ satisfies the expected universal property.

data Free-group (A : Type β) : Type β where inc : A β Free-group A

The higher-inductive presentation of free algebraic structures is very direct: There is no need to describe a set of words and then quotient by an appropriate (complicated) equivalence relation: we can define point constructors corresponding to the operations of a group, then add in the path constructors that make this into a group.

_β_ : Free-group A β Free-group A β Free-group A inv : Free-group A β Free-group A nil : Free-group A

We postulate precisely the data that is needed by make-group. This is potentially more data than is needed, but constructing maps out of Free-group is most conveniently done using the universal property, and there, this redundancy doesnβt matter.

f-assoc : β x y z β (x β y) β z β‘ x β (y β z) f-invl : β x β inv x β x β‘ nil f-invr : β x β x β inv x β‘ nil f-idl : β x β nil β x β‘ x squash : is-set (Free-group A)

We can package these constructors together to give a group with underlying set Free-group. See what was meant by βprecisely the data needed by make-group?β

Free-Group : Type β β Group β Free-Group A .fst = Free-group A Free-Group A .snd = make-group squash nil _β_ inv f-assoc f-invl f-invr f-idl

This lemma will be very useful later. It says that whenever you want to prove a proposition by induction on Free-group, it suffices to address the value constructors. This is because propositions automatically respect (higher) path constructors.

Free-elim-prop : β {β} (B : Free-group A β Type β) β (β x β is-prop (B x)) β (β x β B (inc x)) β (β x y β B x β B y β B (x β y)) β (β x β B x β B (inv x)) β B nil β β x β B x

##
The proof of it is a direct (by which I mean repetitive) case analysis, so Iβve put it in a `<details>`

tag.

Free-elim-prop B bp bi bd binv bnil = go where go : β x β B x go (inc x) = bi x go (x β y) = bd x y (go x) (go y) go (inv x) = binv x (go x) go nil = bnil go (f-assoc x y z i) = is-propβpathp (Ξ» i β bp (f-assoc x y z i)) (bd (x β y) z (bd x y (go x) (go y)) (go z)) (bd x (y β z) (go x) (bd y z (go y) (go z))) i go (f-invl x i) = is-propβpathp (Ξ» i β bp (f-invl x i)) (bd (inv x) x (binv x (go x)) (go x)) bnil i go (f-invr x i) = is-propβpathp (Ξ» i β bp (f-invr x i)) (bd x (inv x) (go x) (binv x (go x))) bnil i go (f-idl x i) = is-propβpathp (Ξ» i β bp (f-idl x i)) (bd nil x bnil (go x)) (go x) i go (squash x y p q i j) = is-propβsquarep (Ξ» i j β bp (squash x y p q i j)) (Ξ» i β go x) (Ξ» i β go (p i)) (Ξ» i β go (q i)) (Ξ» i β go y) i j

## Universal Propertyπ

We now prove the universal property of Free-group, or, more specifically, of the map inc: It gives a universal way of mapping from the category of sets to an object in the category of groups, in that any map from a set to (the underlying set of) a group factors uniquely through inc. To establish this result, we first implement a helper function, fold-free-group, which, given the data of where to send the generators of a free group, determines a group homomorphism.

fold-free-group : {A : Type β} {G : Group β} β (A β G .fst) β Groups.Hom (Free-Group A) G fold-free-group {A = A} {G = G , ggrp} map = go , go-hom where module G = Group-on ggrp

While it might seem that there are many cases to consider when defining the function go, for most of them, our hand is forced: For example, we must take multiplication in the free group (the _β_ constructor) to multiplication in the codomain.

go : Free-group A β G go (inc x) = map x go (x β y) = go x G.β go y go (inv x) = go x G.β»ΒΉ go nil = G.unit

Since _β_ is interpreted as multiplication in $G$, itβs $G$βs associativity, identity and inverse laws that provide the cases for Free-groupβs higher constructors.

go (f-assoc x y z i) = G.associative {x = go x} {y = go y} {z = go z} (~ i) go (f-invl x i) = G.inversel {x = go x} i go (f-invr x i) = G.inverser {x = go x} i go (f-idl x i) = G.idl {x = go x} i go (squash x y p q i j) = G.has-is-set (go x) (go y) (Ξ» i β go (p i)) (Ξ» i β go (q i)) i j open Group-hom go-hom : Group-hom _ _ go go-hom .pres-β x y = refl

Now, given a set $S$, we must come up with a group $G$, with a map $\eta : S \to U(G)$ (in $\sets$, where $U$ is the underlying set functor), such that, for any other group $H$, any map $S \to U(H)$ can be factored uniquely as $S \xrightarrow{\eta} U(G) \to U(H)$. As hinted above, we pick $G = \id{Free}(S)$, the free group with $S$ as its set of generators, and the universal map $\eta$ is in fact inc.

Free-universal-maps : β s β Universal-morphism s (Forget {β}) Free-universal-maps S = um where it : βObj _ Forget it .x = tt it .y = Free-Group β£ S β£ it .map = inc

To prove that this map is unique, suppose we have a group $H$ together with a map $g : S \to U(H)$. We can insert $\id{Free}(S)$ in the middle by breaking this map down as

$S \xrightarrow{\id{inc}} U(\id{Free}(S) \xrightarrow{\id{fold}(g)} H)$

um : Initial _ um .bot = it um .hasβ₯ other = contr factor unique where g : β£ S β£ β other .y .fst g = other .map factor : βHom _ _ it other factor .Ξ± = tt factor .Ξ² = fold-free-group g factor .sq = refl

To show that this factorisation is unique, suppose we had some other group homomorphism $g' : \id{Free}(S) \to H$, which also has the property that $U(g') \circ \id{inc} = g$; We must show that it is equal to $\id{fold}(g)$, which we can do pointwise, so assume we have a $x : \id{Free}(S)$.

By induction on $x$, it suffices to consider the cases where $x$ is a generator, or one of the group operations (inverses, multiplication, or the identity). The case for generators is the most interesting: We have some $y : S$, and must show that $g(y) = U(g')(\id{inc}(y))$; but this is immediate, by assumption. The other cases all follow from the induction hypotheses and $g'$ being a group homomorphism.

unique : β x β factor β‘ x unique factoring = βHom-path _ _ refl path where abstract path : factor .Ξ² β‘ factoring .Ξ² path = Ξ£-prop-path (Ξ» _ β Group-hom-is-prop) (funext (Free-elim-prop _ (Ξ» _ β y other .snd .has-is-set _ _) (Ξ» x β happly (factoring .sq) _) (Ξ» _ _ p q β apβ (other .y .snd ._β_) p q β sym (factoring .Ξ² .snd .pres-β _ _)) (Ξ» _ p β ap (other .y .snd .inverse) p β sym (pres-inv (factoring .Ξ² .snd))) (sym (pres-id (factoring .Ξ² .snd)))))