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

private variable
  β„“ : Level
  A : Type β„“
open is-group-hom
open Group-on
open Initial
open ↓Obj
open ↓Hom

Free GroupsπŸ”—

We give a direct, higher-inductive constructor of the free group F(A)F(A) on a type AA of generators. While we allow the parameter to be any type, these are best behaved in the case where AA is a set; In this case, FF 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 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) (go x) (bd y z (go y) (go z)))
      (bd (x β—† y) z (bd x y (go x) (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-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 ⌟) β†’ 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 GG, it’s GG’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 SS, we must come up with a group GG, with a map η:S→U(G)\eta : S \to U(G) (in Sets\mathbf{Sets}, where UU is the underlying set functor), such that, for any other group HH, any map S→U(H)S \to U(H) can be factored uniquely as S→ηU(G)→U(H)S \xrightarrow{\eta} U(G) \to U(H). As hinted above, we pick G=Free(S)G = \mathrm{Free}(S), the free group with SS as its set of generators, and the universal map η\eta is in fact inc.

make-free-group : make-left-adjoint (Forget {β„“})
make-free-group .Ml.free S = Free-Group ∣ S ∣
make-free-group .Ml.unit _ = inc
make-free-group .Ml.universal f = fold-free-group f
make-free-group .Ml.commutes f = refl
make-free-group .Ml.unique {y = y} {g = g} p =
  Homomorphism-path $ Free-elim-prop _ (Ξ» _ β†’ hlevel!)
    (p $β‚š_)
    (Ξ» a b p q β†’ apβ‚‚ y._⋆_ p q βˆ™ sym (g .preserves .is-group-hom.pres-⋆ _ _))
    (Ξ» a p β†’ ap y.inverse p βˆ™ sym (is-group-hom.pres-inv (g .preserves)))
    (sym (is-group-hom.pres-id (g .preserves)))
  where module y = Group-on (y .snd)
module Free-groups {β„“} = make-left-adjoint (make-free-group {β„“ = β„“})