open import 1Lab.Reflection.Induction

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

open import Cat.Diagram.Initial
open import Cat.Functor.Adjoint
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)