Require Import Basics Types Group Subgroup
  WildCat.Core WildCat.Universe Colimits.Coeq
  Truncations.Core Truncations.SeparatedTrunc
  Spaces.List.Core Spaces.List.Theory.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.

(** [IsFreeGroup] is defined in Group.v. In this file we construct free groups and and prove properties about them. *)

(** We construct the free group on a type [A] as a higher inductive type. This construction is due to Kraus-Altenkirch 2018 arXiv:1805.02069. Their construction is actually more general, but we set-truncate it to suit our needs which is the free group as a set. This is a very simple HIT in a similar manner to the abelianization HIT used in Algebra.AbGroup.Abelianization. *)

Section Reduction.

  Universe u.
  Context (A : Type@{u}).

  Local Open Scope list_scope.

  (** We define words (with inverses) on A to be lists of marked elements of A *)
  Local Definition Words : Type@{u} := list (A + A).

  (** Given a marked element of A we can change its mark *)
  Local Definition change_sign : A + A -> A + A := equiv_sum_symm A A.

  (** We introduce a local notation for [change_sign]. It is only defined in this section however. *)
  Local Notation "a ^'" := (change_sign a) (at level 1).

  (** Changing sign is an involution *)
  Local Definition change_sign_inv a : a^'^' = a.
A: Type
a: (A + A)%type
(a ^') ^' = a
  Proof.
A: Type
a: (A + A)%type
(a ^') ^' = a
    by destruct a.
  Defined.

  (** Now we wish to define the free group on A as the following HIT: 

    HIT N(A) : hSet
     | eta : Words -> N(A)
     | tau (x : Words) (a : A + A) (y : Words)
         : eta (x ++ [a] ++ [a^] ++ y) = eta (x ++ y).

    Since we cannot write our HITs directly like this (without resorting to private inductive types), we will construct this HIT out of HITs we know. In fact, we can define N(A) as a coequalizer. *)

  Local Definition map1 : Words * (A + A) * Words -> Words.
A: Type
Words * (A + A) * Words -> Words
  Proof.
A: Type
Words * (A + A) * Words -> Words
    intros [[x a] y].
A: Type
x: Words
a: (A + A)%type
y: Words
Words
    exact (x ++ [a] ++ [a^'] ++ y).
  Defined.

  Arguments map1 _ /.

  Local Definition map2 : Words * (A + A) * Words -> Words.
A: Type
Words * (A + A) * Words -> Words
  Proof.
A: Type
Words * (A + A) * Words -> Words
    intros [[x a] y].
A: Type
x: Words
a: (A + A)%type
y: Words
Words
    exact (x ++ y).
  Defined.

  Arguments map2 _ /.

  (** Now we can define the underlying type of the free group as the 0-truncated coequalizer of these two maps *)
  Definition freegroup_type : Type := Tr 0 (Coeq map1 map2).

  (** This is the point constructor *)
  Definition freegroup_eta : Words -> freegroup_type := tr o coeq.

  (** This is the path constructor *)
  Definition freegroup_tau (x : Words) (a : A + A) (y : Words)
    : freegroup_eta (x ++ [a] ++ [a^'] ++ y) = freegroup_eta (x ++ y).
A: Type
x: Words
a: (A + A)%type
y: Words
freegroup_eta (x ++ [a] ++ [a ^'] ++ y) =
freegroup_eta (x ++ y)
  Proof.
A: Type
x: Words
a: (A + A)%type
y: Words
freegroup_eta (x ++ [a] ++ [a ^'] ++ y) =
freegroup_eta (x ++ y)
    apply path_Tr, tr.
A: Type
x: Words
a: (A + A)%type
y: Words
coeq (x ++ [a] ++ [a ^'] ++ y) = coeq (x ++ y)
    exact ((cglue (x, a, y))).
  Defined.

  (** The group operation *)
  #[export] Instance sgop_freegroup : SgOp freegroup_type.
A: Type
SgOp freegroup_type
  Proof.
A: Type
SgOp freegroup_type
    intros x y.
A: Type
x, y: freegroup_type
freegroup_type
    strip_truncations.
A: Type
y, x: Coeq map1 map2
freegroup_type
    revert x; snapply Coeq_rec.
A: Type
y: Coeq map1 map2
Words -> freegroup_type
A: Type
y: Coeq map1 map2
forall b : Words * (A + A) * Words,
?coeq' (map1 b) = ?coeq' (map2 b)
    {
A: Type
y: Coeq map1 map2
Words -> freegroup_type intros x; revert y.
A: Type
x: Words
Coeq map1 map2 -> freegroup_type
      snapply Coeq_rec.
A: Type
x: Words
Words -> freegroup_type
A: Type
x: Words
forall b : Words * (A + A) * Words,
?coeq' (map1 b) = ?coeq' (map2 b)
      {
A: Type
x: Words
Words -> freegroup_type intros y.
A: Type
x, y: Words
freegroup_type
        exact (freegroup_eta (x ++ y)). }
A: Type
x: Words
forall b : Words * (A + A) * Words,
(fun y : Words => freegroup_eta (x ++ y)) (map1 b) =
(fun y : Words => freegroup_eta (x ++ y)) (map2 b)
      intros [[y a] z]; simpl.
A: Type
x, y: Words
a: (A + A)%type
z: Words
freegroup_eta (x ++ y ++ a :: a ^' :: z) =
freegroup_eta (x ++ y ++ z)
      change (freegroup_eta (x ++ y ++ ([a] ++ [a^'] ++ z))
        = freegroup_eta (x ++ y ++ z)).
A: Type
x, y: Words
a: (A + A)%type
z: Words
freegroup_eta (x ++ y ++ [a] ++ [a ^'] ++ z) =
freegroup_eta (x ++ y ++ z)
      rhs napply ap.
A: Type
x, y: Words
a: (A + A)%type
z: Words
freegroup_eta (x ++ y ++ [a] ++ [a ^'] ++ z) =
freegroup_eta ?Goal
A: Type
x, y: Words
a: (A + A)%type
z: Words
x ++ y ++ z = ?Goal
      2: napply app_assoc.
A: Type
x, y: Words
a: (A + A)%type
z: Words
freegroup_eta (x ++ y ++ [a] ++ [a ^'] ++ z) =
freegroup_eta ((x ++ y) ++ z)
      lhs napply ap.
A: Type
x, y: Words
a: (A + A)%type
z: Words
x ++ y ++ [a] ++ [a ^'] ++ z = ?Goal
A: Type
x, y: Words
a: (A + A)%type
z: Words
freegroup_eta ?Goal = freegroup_eta ((x ++ y) ++ z)
      1: napply app_assoc.
A: Type
x, y: Words
a: (A + A)%type
z: Words
freegroup_eta ((x ++ y) ++ [a] ++ [a ^'] ++ z) =
freegroup_eta ((x ++ y) ++ z)
      napply (freegroup_tau _ a). }
A: Type
y: Coeq map1 map2
forall b : Words * (A + A) * Words,
(fun x : Words =>
 Coeq_rec freegroup_type
   (fun y : Words => freegroup_eta (x ++ y))
   (fun b0 : Words * (A + A) * Words =>
    (fun fst : Words * (A + A) =>
     (fun (y : Words) (a : A + A) (z : Words) =>
      (ap freegroup_eta
         (app_assoc x y ([a] ++ [a ^'] ++ z)) @
       freegroup_tau (x ++ y) a z) @
      (ap freegroup_eta (app_assoc x y z))^
      :
      freegroup_eta (x ++ map1 (y, a, z)) =
      freegroup_eta (x ++ map2 (y, a, z)))
       (Overture.fst fst) (snd fst)) (fst b0) (snd b0))
   y) (map1 b) =
(fun x : Words =>
 Coeq_rec freegroup_type
   (fun y : Words => freegroup_eta (x ++ y))
   (fun b0 : Words * (A + A) * Words =>
    (fun fst : Words * (A + A) =>
     (fun (y : Words) (a : A + A) (z : Words) =>
      (ap freegroup_eta
         (app_assoc x y ([a] ++ [a ^'] ++ z)) @
       freegroup_tau (x ++ y) a z) @
      (ap freegroup_eta (app_assoc x y z))^
      :
      freegroup_eta (x ++ map1 (y, a, z)) =
      freegroup_eta (x ++ map2 (y, a, z)))
       (Overture.fst fst) (snd fst)) (fst b0) (snd b0))
   y) (map2 b)
    intros [[c b] d].
A: Type
y: Coeq map1 map2
c: Words
b: (A + A)%type
d: Words
Coeq_rec freegroup_type
  (fun y : Words =>
   freegroup_eta (map1 (c, b, d) ++ y))
  (fun b0 : Words * (A + A) * Words =>
   (ap freegroup_eta
      (app_assoc (map1 (c, b, d)) (fst (fst b0))
         ([snd (fst b0)] ++
          [(snd (fst b0)) ^'] ++ snd b0)) @
    freegroup_tau (map1 (c, b, d) ++ fst (fst b0))
      (snd (fst b0)) (snd b0)) @
   (ap freegroup_eta
      (app_assoc (map1 (c, b, d)) (fst (fst b0))
         (snd b0)))^) y =
Coeq_rec freegroup_type
  (fun y : Words =>
   freegroup_eta (map2 (c, b, d) ++ y))
  (fun b0 : Words * (A + A) * Words =>
   (ap freegroup_eta
      (app_assoc (map2 (c, b, d)) (fst (fst b0))
         ([snd (fst b0)] ++
          [(snd (fst b0)) ^'] ++ snd b0)) @
    freegroup_tau (map2 (c, b, d) ++ fst (fst b0))
      (snd (fst b0)) (snd b0)) @
   (ap freegroup_eta
      (app_assoc (map2 (c, b, d)) (fst (fst b0))
         (snd b0)))^) y
    revert y.
A: Type
c: Words
b: (A + A)%type
d: Words
forall y : Coeq map1 map2,
Coeq_rec freegroup_type
  (fun y0 : Words =>
   freegroup_eta (map1 (c, b, d) ++ y0))
  (fun b0 : Words * (A + A) * Words =>
   (ap freegroup_eta
      (app_assoc (map1 (c, b, d)) (fst (fst b0))
         ([snd (fst b0)] ++
          [(snd (fst b0)) ^'] ++ snd b0)) @
    freegroup_tau (map1 (c, b, d) ++ fst (fst b0))
      (snd (fst b0)) (snd b0)) @
   (ap freegroup_eta
      (app_assoc (map1 (c, b, d)) (fst (fst b0))
         (snd b0)))^) y =
Coeq_rec freegroup_type
  (fun y0 : Words =>
   freegroup_eta (map2 (c, b, d) ++ y0))
  (fun b0 : Words * (A + A) * Words =>
   (ap freegroup_eta
      (app_assoc (map2 (c, b, d)) (fst (fst b0))
         ([snd (fst b0)] ++
          [(snd (fst b0)) ^'] ++ snd b0)) @
    freegroup_tau (map2 (c, b, d) ++ fst (fst b0))
      (snd (fst b0)) (snd b0)) @
   (ap freegroup_eta
      (app_assoc (map2 (c, b, d)) (fst (fst b0))
         (snd b0)))^) y
    srapply Coeq_ind_hprop.
A: Type
c: Words
b: (A + A)%type
d: Words
forall a : Words,
(fun x : Coeq map1 map2 =>
 Coeq_rec freegroup_type
   (fun y : Words =>
    freegroup_eta (map1 (c, b, d) ++ y))
   (fun b0 : Words * (A + A) * Words =>
    (ap freegroup_eta
       (app_assoc (map1 (c, b, d)) (fst (fst b0))
          ([snd (fst b0)] ++
           [(snd (fst b0)) ^'] ++ snd b0)) @
     freegroup_tau (map1 (c, b, d) ++ fst (fst b0))
       (snd (fst b0)) (snd b0)) @
    (ap freegroup_eta
       (app_assoc (map1 (c, b, d)) (fst (fst b0))
          (snd b0)))^) x =
 Coeq_rec freegroup_type
   (fun y : Words =>
    freegroup_eta (map2 (c, b, d) ++ y))
   (fun b0 : Words * (A + A) * Words =>
    (ap freegroup_eta
       (app_assoc (map2 (c, b, d)) (fst (fst b0))
          ([snd (fst b0)] ++
           [(snd (fst b0)) ^'] ++ snd b0)) @
     freegroup_tau (map2 (c, b, d) ++ fst (fst b0))
       (snd (fst b0)) (snd b0)) @
    (ap freegroup_eta
       (app_assoc (map2 (c, b, d)) (fst (fst b0))
          (snd b0)))^) x) (coeq a)
    intro a.
A: Type
c: Words
b: (A + A)%type
d, a: Words
(fun x : Coeq map1 map2 =>
 Coeq_rec freegroup_type
   (fun y : Words =>
    freegroup_eta (map1 (c, b, d) ++ y))
   (fun b0 : Words * (A + A) * Words =>
    (ap freegroup_eta
       (app_assoc (map1 (c, b, d)) (fst (fst b0))
          ([snd (fst b0)] ++
           [(snd (fst b0)) ^'] ++ snd b0)) @
     freegroup_tau (map1 (c, b, d) ++ fst (fst b0))
       (snd (fst b0)) (snd b0)) @
    (ap freegroup_eta
       (app_assoc (map1 (c, b, d)) (fst (fst b0))
          (snd b0)))^) x =
 Coeq_rec freegroup_type
   (fun y : Words =>
    freegroup_eta (map2 (c, b, d) ++ y))
   (fun b0 : Words * (A + A) * Words =>
    (ap freegroup_eta
       (app_assoc (map2 (c, b, d)) (fst (fst b0))
          ([snd (fst b0)] ++
           [(snd (fst b0)) ^'] ++ snd b0)) @
     freegroup_tau (map2 (c, b, d) ++ fst (fst b0))
       (snd (fst b0)) (snd b0)) @
    (ap freegroup_eta
       (app_assoc (map2 (c, b, d)) (fst (fst b0))
          (snd b0)))^) x) (coeq a)
    change (freegroup_eta ((c ++ [b] ++ [b^'] ++ d) ++ a)
      = freegroup_eta ((c ++ d) ++ a)).
A: Type
c: Words
b: (A + A)%type
d, a: Words
freegroup_eta ((c ++ [b] ++ [b ^'] ++ d) ++ a) =
freegroup_eta ((c ++ d) ++ a)
    lhs_V napply ap.
A: Type
c: Words
b: (A + A)%type
d, a: Words
?Goal = (c ++ [b] ++ [b ^'] ++ d) ++ a
A: Type
c: Words
b: (A + A)%type
d, a: Words
freegroup_eta ?Goal = freegroup_eta ((c ++ d) ++ a)
    1: napply app_assoc.
A: Type
c: Words
b: (A + A)%type
d, a: Words
freegroup_eta (c ++ ([b] ++ [b ^'] ++ d) ++ a) =
freegroup_eta ((c ++ d) ++ a)
    lhs_V napply (ap (fun x => freegroup_eta (c ++ x))).
A: Type
c: Words
b: (A + A)%type
d, a: Words
?Goal = ([b] ++ [b ^'] ++ d) ++ a
A: Type
c: Words
b: (A + A)%type
d, a: Words
freegroup_eta (c ++ ?Goal) =
freegroup_eta ((c ++ d) ++ a)
    1: napply app_assoc.
A: Type
c: Words
b: (A + A)%type
d, a: Words
freegroup_eta (c ++ [b] ++ ([b ^'] ++ d) ++ a) =
freegroup_eta ((c ++ d) ++ a)
    lhs_V napply (ap (fun x => freegroup_eta (c ++ _ ++ x))).
A: Type
c: Words
b: (A + A)%type
d, a: Words
?Goal = ([b ^'] ++ d) ++ a
A: Type
c: Words
b: (A + A)%type
d, a: Words
freegroup_eta (c ++ [b] ++ ?Goal) =
freegroup_eta ((c ++ d) ++ a)
    1: napply app_assoc.
A: Type
c: Words
b: (A + A)%type
d, a: Words
freegroup_eta (c ++ [b] ++ [b ^'] ++ d ++ a) =
freegroup_eta ((c ++ d) ++ a)
    rhs_V napply ap.
A: Type
c: Words
b: (A + A)%type
d, a: Words
freegroup_eta (c ++ [b] ++ [b ^'] ++ d ++ a) =
freegroup_eta ?Goal
A: Type
c: Words
b: (A + A)%type
d, a: Words
?Goal = (c ++ d) ++ a
    2: napply app_assoc.
A: Type
c: Words
b: (A + A)%type
d, a: Words
freegroup_eta (c ++ [b] ++ [b ^'] ++ d ++ a) =
freegroup_eta (c ++ d ++ a)
    napply freegroup_tau.
  Defined.

  (** The unit of the free group is the empty word *)
  #[export] Instance monunit_freegroup_type : MonUnit freegroup_type
    := freegroup_eta nil.

  (** We can change the sign of all the elements in a word and reverse the order. This will be the inversion in the group *)
  Definition word_change_sign (x : Words) : Words
    := reverse (list_map change_sign x).

  (** Changing the sign changes the order of word concatenation *)
  Definition word_change_sign_ww (x y : Words)
    : word_change_sign (x ++ y) = word_change_sign y ++ word_change_sign x.
A: Type
x, y: Words
word_change_sign (x ++ y) =
word_change_sign y ++ word_change_sign x
  Proof.
A: Type
x, y: Words
word_change_sign (x ++ y) =
word_change_sign y ++ word_change_sign x
    unfold word_change_sign.
A: Type
x, y: Words
reverse (list_map change_sign (x ++ y)) =
reverse (list_map change_sign y) ++
reverse (list_map change_sign x)
    lhs napply (ap reverse).
A: Type
x, y: Words
list_map change_sign (x ++ y) = ?Goal
A: Type
x, y: Words
reverse ?Goal =
reverse (list_map change_sign y) ++
reverse (list_map change_sign x)
    1: napply list_map_app.
A: Type
x, y: Words
reverse
  (list_map change_sign x ++ list_map change_sign y) =
reverse (list_map change_sign y) ++
reverse (list_map change_sign x)
    napply reverse_app.
  Defined.

  (** This is also involutive *)
  Lemma word_change_sign_inv x : word_change_sign (word_change_sign x) = x.
A: Type
x: Words
word_change_sign (word_change_sign x) = x
  Proof.
A: Type
x: Words
word_change_sign (word_change_sign x) = x
    unfold word_change_sign.
A: Type
x: Words
reverse
  (list_map change_sign
     (reverse (list_map change_sign x))) = x
    lhs_V napply list_map_reverse.
A: Type
x: Words
list_map change_sign
  (reverse (reverse (list_map change_sign x))) = x
    lhs napply ap.
A: Type
x: Words
reverse (reverse (list_map change_sign x)) = ?Goal
A: Type
x: Words
list_map change_sign ?Goal = x
    1: napply reverse_reverse.
A: Type
x: Words
list_map change_sign (list_map change_sign x) = x 
    lhs_V napply list_map_compose.
A: Type
x: Words
list_map (fun x : A + A => (x ^') ^') x = x
    snapply list_map_id.
A: Type
x: Words
forall x0 : A + A,
InList x0 x -> (fun x : A + A => (x ^') ^') x0 = x0
    intros a ?.
A: Type
x: Words
a: (A + A)%type
X: InList a x
(fun x : A + A => (x ^') ^') a = a
    apply change_sign_inv.
  Defined.

  (** Changing the sign gives us left inverses *)
  Lemma word_concat_Vw x : freegroup_eta (word_change_sign x ++ x) = mon_unit.
A: Type
x: Words
freegroup_eta (word_change_sign x ++ x) = 1
  Proof.
A: Type
x: Words
freegroup_eta (word_change_sign x ++ x) = 1
    induction x.
A: Type
freegroup_eta (word_change_sign nil ++ nil) = 1
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x ++ x) = 1
freegroup_eta (word_change_sign (a :: x) ++ a :: x) =
1
    1: reflexivity.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x ++ x) = 1
freegroup_eta (word_change_sign (a :: x) ++ a :: x) =
1
    lhs napply (ap (fun x => freegroup_eta (x ++ _))).
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x ++ x) = 1
word_change_sign (a :: x) = ?Goal
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x ++ x) = 1
freegroup_eta (?Goal ++ a :: x) = 1
    1: napply reverse_cons.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x ++ x) = 1
freegroup_eta
  ((reverse
      ((fix list_map
          (A B : Type) (f : A -> B) (l : list A)
          {struct l} : list B :=
          match l with
          | nil => nil
          | x :: l0 => f x :: list_map A B f l0
          end) (A + A)%type (A + A)%type change_sign x) ++
    [a ^']) ++ a :: x) = 1
    change (freegroup_eta ((word_change_sign x ++ [a^']) ++ [a] ++ x)
      = mon_unit).
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x ++ x) = 1
freegroup_eta
  ((word_change_sign x ++ [a ^']) ++ [a] ++ x) = 1 
    lhs_V napply ap.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x ++ x) = 1
?Goal = (word_change_sign x ++ [a ^']) ++ [a] ++ x
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x ++ x) = 1
freegroup_eta ?Goal = 1
    1: napply app_assoc.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x ++ x) = 1
freegroup_eta
  (word_change_sign x ++ [a ^'] ++ [a] ++ x) = 1
    set (a' := a^').
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x ++ x) = 1
a':= a ^': (A + A)%type
freegroup_eta (word_change_sign x ++ [a'] ++ [a] ++ x) =
1
    rewrite <- (change_sign_inv a).
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x ++ x) = 1
a':= a ^': (A + A)%type
freegroup_eta
  (word_change_sign x ++ [a'] ++ [(a ^') ^'] ++ x) = 1
    lhs napply freegroup_tau.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x ++ x) = 1
a':= a ^': (A + A)%type
freegroup_eta (word_change_sign x ++ x) = 1
    exact IHx.
  Defined.

  (** And since changing the sign is involutive we get right inverses from left inverses *)
  Lemma word_concat_wV x : freegroup_eta (x ++ word_change_sign x) = mon_unit.
A: Type
x: list (A + A)
freegroup_eta (x ++ word_change_sign x) = 1
  Proof.
A: Type
x: list (A + A)
freegroup_eta (x ++ word_change_sign x) = 1
    set (x' := word_change_sign x).
A: Type
x: list (A + A)
x':= word_change_sign x: Words
freegroup_eta (x ++ x') = 1
    rewrite <- (word_change_sign_inv x).
A: Type
x: list (A + A)
x':= word_change_sign x: Words
freegroup_eta
  (word_change_sign (word_change_sign x) ++ x') = 1
    change (freegroup_eta (word_change_sign x' ++ x') = mon_unit).
A: Type
x: list (A + A)
x':= word_change_sign x: Words
freegroup_eta (word_change_sign x' ++ x') = 1
    apply word_concat_Vw.
  Defined.

  (** Inverses are defined by changing the order of a word that appears in eta. Most of the work here is checking that it is agreeable with the path constructor. *)
  #[export] Instance inverse_freegroup_type : Inverse freegroup_type.
A: Type
Inverse freegroup_type
  Proof.
A: Type
Inverse freegroup_type
    intro x.
A: Type
x: freegroup_type
freegroup_type
    strip_truncations.
A: Type
x: Coeq map1 map2
freegroup_type
    revert x; srapply Coeq_rec.
A: Type
Words -> freegroup_type
A: Type
forall b : Words * (A + A) * Words,
?coeq' (map1 b) = ?coeq' (map2 b)
    {
A: Type
Words -> freegroup_type intro x.
A: Type
x: Words
freegroup_type
      apply freegroup_eta.
A: Type
x: Words
Words
      exact (word_change_sign x). }
A: Type
forall b : Words * (A + A) * Words,
(fun x : Words => freegroup_eta (word_change_sign x))
  (map1 b) =
(fun x : Words => freegroup_eta (word_change_sign x))
  (map2 b)
    intros [[b a] c].
A: Type
b: Words
a: (A + A)%type
c: Words
freegroup_eta (word_change_sign (map1 (b, a, c))) =
freegroup_eta (word_change_sign (map2 (b, a, c)))
    unfold map1, map2.
A: Type
b: Words
a: (A + A)%type
c: Words
freegroup_eta
  (word_change_sign (b ++ [a] ++ [a ^'] ++ c)) =
freegroup_eta (word_change_sign (b ++ c))
    lhs napply ap.
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign (b ++ [a] ++ [a ^'] ++ c) = ?Goal
A: Type
b: Words
a: (A + A)%type
c: Words
freegroup_eta ?Goal =
freegroup_eta (word_change_sign (b ++ c))
    {
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign (b ++ [a] ++ [a ^'] ++ c) = ?Goal lhs napply word_change_sign_ww.
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign ([a] ++ [a ^'] ++ c) ++
word_change_sign b = ?Goal
      napply (ap (fun x => x ++ _)).
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign ([a] ++ [a ^'] ++ c) = ?Goal0 
      lhs napply word_change_sign_ww.
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign ([a ^'] ++ c) ++ word_change_sign [a] =
?Goal0
      napply (ap (fun x => x ++ _)).
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign ([a ^'] ++ c) = ?Goal0 
      lhs napply word_change_sign_ww.
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign c ++ word_change_sign [a ^'] = ?Goal0
      napply (ap (fun x => _ ++ x)).
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign [a ^'] = ?Goal0
      exact (word_change_sign_inv [a]). }
A: Type
b: Words
a: (A + A)%type
c: Words
freegroup_eta
  (((word_change_sign c ++ [a]) ++
    word_change_sign [a]) ++ word_change_sign b) =
freegroup_eta (word_change_sign (b ++ c))
    lhs_V napply ap.
A: Type
b: Words
a: (A + A)%type
c: Words
?Goal =
((word_change_sign c ++ [a]) ++ word_change_sign [a]) ++
word_change_sign b
A: Type
b: Words
a: (A + A)%type
c: Words
freegroup_eta ?Goal =
freegroup_eta (word_change_sign (b ++ c))
    1: rhs_V napply app_assoc.
A: Type
b: Words
a: (A + A)%type
c: Words
?Goal =
(word_change_sign c ++ [a]) ++
word_change_sign [a] ++ word_change_sign b
A: Type
b: Words
a: (A + A)%type
c: Words
freegroup_eta ?Goal =
freegroup_eta (word_change_sign (b ++ c))
    1: napply app_assoc.
A: Type
b: Words
a: (A + A)%type
c: Words
freegroup_eta
  (word_change_sign c ++
   [a] ++ word_change_sign [a] ++ word_change_sign b) =
freegroup_eta (word_change_sign (b ++ c))
    rhs napply ap.
A: Type
b: Words
a: (A + A)%type
c: Words
freegroup_eta
  (word_change_sign c ++
   [a] ++ word_change_sign [a] ++ word_change_sign b) =
freegroup_eta ?Goal
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign (b ++ c) = ?Goal
    2: napply word_change_sign_ww.
A: Type
b: Words
a: (A + A)%type
c: Words
freegroup_eta
  (word_change_sign c ++
   [a] ++ word_change_sign [a] ++ word_change_sign b) =
freegroup_eta
  (word_change_sign c ++ word_change_sign b)
    napply freegroup_tau.
  Defined.

  (** Now we can start to prove the group laws. Since these are hprops we can ignore what happens with the path constructor. *)

  (** Our operation is associative *)
  #[export] Instance associative_freegroup_type : Associative sg_op.
A: Type
Associative sg_op
  Proof.
A: Type
Associative sg_op
    intros x y z.
A: Type
x, y, z: freegroup_type
x * (y * z) = x * y * z
    strip_truncations.
A: Type
z, y, x: Coeq map1 map2
tr x * (tr y * tr z) = tr x * tr y * tr z
    revert x; srapply Coeq_ind_hprop; intro x.
A: Type
z, y: Coeq map1 map2
x: Words
(fun x : Coeq map1 map2 =>
 tr x * (tr y * tr z) = tr x * tr y * tr z) (coeq x)
    revert y; srapply Coeq_ind_hprop; intro y.
A: Type
z: Coeq map1 map2
x, y: Words
(fun x0 : Coeq map1 map2 =>
 (fun x : Coeq map1 map2 =>
  tr x * (tr x0 * tr z) = tr x * tr x0 * tr z)
   (coeq x)) (coeq y)
    revert z; srapply Coeq_ind_hprop; intro z.
A: Type
x, y, z: Words
(fun x0 : Coeq map1 map2 =>
 (fun x1 : Coeq map1 map2 =>
  (fun x : Coeq map1 map2 =>
   tr x * (tr x1 * tr x0) = tr x * tr x1 * tr x0)
    (coeq x)) (coeq y)) (coeq z)
    napply (ap (tr o coeq)).
A: Type
x, y, z: Words
x ++ y ++ z = (x ++ y) ++ z
    napply app_assoc.
  Defined.

  (** Left identity *)
  #[export] Instance leftidentity_freegroup_type : LeftIdentity sg_op mon_unit.
A: Type
LeftIdentity sg_op 1
  Proof.
A: Type
LeftIdentity sg_op 1
    rapply Trunc_ind.
A: Type
forall a : Coeq map1 map2, 1 * tr a = tr a
    srapply Coeq_ind_hprop; intros x.
A: Type
x: Words
(fun x : Coeq map1 map2 => 1 * tr x = tr x) (coeq x)
    reflexivity.
  Defined.

  (** Right identity *)
  #[export] Instance rightidentity_freegroup_type : RightIdentity sg_op mon_unit.
A: Type
RightIdentity sg_op 1
  Proof.
A: Type
RightIdentity sg_op 1
    rapply Trunc_ind.
A: Type
forall a : Coeq map1 map2, tr a * 1 = tr a
    srapply Coeq_ind_hprop; intros x.
A: Type
x: Words
(fun x : Coeq map1 map2 => tr x * 1 = tr x) (coeq x)
    apply (ap tr), ap.
A: Type
x: Words
x ++ nil = x
    napply app_nil.
  Defined.

  (** Left inverse *)
  #[export] Instance leftinverse_freegroup_type : LeftInverse (.*.) (^) mon_unit.
A: Type
LeftInverse sg_op inv 1
  Proof.
A: Type
LeftInverse sg_op inv 1
    rapply Trunc_ind.
A: Type
forall a : Coeq map1 map2, (tr a)^ * tr a = 1
    srapply Coeq_ind_hprop; intro x.
A: Type
x: Words
(fun x : Coeq map1 map2 => (tr x)^ * tr x = 1)
  (coeq x)
    apply word_concat_Vw.
  Defined.

  (** Right inverse *)
  #[export] Instance rightinverse_freegroup_type : RightInverse (.*.) (^) mon_unit.
A: Type
RightInverse sg_op inv 1
  Proof.
A: Type
RightInverse sg_op inv 1
    rapply Trunc_ind.
A: Type
forall a : Coeq map1 map2, tr a * (tr a)^ = 1
    srapply Coeq_ind_hprop; intro x.
A: Type
x: Words
(fun x : Coeq map1 map2 => tr x * (tr x)^ = 1)
  (coeq x)
    apply word_concat_wV.
  Defined.

  (** Finally we have defined the free group on [A] *)
  Definition FreeGroup : Group.
A: Type
Group
  Proof.
A: Type
Group
    snapply (Build_Group freegroup_type); repeat split; exact _.
  Defined.

  Definition word_rec (G : Group) (s : A -> G) : A + A -> G.
A: Type
G: Group
s: A -> G
A + A -> G
  Proof.
A: Type
G: Group
s: A -> G
A + A -> G
    intros [x|x].
A: Type
G: Group
s: A -> G
x: A
G
A: Type
G: Group
s: A -> G
x: A
G
    -
A: Type
G: Group
s: A -> G
x: A
G exact (s x).
    -
A: Type
G: Group
s: A -> G
x: A
G exact (s x)^.
  Defined.

  (** When we have a list of words we can recursively define a group element. The obvious choice would be to map [nil] to the identity and [x :: xs] to [x * words_rec xs]. This has the disadvantage that a single generating element gets mapped to [x * 1] instead of [x]. To fix this issue, we map [nil] to the identity, the singleton to the element we want, and do the rest recursively. *)
  Definition words_rec (G : Group) (s : A -> G) : Words -> G.
A: Type
G: Group
s: A -> G
Words -> G
  Proof.
A: Type
G: Group
s: A -> G
Words -> G
    intro xs.
A: Type
G: Group
s: A -> G
xs: Words
G
    induction xs as [|x [|y xs] IHxs].
A: Type
G: Group
s: A -> G
G
A: Type
G: Group
s: A -> G
x: (A + A)%type
IHxs: G
G
A: Type
G: Group
s: A -> G
x, y: (A + A)%type
xs: list (A + A)
IHxs: G
G
    -
A: Type
G: Group
s: A -> G
G exact mon_unit.
    -
A: Type
G: Group
s: A -> G
x: (A + A)%type
IHxs: G
G exact (word_rec G s x).
    -
A: Type
G: Group
s: A -> G
x, y: (A + A)%type
xs: list (A + A)
IHxs: G
G exact (word_rec G s x * IHxs).
  Defined.

  Definition words_rec_cons (G : Group) (s : A -> G) (x : A + A) (xs : Words)
    : words_rec G s (x :: xs)%list = word_rec G s x * words_rec G s xs.
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: Words
words_rec G s (x :: xs) =
word_rec G s x * words_rec G s xs
  Proof.
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: Words
words_rec G s (x :: xs) =
word_rec G s x * words_rec G s xs
    induction xs in x |- *.
A: Type
G: Group
s: A -> G
x: (A + A)%type
words_rec G s [x] = word_rec G s x * words_rec G s nil
A: Type
G: Group
s: A -> G
x, a: (A + A)%type
xs: list (A + A)
IHxs: forall x : A + A,
words_rec G s (x :: xs) =
word_rec G s x * words_rec G s xs
words_rec G s (x :: a :: xs) =
word_rec G s x * words_rec G s (a :: xs)
    -
A: Type
G: Group
s: A -> G
x: (A + A)%type
words_rec G s [x] = word_rec G s x * words_rec G s nil symmetry; napply grp_unit_r.
    -
A: Type
G: Group
s: A -> G
x, a: (A + A)%type
xs: list (A + A)
IHxs: forall x : A + A,
words_rec G s (x :: xs) =
word_rec G s x * words_rec G s xs
words_rec G s (x :: a :: xs) =
word_rec G s x * words_rec G s (a :: xs) reflexivity.
  Defined.

  Lemma words_rec_pp (G : Group) (s : A -> G)  (x y : Words)
    : words_rec G s (x ++ y) = words_rec G s x * words_rec G s y.
A: Type
G: Group
s: A -> G
x, y: Words
words_rec G s (x ++ y) =
words_rec G s x * words_rec G s y
  Proof.
A: Type
G: Group
s: A -> G
x, y: Words
words_rec G s (x ++ y) =
words_rec G s x * words_rec G s y
    induction x as [|x xs IHxs] in y |- *.
A: Type
G: Group
s: A -> G
y: Words
words_rec G s (nil ++ y) =
words_rec G s nil * words_rec G s y
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: list (A + A)
y: Words
IHxs: forall y : Words,
words_rec G s (xs ++ y) =
words_rec G s xs * words_rec G s y
words_rec G s ((x :: xs) ++ y) =
words_rec G s (x :: xs) * words_rec G s y
    -
A: Type
G: Group
s: A -> G
y: Words
words_rec G s (nil ++ y) =
words_rec G s nil * words_rec G s y symmetry; napply grp_unit_l.
    -
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: list (A + A)
y: Words
IHxs: forall y : Words,
words_rec G s (xs ++ y) =
words_rec G s xs * words_rec G s y
words_rec G s ((x :: xs) ++ y) =
words_rec G s (x :: xs) * words_rec G s y change ((?x :: ?xs) ++ y) with (x :: xs ++ y).
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: list (A + A)
y: Words
IHxs: forall y : Words,
words_rec G s (xs ++ y) =
words_rec G s xs * words_rec G s y
words_rec G s (x :: xs ++ y) =
words_rec G s (x :: xs) * words_rec G s y
      lhs napply words_rec_cons.
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: list (A + A)
y: Words
IHxs: forall y : Words,
words_rec G s (xs ++ y) =
words_rec G s xs * words_rec G s y
word_rec G s x * words_rec G s (xs ++ y) =
words_rec G s (x :: xs) * words_rec G s y
      lhs napply ap.
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: list (A + A)
y: Words
IHxs: forall y : Words,
words_rec G s (xs ++ y) =
words_rec G s xs * words_rec G s y
words_rec G s (xs ++ y) = ?Goal
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: list (A + A)
y: Words
IHxs: forall y : Words,
words_rec G s (xs ++ y) =
words_rec G s xs * words_rec G s y
word_rec G s x * ?Goal =
words_rec G s (x :: xs) * words_rec G s y
      1: napply IHxs.
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: list (A + A)
y: Words
IHxs: forall y : Words,
words_rec G s (xs ++ y) =
words_rec G s xs * words_rec G s y
word_rec G s x * (words_rec G s xs * words_rec G s y) =
words_rec G s (x :: xs) * words_rec G s y
      lhs napply grp_assoc.
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: list (A + A)
y: Words
IHxs: forall y : Words,
words_rec G s (xs ++ y) =
words_rec G s xs * words_rec G s y
word_rec G s x * words_rec G s xs * words_rec G s y =
words_rec G s (x :: xs) * words_rec G s y
      napply (ap (.* _)).
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: list (A + A)
y: Words
IHxs: forall y : Words,
words_rec G s (xs ++ y) =
words_rec G s xs * words_rec G s y
word_rec G s x * words_rec G s xs =
words_rec G s (x :: xs)
      symmetry.
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: list (A + A)
y: Words
IHxs: forall y : Words,
words_rec G s (xs ++ y) =
words_rec G s xs * words_rec G s y
words_rec G s (x :: xs) =
word_rec G s x * words_rec G s xs
      apply words_rec_cons.
  Defined.

  Lemma words_rec_coh (G : Group) (s : A -> G) (a : A + A) (b c : Words)
    : words_rec G s (map1 (b, a, c)) = words_rec G s (map2 (b, a, c)).
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s (map1 (b, a, c)) =
words_rec G s (map2 (b, a, c))
  Proof.
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s (map1 (b, a, c)) =
words_rec G s (map2 (b, a, c))
    unfold map1, map2.
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s (b ++ [a] ++ [a ^'] ++ c) =
words_rec G s (b ++ c)
    rhs napply (words_rec_pp G s).
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s (b ++ [a] ++ [a ^'] ++ c) =
words_rec G s b * words_rec G s c
    lhs napply words_rec_pp.
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s b * words_rec G s ([a] ++ [a ^'] ++ c) =
words_rec G s b * words_rec G s c
    napply (ap (_ *.)).
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s ([a] ++ [a ^'] ++ c) = words_rec G s c
    lhs napply words_rec_pp.
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s [a] * words_rec G s ([a ^'] ++ c) =
words_rec G s c
    lhs napply ap.
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s ([a ^'] ++ c) = ?Goal
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s [a] * ?Goal = words_rec G s c
    1: napply words_rec_pp.
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s [a] *
(words_rec G s [a ^'] * words_rec G s c) =
words_rec G s c
    lhs napply grp_assoc.
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s [a] * words_rec G s [a ^'] *
words_rec G s c = words_rec G s c
    rhs_V napply grp_unit_l.
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s [a] * words_rec G s [a ^'] *
words_rec G s c = 1 * words_rec G s c
    napply (ap (.* _)).
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s [a] * words_rec G s [a ^'] = 1
    destruct a; simpl.
A: Type
G: Group
s: A -> G
a: A
b, c: Words
s a * (s a)^ = 1
A: Type
G: Group
s: A -> G
a: A
b, c: Words
(s a)^ * s a = 1
    -
A: Type
G: Group
s: A -> G
a: A
b, c: Words
s a * (s a)^ = 1 napply grp_inv_r.
    -
A: Type
G: Group
s: A -> G
a: A
b, c: Words
(s a)^ * s a = 1 napply grp_inv_l.
  Defined.

  (** Given a group [G] we can construct a group homomorphism [FreeGroup A $-> G] if we have a map [A -> G]. *)
  Definition FreeGroup_rec {G : Group} (s : A -> G) : FreeGroup $-> G.
A: Type
G: Group
s: A -> G
FreeGroup $-> G
  Proof.
A: Type
G: Group
s: A -> G
FreeGroup $-> G
    snapply Build_GroupHomomorphism.
A: Type
G: Group
s: A -> G
FreeGroup -> G
A: Type
G: Group
s: A -> G
IsSemiGroupPreserving ?grp_homo_map
    {
A: Type
G: Group
s: A -> G
FreeGroup -> G rapply Trunc_rec.
A: Type
G: Group
s: A -> G
Coeq map1 map2 -> G
      srapply Coeq_rec.
A: Type
G: Group
s: A -> G
Words -> G
A: Type
G: Group
s: A -> G
forall b : Words * (A + A) * Words,
?coeq' (map1 b) = ?coeq' (map2 b)
      1: apply words_rec, s.
A: Type
G: Group
s: A -> G
forall b : Words * (A + A) * Words,
words_rec G s (map1 b) = words_rec G s (map2 b)
      intros [[b a] c].
A: Type
G: Group
s: A -> G
b: Words
a: (A + A)%type
c: Words
words_rec G s (map1 (b, a, c)) =
words_rec G s (map2 (b, a, c))
      apply words_rec_coh. }
A: Type
G: Group
s: A -> G
IsSemiGroupPreserving
  (Trunc_rec
     (Coeq_rec G (words_rec G s)
        (fun b0 : Words * (A + A) * Words =>
         (fun fst : Words * (A + A) =>
          (fun (b : Words) (a : A + A) (c : Words) =>
           words_rec_coh G s a b c) (Overture.fst fst)
            (snd fst)) (fst b0) (snd b0))))
    intros x y; strip_truncations.
A: Type
G: Group
s: A -> G
y, x: Coeq map1 map2
Trunc_rec
  (Coeq_rec G (words_rec G s)
     (fun b0 : Words * (A + A) * Words =>
      words_rec_coh G s (snd (fst b0)) (fst (fst b0))
        (snd b0))) (tr x * tr y) =
Trunc_rec
  (Coeq_rec G (words_rec G s)
     (fun b0 : Words * (A + A) * Words =>
      words_rec_coh G s (snd (fst b0)) (fst (fst b0))
        (snd b0))) (tr x) *
Trunc_rec
  (Coeq_rec G (words_rec G s)
     (fun b0 : Words * (A + A) * Words =>
      words_rec_coh G s (snd (fst b0)) (fst (fst b0))
        (snd b0))) (tr y)
    revert x; srapply Coeq_ind_hprop; intro x.
A: Type
G: Group
s: A -> G
y: Coeq map1 map2
x: Words
(fun x : Coeq map1 map2 =>
 Trunc_rec
   (Coeq_rec G (words_rec G s)
      (fun b0 : Words * (A + A) * Words =>
       words_rec_coh G s (snd (fst b0)) (fst (fst b0))
         (snd b0))) (tr x * tr y) =
 Trunc_rec
   (Coeq_rec G (words_rec G s)
      (fun b0 : Words * (A + A) * Words =>
       words_rec_coh G s (snd (fst b0)) (fst (fst b0))
         (snd b0))) (tr x) *
 Trunc_rec
   (Coeq_rec G (words_rec G s)
      (fun b0 : Words * (A + A) * Words =>
       words_rec_coh G s (snd (fst b0)) (fst (fst b0))
         (snd b0))) (tr y)) (coeq x)
    revert y; srapply Coeq_ind_hprop; intro y.
A: Type
G: Group
s: A -> G
x, y: Words
(fun x0 : Coeq map1 map2 =>
 (fun x : Coeq map1 map2 =>
  Trunc_rec
    (Coeq_rec G (words_rec G s)
       (fun b0 : Words * (A + A) * Words =>
        words_rec_coh G s (snd (fst b0))
          (fst (fst b0)) (snd b0))) (tr x * tr x0) =
  Trunc_rec
    (Coeq_rec G (words_rec G s)
       (fun b0 : Words * (A + A) * Words =>
        words_rec_coh G s (snd (fst b0))
          (fst (fst b0)) (snd b0))) (tr x) *
  Trunc_rec
    (Coeq_rec G (words_rec G s)
       (fun b0 : Words * (A + A) * Words =>
        words_rec_coh G s (snd (fst b0))
          (fst (fst b0)) (snd b0))) (tr x0)) (coeq x))
  (coeq y) 
    simpl.
A: Type
G: Group
s: A -> G
x, y: Words
words_rec G s (x ++ y) =
words_rec G s x * words_rec G s y
    apply words_rec_pp.
  Defined.

  Definition freegroup_in : A -> FreeGroup
    := freegroup_eta o (fun x => [ x ]) o inl.

  Definition FreeGroup_rec_beta {G : Group} (f : A -> G)
    : FreeGroup_rec f o freegroup_in == f
    := fun _ => idpath.

  Coercion freegroup_in : A >-> group_type.

  Definition FreeGroup_ind_hprop' (P : FreeGroup -> Type)
    `{forall x, IsHProp (P x)}
    (H1 : forall w, P (freegroup_eta w))
    : forall x, P x.
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: forall w : Words, P (freegroup_eta w)
forall x : FreeGroup, P x
  Proof.
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: forall w : Words, P (freegroup_eta w)
forall x : FreeGroup, P x
    rapply Trunc_ind.
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: forall w : Words, P (freegroup_eta w)
forall a : Coeq map1 map2, P (tr a)
    srapply Coeq_ind_hprop.
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: forall w : Words, P (freegroup_eta w)
forall a : Words,
(fun x : Coeq map1 map2 => P (tr x)) (coeq a)
    exact H1.
  Defined.

  Definition FreeGroup_ind_hprop (P : FreeGroup -> Type)
    `{forall x, IsHProp (P x)}
    (H1 : P mon_unit)
    (Hin : forall x, P (freegroup_in x))
    (Hop : forall x y, P x -> P y -> P (x^ * y))
    : forall x, P x.
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
forall x : FreeGroup, P x
  Proof.
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
forall x : FreeGroup, P x
    rapply FreeGroup_ind_hprop'.
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
forall w : Words, P (freegroup_eta w)
    intros w.
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
w: Words
P (freegroup_eta w)
    induction w as [|a w IHw].
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
P (freegroup_eta nil)
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: (A + A)%type
w: list (A + A)
IHw: P (freegroup_eta w)
P (freegroup_eta (a :: w))
    -
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
P (freegroup_eta nil) exact H1.
    -
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: (A + A)%type
w: list (A + A)
IHw: P (freegroup_eta w)
P (freegroup_eta (a :: w)) destruct a as [a|a].
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: A
w: list (A + A)
IHw: P (freegroup_eta w)
P (freegroup_eta (inl a :: w))
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: A
w: list (A + A)
IHw: P (freegroup_eta w)
P (freegroup_eta (inr a :: w))
      +
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: A
w: list (A + A)
IHw: P (freegroup_eta w)
P (freegroup_eta (inl a :: w)) change (P ((freegroup_in a) * freegroup_eta w)).
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: A
w: list (A + A)
IHw: P (freegroup_eta w)
P (a * freegroup_eta w)  
        rewrite <- (grp_inv_inv a).
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: A
w: list (A + A)
IHw: P (freegroup_eta w)
P ((a^)^ * freegroup_eta w)
        apply Hop.
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: A
w: list (A + A)
IHw: P (freegroup_eta w)
P a^
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: A
w: list (A + A)
IHw: P (freegroup_eta w)
P (freegroup_eta w)
        *
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: A
w: list (A + A)
IHw: P (freegroup_eta w)
P a^ rewrite <- grp_unit_r.
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: A
w: list (A + A)
IHw: P (freegroup_eta w)
P (a^ * 1)
          by apply Hop.
        *
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: A
w: list (A + A)
IHw: P (freegroup_eta w)
P (freegroup_eta w) assumption.
      +
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: A
w: list (A + A)
IHw: P (freegroup_eta w)
P (freegroup_eta (inr a :: w)) change (P ((freegroup_in a)^ * freegroup_eta w)).
A: Type
P: FreeGroup -> Type
H: forall x : FreeGroup, IsHProp (P x)
H1: P 1
Hin: forall x : A, P x
Hop: forall x y : FreeGroup, P x -> P y -> P (x^ * y)
a: A
w: list (A + A)
IHw: P (freegroup_eta w)
P (a^ * freegroup_eta w)
        by apply Hop.
  Defined.

  Definition FreeGroup_ind_homotopy {G : Group} {f f' : FreeGroup $-> G}
    (H : forall x, f (freegroup_in x) = f' (freegroup_in x))
    : f $== f'.
A: Type
G: Group
f, f': FreeGroup $-> G
H: forall x : A, f x = f' x
f $== f'
  Proof.
A: Type
G: Group
f, f': FreeGroup $-> G
H: forall x : A, f x = f' x
f $== f'
    rapply FreeGroup_ind_hprop.
A: Type
G: Group
f, f': FreeGroup $-> G
H: forall x : A, f x = f' x
f 1 = f' 1
A: Type
G: Group
f, f': FreeGroup $-> G
H: forall x : A, f x = f' x
forall x : A, f x = f' x
A: Type
G: Group
f, f': FreeGroup $-> G
H: forall x : A, f x = f' x
forall x y : FreeGroup,
f x = f' x -> f y = f' y -> f (x^ * y) = f' (x^ * y)
    -
A: Type
G: Group
f, f': FreeGroup $-> G
H: forall x : A, f x = f' x
f 1 = f' 1 exact (concat (grp_homo_unit f) (grp_homo_unit f')^).
    -
A: Type
G: Group
f, f': FreeGroup $-> G
H: forall x : A, f x = f' x
forall x : A, f x = f' x exact H.
    -
A: Type
G: Group
f, f': FreeGroup $-> G
H: forall x : A, f x = f' x
forall x y : FreeGroup,
f x = f' x -> f y = f' y -> f (x^ * y) = f' (x^ * y) intros x y p q.
A: Type
G: Group
f, f': FreeGroup $-> G
H: forall x : A, f x = f' x
x, y: FreeGroup
p: f x = f' x
q: f y = f' y
f (x^ * y) = f' (x^ * y) refine (grp_homo_op_agree f f' _ q).
A: Type
G: Group
f, f': FreeGroup $-> G
H: forall x : A, f x = f' x
x, y: FreeGroup
p: f x = f' x
q: f y = f' y
f x^ = f' x^
      lhs napply grp_homo_inv.
A: Type
G: Group
f, f': FreeGroup $-> G
H: forall x : A, f x = f' x
x, y: FreeGroup
p: f x = f' x
q: f y = f' y
(f x)^ = f' x^
      rhs napply grp_homo_inv.
A: Type
G: Group
f, f': FreeGroup $-> G
H: forall x : A, f x = f' x
x, y: FreeGroup
p: f x = f' x
q: f y = f' y
(f x)^ = (f' x)^
      exact (ap _ p).
  Defined.

  (** Now we need to prove that the free group satisfies the universal property of the free group. *)
  (** TODO: remove funext from here and universal property of free group *)
  #[export] Instance isfreegroupon_freegroup `{Funext}
    : IsFreeGroupOn A FreeGroup freegroup_in.
A: Type
H: Funext
IsFreeGroupOn A FreeGroup freegroup_in
  Proof.
A: Type
H: Funext
IsFreeGroupOn A FreeGroup freegroup_in
    intros G f.
A: Type
H: Funext
G: Group
f: A -> G
Contr
  (FactorsThroughFreeGroup A FreeGroup freegroup_in G
     f)
    snapply Build_Contr.
A: Type
H: Funext
G: Group
f: A -> G
FactorsThroughFreeGroup A FreeGroup freegroup_in G f
A: Type
H: Funext
G: Group
f: A -> G
forall
y : FactorsThroughFreeGroup A FreeGroup freegroup_in G
      f, ?center = y
    {
A: Type
H: Funext
G: Group
f: A -> G
FactorsThroughFreeGroup A FreeGroup freegroup_in G f srefine (_;_); simpl.
A: Type
H: Funext
G: Group
f: A -> G
GroupHomomorphism FreeGroup G
A: Type
H: Funext
G: Group
f: A -> G
(fun x : A => ?Goal x) == f
      1: apply FreeGroup_rec, f.
A: Type
H: Funext
G: Group
f: A -> G
(fun x : A => FreeGroup_rec f x) == f
      intro x; reflexivity. }
A: Type
H: Funext
G: Group
f: A -> G
forall
y : FactorsThroughFreeGroup A FreeGroup freegroup_in G
      f,
(FreeGroup_rec f : FreeGroup $-> G;
((fun x : A => 1%path)
 :
 (fun x : A => FreeGroup_rec f x) == f)
:
(fun f0 : FreeGroup $-> G => f0 o freegroup_in == f)
  (FreeGroup_rec f : FreeGroup $-> G)) = y
    intros [g h].
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g x) == f
(FreeGroup_rec f; fun x : A => 1%path) = (g; h)
    napply path_sigma_hprop; [ exact _ |].
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g x) == f
(FreeGroup_rec f; fun x : A => 1%path).1 = (g; h).1
    simpl.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g x) == f
FreeGroup_rec f = g
    apply equiv_path_grouphomomorphism.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g x) == f
FreeGroup_rec f == g
    symmetry.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g x) == f
g == FreeGroup_rec f
    snapply FreeGroup_ind_homotopy.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g x) == f
forall x : A, g x = FreeGroup_rec f x
    exact h.
  Defined.

  (** Typeclass search can already find this but we leave it here as a definition for reference. *)
  Definition isfreegroup_freegroup `{Funext} : IsFreeGroup FreeGroup := _.

End Reduction.

Arguments FreeGroup_rec {A G}.
Arguments FreeGroup_ind_homotopy {A G f f'}.
Arguments freegroup_eta {A}.
Arguments freegroup_in {A}.

(** Properties of free groups *)

(* Given a function on the generators, there is an induced group homomorphism from the free group. *)
Definition isfreegroupon_rec {S : Type} {F_S : Group}
  {i : S -> F_S} `{IsFreeGroupOn S F_S i}
  {G : Group} (f : S -> G) : F_S $-> G
  := (center (FactorsThroughFreeGroup S F_S i G f)).1.

(* The propositional computation rule for the recursor. *)
Definition isfreegroupon_rec_beta
  {S : Type} {F_S : Group} {i : S -> F_S} `{IsFreeGroupOn S F_S i}
  {G : Group} (f : S -> G)
  : isfreegroupon_rec f o i == f
  := (center (FactorsThroughFreeGroup S F_S i G f)).2.

(* Two homomorphisms from a free group are equal if they agree on the generators. *)
Definition path_homomorphism_from_free_group {S : Type}
  {F_S : Group} {i : S -> F_S} `{IsFreeGroupOn S F_S i}
  {G : Group} (f g : F_S $-> G) (K : f o i == g o i)
  : f = g.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
G: Group
f, g: F_S $-> G
K: f o i == g o i
f = g
Proof.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
G: Group
f, g: F_S $-> G
K: f o i == g o i
f = g
  (* By assumption, the type [FactorsThroughFreeGroup S F_S i G (g o i)] of factorizations of [g o i] through [i] is contractible.  Therefore the two elements we have are equal.  Therefore, their first components are equal. *)
  exact (path_contr (f; K) (g; fun x => idpath))..1.
Defined.

Instance isequiv_isfreegroupon_rec `{Funext} {S : Type}
  {F_S : Group} {i : S -> F_S} `{IsFreeGroupOn S F_S i} {G : Group}
  : IsEquiv (@isfreegroupon_rec S F_S i _ G).
H: Funext
S: Type
F_S: Group
i: S -> F_S
H0: IsFreeGroupOn S F_S i
G: Group
IsEquiv isfreegroupon_rec
Proof.
H: Funext
S: Type
F_S: Group
i: S -> F_S
H0: IsFreeGroupOn S F_S i
G: Group
IsEquiv isfreegroupon_rec
  apply (isequiv_adjointify isfreegroupon_rec (fun f => f o i)).
H: Funext
S: Type
F_S: Group
i: S -> F_S
H0: IsFreeGroupOn S F_S i
G: Group
(fun x : F_S $-> G =>
 isfreegroupon_rec (fun x0 : S => x (i x0))) == idmap
H: Funext
S: Type
F_S: Group
i: S -> F_S
H0: IsFreeGroupOn S F_S i
G: Group
(fun (x : S -> G) (x0 : S) =>
 isfreegroupon_rec x (i x0)) == idmap
  -
H: Funext
S: Type
F_S: Group
i: S -> F_S
H0: IsFreeGroupOn S F_S i
G: Group
(fun x : F_S $-> G =>
 isfreegroupon_rec (fun x0 : S => x (i x0))) == idmap intro f.
H: Funext
S: Type
F_S: Group
i: S -> F_S
H0: IsFreeGroupOn S F_S i
G: Group
f: F_S $-> G
isfreegroupon_rec (fun x : S => f (i x)) = f
    apply path_homomorphism_from_free_group.
H: Funext
S: Type
F_S: Group
i: S -> F_S
H0: IsFreeGroupOn S F_S i
G: Group
f: F_S $-> G
(fun x : S =>
 isfreegroupon_rec (fun x0 : S => f (i x0)) (i x)) ==
(fun x : S => f (i x))
    apply isfreegroupon_rec_beta.
  -
H: Funext
S: Type
F_S: Group
i: S -> F_S
H0: IsFreeGroupOn S F_S i
G: Group
(fun (x : S -> G) (x0 : S) =>
 isfreegroupon_rec x (i x0)) == idmap intro f.
H: Funext
S: Type
F_S: Group
i: S -> F_S
H0: IsFreeGroupOn S F_S i
G: Group
f: S -> G
(fun x : S => isfreegroupon_rec f (i x)) = f
    (* here we need [Funext]: *)
    apply path_arrow, isfreegroupon_rec_beta.
Defined.

(** The universal property of a free group. *)
Definition equiv_isfreegroupon_rec `{Funext} {G F : Group} {A : Type}
  {i : A -> F} `{IsFreeGroupOn A F i}
  : (A -> G) <~> (F $-> G) := Build_Equiv _ _ isfreegroupon_rec _.

(** The above theorem is true regardless of the implementation of free groups. This lets us state the more specific theorem about the canonical free groups. This can be read as [FreeGroup] is left adjoint to the forgetful functor [group_type]. *)
Definition equiv_freegroup_rec `{Funext} (G : Group) (A : Type)
  : (A -> G) <~> (FreeGroup A $-> G)
  := equiv_isfreegroupon_rec.

Instance ishprop_isfreegroupon `{Funext} (F : Group) (A : Type) (i : A -> F)
  : IsHProp (IsFreeGroupOn A F i).
H: Funext
F: Group
A: Type
i: A -> F
IsHProp (IsFreeGroupOn A F i)
Proof.
H: Funext
F: Group
A: Type
i: A -> F
IsHProp (IsFreeGroupOn A F i)
  unfold IsFreeGroupOn.
H: Funext
F: Group
A: Type
i: A -> F
IsHProp
  (forall (A0 : Group) (g : A -> A0),
   Contr (FactorsThroughFreeGroup A F i A0 g))
  exact istrunc_forall.
Defined.

(** Both ways of stating the universal property are equivalent. *)
Definition equiv_isfreegroupon_isequiv_precomp `{Funext}
  (F : Group) (A : Type) (i : A -> F)
  : IsFreeGroupOn A F i <~> forall G, IsEquiv (fun f : F $-> G => f o i).
H: Funext
F: Group
A: Type
i: A -> F
IsFreeGroupOn A F i <~>
(forall G : Group, IsEquiv (fun f : F $-> G => f o i))
Proof.
H: Funext
F: Group
A: Type
i: A -> F
IsFreeGroupOn A F i <~>
(forall G : Group, IsEquiv (fun f : F $-> G => f o i))
  srapply equiv_iff_hprop.
H: Funext
F: Group
A: Type
i: A -> F
IsFreeGroupOn A F i ->
forall G : Group, IsEquiv (fun f : F $-> G => f o i)
H: Funext
F: Group
A: Type
i: A -> F
(forall G : Group, IsEquiv (fun f : F $-> G => f o i)) ->
IsFreeGroupOn A F i
  1: intros ? ?; exact (equiv_isequiv (equiv_isfreegroupon_rec)^-1).
H: Funext
F: Group
A: Type
i: A -> F
(forall G : Group, IsEquiv (fun f : F $-> G => f o i)) ->
IsFreeGroupOn A F i
  intros k G g.
H: Funext
F: Group
A: Type
i: A -> F
k: forall G : Group,
IsEquiv (fun f : F $-> G => f o i)
G: Group
g: A -> G
Contr (FactorsThroughFreeGroup A F i G g)
  specialize (k G).
H: Funext
F: Group
A: Type
i: A -> F
G: Group
k: IsEquiv (fun f : F $-> G => f o i)
g: A -> G
Contr (FactorsThroughFreeGroup A F i G g)
  snapply contr_equiv'.
H: Funext
F: Group
A: Type
i: A -> F
G: Group
k: IsEquiv (fun f : F $-> G => f o i)
g: A -> G
Type
H: Funext
F: Group
A: Type
i: A -> F
G: Group
k: IsEquiv (fun f : F $-> G => f o i)
g: A -> G
?A <~> FactorsThroughFreeGroup A F i G g
H: Funext
F: Group
A: Type
i: A -> F
G: Group
k: IsEquiv (fun f : F $-> G => f o i)
g: A -> G
Contr ?A
  1: exact (hfiber (fun f x => grp_homo_map f (i x)) g).
H: Funext
F: Group
A: Type
i: A -> F
G: Group
k: IsEquiv (fun f : F $-> G => f o i)
g: A -> G
hfiber
  (fun (f : GroupHomomorphism F G) (x : A) => f (i x))
  g <~> FactorsThroughFreeGroup A F i G g
H: Funext
F: Group
A: Type
i: A -> F
G: Group
k: IsEquiv (fun f : F $-> G => f o i)
g: A -> G
Contr
  (hfiber
     (fun (f : GroupHomomorphism F G) (x : A) =>
      f (i x)) g)
  {
H: Funext
F: Group
A: Type
i: A -> F
G: Group
k: IsEquiv (fun f : F $-> G => f o i)
g: A -> G
hfiber
  (fun (f : GroupHomomorphism F G) (x : A) => f (i x))
  g <~> FactorsThroughFreeGroup A F i G g rapply equiv_functor_sigma_id.
H: Funext
F: Group
A: Type
i: A -> F
G: Group
k: IsEquiv (fun f : F $-> G => f o i)
g: A -> G
forall a : GroupHomomorphism F G,
(fun x : A => a (i x)) = g <~>
(fun x : A => a (i x)) == g
    intro y; symmetry.
H: Funext
F: Group
A: Type
i: A -> F
G: Group
k: IsEquiv (fun f : F $-> G => f o i)
g: A -> G
y: GroupHomomorphism F G
(fun x : A => y (i x)) == g <~>
(fun x : A => y (i x)) = g
    apply equiv_path_forall. }
H: Funext
F: Group
A: Type
i: A -> F
G: Group
k: IsEquiv (fun f : F $-> G => f o i)
g: A -> G
Contr
  (hfiber
     (fun (f : GroupHomomorphism F G) (x : A) =>
      f (i x)) g)
  exact _.
Defined.

(** ** Subgroups of free groups *)

(* We say that a group [G] is generated by a subtype [X] if the natural map from the subgroup generated by [X] to [G] is a surjection.  One could equivalently say [IsEquiv (subgroup_incl (subgroup_generated X))], [forall g, subgroup_generated X g], or [subgroup_generated X = maximal_subgroup], but the definition using surjectivity is convenient later. *)
Definition isgeneratedby (G : Group) (X : G -> Type)
  := IsSurjection (subgroup_incl (subgroup_generated X)).

Section FreeGroupGenerated.
  (* In this Section, we prove that the free group [F_S] on a type [S] is generated in the above sense by the image of [S].  We conclude that the inclusion map is an equivalence, and that the free group is isomorphic as a group to the subgroup. We show that the inclusion is a surjection by showing that it is split epi in the category of groups. *)

  Context {S : Type} {F_S : Group} {i : S -> F_S} `{IsFreeGroupOn S F_S i}.

  (* We define a group homomorphism from [F_S] to the subgroup [G] generated by [S] by sending a generator [s] to "itself".  This map will be a section of the inclusion map. *)
  Local Definition to_subgroup_generated
    : F_S $-> subgroup_generated (hfiber i).
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
F_S $-> subgroup_generated (hfiber i)
  Proof.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
F_S $-> subgroup_generated (hfiber i)
    apply isfreegroupon_rec.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
S -> subgroup_generated (hfiber i)
    intro s.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
s: S
subgroup_generated (hfiber i)
    snapply subgroup_generated_gen_incl.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
s: S
F_S
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
s: S
hfiber i ?g
    -
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
s: S
F_S exact (i s).
    -
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
s: S
hfiber i (i s) exact (s; idpath).
  Defined.

  (* We record the computation rule that [to_subgroup_generated] satisfies. *)
  Local Definition to_subgroup_generated_beta (s : S)
    : to_subgroup_generated (i s) = subgroup_generated_gen_incl (i s) (s; idpath)
    := isfreegroupon_rec_beta _ _.

  (* It follows that [to_subgroup_generated] is a section of the inclusion map from [G] to [F_S]. *)
  Local Definition is_retraction
    : (subgroup_incl _) $o to_subgroup_generated = grp_homo_id.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
subgroup_incl (subgroup_generated (hfiber i)) $o
to_subgroup_generated = grp_homo_id
  Proof.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
subgroup_incl (subgroup_generated (hfiber i)) $o
to_subgroup_generated = grp_homo_id
    apply path_homomorphism_from_free_group; cbn.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
(fun x : S => (to_subgroup_generated (i x)).1) ==
(fun x : S => i x)
    intro s.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
s: S
(to_subgroup_generated (i s)).1 = i s
    exact (ap pr1 (to_subgroup_generated_beta s)).
  Defined.

  (* It follows that the inclusion map is a surjection, i.e., that [F_S] is generated by the image of [S]. *)
  Definition isgenerated_isfreegroupon
    : isgeneratedby F_S (hfiber i).
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
isgeneratedby F_S (hfiber i)
  Proof.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
isgeneratedby F_S (hfiber i)
    snapply issurj_retr.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
F_S -> subgroup_generated (hfiber i)
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
forall y : F_S,
subgroup_incl (subgroup_generated (hfiber i)) (?s y) =
y
    -
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
F_S -> subgroup_generated (hfiber i) exact to_subgroup_generated.
    -
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
forall y : F_S,
subgroup_incl (subgroup_generated (hfiber i))
  (to_subgroup_generated y) = y apply ap10; cbn.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
(fun x : F_S => (to_subgroup_generated x).1) = idmap
      exact (ap grp_homo_map is_retraction).
  Defined.

  (* Therefore, the inclusion map is an equivalence, since it is known to be an embedding. *)
  Definition isequiv_subgroup_incl_freegroupon
    : IsEquiv (subgroup_incl (subgroup_generated (hfiber i))).
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
IsEquiv
  (subgroup_incl (subgroup_generated (hfiber i)))
  Proof.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
IsEquiv
  (subgroup_incl (subgroup_generated (hfiber i)))
    apply isequiv_surj_emb.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  (subgroup_incl (subgroup_generated (hfiber i)))
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
IsEmbedding
  (subgroup_incl (subgroup_generated (hfiber i)))
    -
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  (subgroup_incl (subgroup_generated (hfiber i))) exact isgenerated_isfreegroupon.
    -
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
IsEmbedding
  (subgroup_incl (subgroup_generated (hfiber i))) exact _.
  Defined.

  (* Therefore, the subgroup is isomorphic to the free group. *)
  Definition iso_subgroup_incl_freegroupon
    : GroupIsomorphism (subgroup_generated (hfiber i)) F_S.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
GroupIsomorphism (subgroup_generated (hfiber i)) F_S
  Proof.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
GroupIsomorphism (subgroup_generated (hfiber i)) F_S
    napply Build_GroupIsomorphism.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
IsEquiv ?Goal
    exact isequiv_subgroup_incl_freegroupon.
  Defined.

End FreeGroupGenerated.

(** ** Properties of recursor *)

Definition freegroup_rec_in {A : Type}
  : FreeGroup_rec freegroup_in $== Id (FreeGroup A).
A: Type
FreeGroup_rec freegroup_in $== Id (FreeGroup A)
Proof.
A: Type
FreeGroup_rec freegroup_in $== Id (FreeGroup A)
  by snapply FreeGroup_ind_homotopy.
Defined.

Definition freegroup_rec_compose {A : Type} {G H : Group}
  (f : A -> G) (k : G $-> H)
  : FreeGroup_rec (k o f) $== k $o FreeGroup_rec f.
A: Type
G, H: Group
f: A -> G
k: G $-> H
FreeGroup_rec (k o f) $== k $o FreeGroup_rec f
Proof.
A: Type
G, H: Group
f: A -> G
k: G $-> H
FreeGroup_rec (k o f) $== k $o FreeGroup_rec f
  by snapply FreeGroup_ind_homotopy; intros x.
Defined.

Definition freegroup_const {A : Type} {G : Group}
  : FreeGroup_rec (fun _ : A => 1) $== @grp_homo_const _ G.
A: Type
G: Group
FreeGroup_rec (fun _ : A => 1) $== grp_homo_const
Proof.
A: Type
G: Group
FreeGroup_rec (fun _ : A => 1) $== grp_homo_const
  by snapply FreeGroup_ind_homotopy.
Defined.

(** ** Functoriality *)

Instance is0functor_freegroup : Is0Functor FreeGroup.
Is0Functor FreeGroup
Proof.
Is0Functor FreeGroup
  snapply Build_Is0Functor.
forall a b : Type,
(a $-> b) -> FreeGroup a $-> FreeGroup b
  intros X Y f.
X, Y: Type
f: X $-> Y
FreeGroup X $-> FreeGroup Y
  snapply FreeGroup_rec.
X, Y: Type
f: X $-> Y
X -> FreeGroup Y
  exact (freegroup_in o f).
Defined.

Instance is1functor_freegroup : Is1Functor FreeGroup.
Is1Functor FreeGroup
Proof.
Is1Functor FreeGroup
  snapply Build_Is1Functor.
forall (a b : Type) (f g : a $-> b),
f $== g -> fmap FreeGroup f $== fmap FreeGroup g
forall a : Type,
fmap FreeGroup (Id a) $== Id (FreeGroup a)
forall (a b c : Type) (f : a $-> b) (g : b $-> c),
fmap FreeGroup (g $o f) $==
fmap FreeGroup g $o fmap FreeGroup f
  -
forall (a b : Type) (f g : a $-> b),
f $== g -> fmap FreeGroup f $== fmap FreeGroup g intros X Y f g p.
X, Y: Type
f, g: X $-> Y
p: f $== g
fmap FreeGroup f $== fmap FreeGroup g
    snapply FreeGroup_ind_homotopy.
X, Y: Type
f, g: X $-> Y
p: f $== g
forall x : X,
fmap FreeGroup f (freegroup_in x) =
fmap FreeGroup g (freegroup_in x)
    intros x.
X, Y: Type
f, g: X $-> Y
p: f $== g
x: X
fmap FreeGroup f (freegroup_in x) =
fmap FreeGroup g (freegroup_in x)
    exact (ap freegroup_in (p x)).
  -
forall a : Type,
fmap FreeGroup (Id a) $== Id (FreeGroup a) intro; exact freegroup_rec_in.
  -
forall (a b c : Type) (f : a $-> b) (g : b $-> c),
fmap FreeGroup (g $o f) $==
fmap FreeGroup g $o fmap FreeGroup f intros X Y Z f g.
X, Y, Z: Type
f: X $-> Y
g: Y $-> Z
fmap FreeGroup (g $o f) $==
fmap FreeGroup g $o fmap FreeGroup f
    by snapply FreeGroup_ind_homotopy.
Defined.