open import 1Lab.Reflection.Induction

open import Algebra.Group.Cat.Base
open import Algebra.Group

open import Cat.Diagram.Initial
open import Cat.Prelude

module Algebra.Group.Free where

private variable
β : Level
A : Type β
open is-group-hom
open Group-on
open Initial


# Free groupsπ

We give a direct, higher-inductive constructor of the free group on a type of generators. While we allow the parameter to be any type, these are best behaved in the case where is a set; In this case, 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-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 = to-group fg where
fg : make-group (Free-group A)
fg .make-group.group-is-set = squash
fg .make-group.unit = nil
fg .make-group.mul = _β_
fg .make-group.inv = inv
fg .make-group.assoc = f-assoc
fg .make-group.invl = f-invl
fg .make-group.idl = 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 β B x β β y β 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 we let our reflection machinery handle it for us.

unquoteDef Free-elim-prop = make-elim-with (default-elim-visible into 1)
Free-elim-prop (quote Free-group)


## 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 β) β Groups.Hom (Free-Group A) G
fold-free-group {A = A} {G = G , ggrp} map = total-hom 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 itβ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-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 is-group-hom

go-hom : is-group-hom _ _ go
go-hom .pres-β x y = refl


Now, given a set we must come up with a group with a map (in where is the underlying set functor), such that, for any other group any map can be factored uniquely as As hinted above, we pick the free group with as its set of generators, and the universal map is in fact inc.

open Free-object

make-free-group : β {β} (S : Set β) β Free-object GrpβͺSets S
make-free-group S .free = Free-Group β S β
make-free-group S .unit = inc
make-free-group S .fold = fold-free-group
make-free-group S .commute = refl
make-free-group S .unique {H} g p =
ext \$ Free-elim-prop _ (Ξ» _ β hlevel 1)
(p #β_)
(Ξ» a p b q β g.pres-β a b β apβ H._β_ p q)
(Ξ» a p β g.pres-inv β ap H.inverse p)
g.pres-id
where
module H = Group-on (H .snd)
module g = is-group-hom (g .preserves)

module Free-groups {β} (S : Set β) = Free-object (make-free-group S)