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)))))