Require Import Basics Types Group Subgroup
  WildCat.Core 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}).

  (** 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 "x ^" := (change_sign x).

  (** 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.

  (** We can concatenate words using list concatenation *)
  Local Definition word_concat : Words -> Words -> Words := @app _.

  (** We introduce a local notation for word_concat. *)
  Local Infix "@" := word_concat.

  Local Definition word_concat_w_nil x : x @ nil = x.
A: Type
x: Words
x @ nil = x
  Proof.
A: Type
x: Words
x @ nil = x
    induction x; trivial.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: x @ nil = x
(a :: x)%list @ nil = (a :: x)%list
    cbn; f_ap.
  Defined.

  Local Definition word_concat_w_ww x y z : x @ (y @ z) = (x @ y) @ z.
A: Type
x, y, z: Words
x @ (y @ z) = (x @ y) @ z
  Proof.
A: Type
x, y, z: Words
x @ (y @ z) = (x @ y) @ z
    apply app_assoc.
  Defined.

  (** Singleton word *)
  Local Definition word_sing (x : A + A) : Words := (cons x nil).

  Local Notation "[ x ]" := (word_sing x).

  (** 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.

  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.

  (** 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 *)
  Global 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; snrapply 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
      snrapply 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]; cbn.
A: Type
x, y: Words
a: (A + A)%type
z: Words
freegroup_eta
  (x @
   (((y @ [a]) @
     [match a with
      | inl a => inr a
      | inr b => inl b
      end]) @ z)) = freegroup_eta (x @ (y @ z))
      refine (concat (ap _ _) _).
A: Type
x, y: Words
a: (A + A)%type
z: Words
x @
(((y @ [a]) @
  [match a with
   | inl a => inr a
   | inr b => inl b
   end]) @ z) = ?Goal
A: Type
x, y: Words
a: (A + A)%type
z: Words
freegroup_eta ?Goal = freegroup_eta (x @ (y @ z))
      {
A: Type
x, y: Words
a: (A + A)%type
z: Words
x @
(((y @ [a]) @
  [match a with
   | inl a => inr a
   | inr b => inl b
   end]) @ z) = ?Goal refine (concat (word_concat_w_ww _ _ _) _).
A: Type
x, y: Words
a: (A + A)%type
z: Words
(x @
 ((y @ [a]) @
  [match a with
   | inl a => inr a
   | inr b => inl b
   end])) @ z = ?Goal
        rapply (ap (fun t => t @ _)).
A: Type
x, y: Words
a: (A + A)%type
z: Words
x @
((y @ [a]) @
 [match a with
  | inl a => inr a
  | inr b => inl b
  end]) = ?Goal0
        refine (concat (word_concat_w_ww _ _ _) _).
A: Type
x, y: Words
a: (A + A)%type
z: Words
(x @ (y @ [a])) @
[match a with
 | inl a => inr a
 | inr b => inl b
 end] = ?Goal0
        rapply (ap (fun t => t @ _)).
A: Type
x, y: Words
a: (A + A)%type
z: Words
x @ (y @ [a]) = ?Goal0
        refine (word_concat_w_ww _ _ _). }
A: Type
x, y: Words
a: (A + A)%type
z: Words
freegroup_eta
  ((((x @ y) @ [a]) @
    [match a with
     | inl a => inr a
     | inr b => inl b
     end]) @ z) = freegroup_eta (x @ (y @ z))
      refine (concat _ (ap _ _^)).
A: Type
x, y: Words
a: (A + A)%type
z: Words
freegroup_eta
  ((((x @ y) @ [a]) @
    [match a with
     | inl a => inr a
     | inr b => inl b
     end]) @ z) = freegroup_eta ?Goal0
A: Type
x, y: Words
a: (A + A)%type
z: Words
x @ (y @ z) = ?Goal0
      2: apply word_concat_w_ww.
A: Type
x, y: Words
a: (A + A)%type
z: Words
freegroup_eta
  ((((x @ y) @ [a]) @
    [match a with
     | inl a => inr a
     | inr b => inl b
     end]) @ z) = freegroup_eta ((x @ y) @ z)
      apply freegroup_tau. }
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
         (word_concat_w_ww x
            (word_concat (word_concat y [a])
               [match a with
                | inl a0 => inr a0
                | inr b1 => inl b1
                end]) z @
          ap (fun t : Words => word_concat t z)
            (word_concat_w_ww x (word_concat y [a])
               [match ... with
                | ... => inr a0
                | ... => inl b1
                end] @
             ap (fun ... => word_concat t [...])
               (word_concat_w_ww x y [a]))) @
       (freegroup_tau (word_concat x y) a z @
        ap freegroup_eta (word_concat_w_ww x y z)^))%path
      :
      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
         (word_concat_w_ww x
            (word_concat (word_concat y [a])
               [match a with
                | inl a0 => inr a0
                | inr b1 => inl b1
                end]) z @
          ap (fun t : Words => word_concat t z)
            (word_concat_w_ww x (word_concat y [a])
               [match ... with
                | ... => inr a0
                | ... => inl b1
                end] @
             ap (fun ... => word_concat t [...])
               (word_concat_w_ww x y [a]))) @
       (freegroup_tau (word_concat x y) a z @
        ap freegroup_eta (word_concat_w_ww x y z)^))%path
      :
      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
      (word_concat_w_ww (map1 (c, b, d))
         (word_concat
            (word_concat (fst (fst b0)) [snd (fst b0)])
            [match snd (fst b0) with
             | inl a => inr a
             | inr b => inl b
             end]) (snd b0) @
       ap (fun t : Words => word_concat t (snd b0))
         (word_concat_w_ww (map1 (c, b, d))
            (word_concat (fst (fst b0)) [snd (fst b0)])
            [match snd (fst b0) with
             | inl a => inr a
             | inr b => inl b
             end] @
          ap
            (fun t : Words =>
             word_concat t
               [match snd (fst b0) with
                | inl a => inr a
                | inr b => inl b
                end])
            (word_concat_w_ww (map1 (c, b, d))
               (fst (fst b0)) [snd (fst b0)]))) @
    (freegroup_tau
       (word_concat (map1 (c, b, d)) (fst (fst b0)))
       (snd (fst b0)) (snd b0) @
     ap freegroup_eta
       (word_concat_w_ww (map1 (c, b, d))
          (fst (fst b0)) (snd b0))^))%path) y =
Coeq_rec freegroup_type
  (fun y : Words => freegroup_eta (map2 (c, b, d) @ y))
  (fun b0 : Words * (A + A) * Words =>
   (ap freegroup_eta
      (word_concat_w_ww (map2 (c, b, d))
         (word_concat
            (word_concat (fst (fst b0)) [snd (fst b0)])
            [match snd (fst b0) with
             | inl a => inr a
             | inr b => inl b
             end]) (snd b0) @
       ap (fun t : Words => word_concat t (snd b0))
         (word_concat_w_ww (map2 (c, b, d))
            (word_concat (fst (fst b0)) [snd (fst b0)])
            [match snd (fst b0) with
             | inl a => inr a
             | inr b => inl b
             end] @
          ap
            (fun t : Words =>
             word_concat t
               [match snd (fst b0) with
                | inl a => inr a
                | inr b => inl b
                end])
            (word_concat_w_ww (map2 (c, b, d))
               (fst (fst b0)) [snd (fst b0)]))) @
    (freegroup_tau
       (word_concat (map2 (c, b, d)) (fst (fst b0)))
       (snd (fst b0)) (snd b0) @
     ap freegroup_eta
       (word_concat_w_ww (map2 (c, b, d))
          (fst (fst b0)) (snd b0))^))%path) y
    simpl.
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
      (word_concat_w_ww (map1 (c, b, d))
         (word_concat
            (word_concat (fst (fst b0)) [snd (fst b0)])
            [match snd (fst b0) with
             | inl a => inr a
             | inr b => inl b
             end]) (snd b0) @
       ap (fun t : Words => word_concat t (snd b0))
         (word_concat_w_ww (map1 (c, b, d))
            (word_concat (fst (fst b0)) [snd (fst b0)])
            [match snd (fst b0) with
             | inl a => inr a
             | inr b => inl b
             end] @
          ap
            (fun t : Words =>
             word_concat t
               [match snd (fst b0) with
                | inl a => inr a
                | inr b => inl b
                end])
            (word_concat_w_ww (map1 (c, b, d))
               (fst (fst b0)) [snd (fst b0)]))) @
    (freegroup_tau
       (word_concat (map1 (c, b, d)) (fst (fst b0)))
       (snd (fst b0)) (snd b0) @
     ap freegroup_eta
       (word_concat_w_ww (map1 (c, b, d))
          (fst (fst b0)) (snd b0))^))%path) y =
Coeq_rec freegroup_type
  (fun y : Words => freegroup_eta (map2 (c, b, d) @ y))
  (fun b0 : Words * (A + A) * Words =>
   (ap freegroup_eta
      (word_concat_w_ww (map2 (c, b, d))
         (word_concat
            (word_concat (fst (fst b0)) [snd (fst b0)])
            [match snd (fst b0) with
             | inl a => inr a
             | inr b => inl b
             end]) (snd b0) @
       ap (fun t : Words => word_concat t (snd b0))
         (word_concat_w_ww (map2 (c, b, d))
            (word_concat (fst (fst b0)) [snd (fst b0)])
            [match snd (fst b0) with
             | inl a => inr a
             | inr b => inl b
             end] @
          ap
            (fun t : Words =>
             word_concat t
               [match snd (fst b0) with
                | inl a => inr a
                | inr b => inl b
                end])
            (word_concat_w_ww (map2 (c, b, d))
               (fst (fst b0)) [snd (fst b0)]))) @
    (freegroup_tau
       (word_concat (map2 (c, b, d)) (fst (fst b0)))
       (snd (fst b0)) (snd b0) @
     ap freegroup_eta
       (word_concat_w_ww (map2 (c, b, d))
          (fst (fst b0)) (snd b0))^))%path) 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
      (word_concat_w_ww (map1 (c, b, d))
         (word_concat
            (word_concat (fst (fst b0)) [snd (fst b0)])
            [match snd (fst b0) with
             | inl a => inr a
             | inr b => inl b
             end]) (snd b0) @
       ap (fun t : Words => word_concat t (snd b0))
         (word_concat_w_ww (map1 (c, b, d))
            (word_concat (fst (fst b0)) [snd (fst b0)])
            [match snd (fst b0) with
             | inl a => inr a
             | inr b => inl b
             end] @
          ap
            (fun t : Words =>
             word_concat t
               [match snd (fst b0) with
                | inl a => inr a
                | inr b => inl b
                end])
            (word_concat_w_ww (map1 (c, b, d))
               (fst (fst b0)) [snd (fst b0)]))) @
    (freegroup_tau
       (word_concat (map1 (c, b, d)) (fst (fst b0)))
       (snd (fst b0)) (snd b0) @
     ap freegroup_eta
       (word_concat_w_ww (map1 (c, b, d))
          (fst (fst b0)) (snd b0))^))%path) y =
Coeq_rec freegroup_type
  (fun y0 : Words =>
   freegroup_eta (map2 (c, b, d) @ y0))
  (fun b0 : Words * (A + A) * Words =>
   (ap freegroup_eta
      (word_concat_w_ww (map2 (c, b, d))
         (word_concat
            (word_concat (fst (fst b0)) [snd (fst b0)])
            [match snd (fst b0) with
             | inl a => inr a
             | inr b => inl b
             end]) (snd b0) @
       ap (fun t : Words => word_concat t (snd b0))
         (word_concat_w_ww (map2 (c, b, d))
            (word_concat (fst (fst b0)) [snd (fst b0)])
            [match snd (fst b0) with
             | inl a => inr a
             | inr b => inl b
             end] @
          ap
            (fun t : Words =>
             word_concat t
               [match snd (fst b0) with
                | inl a => inr a
                | inr b => inl b
                end])
            (word_concat_w_ww (map2 (c, b, d))
               (fst (fst b0)) [snd (fst b0)]))) @
    (freegroup_tau
       (word_concat (map2 (c, b, d)) (fst (fst b0)))
       (snd (fst b0)) (snd b0) @
     ap freegroup_eta
       (word_concat_w_ww (map2 (c, b, d))
          (fst (fst b0)) (snd b0))^))%path) y
    snrapply Coeq_ind.
A: Type
c: Words
b: (A + A)%type
d: Words
forall a : Words,
(fun w : 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
       (word_concat_w_ww (map1 (c, b, d))
          (word_concat
             (word_concat (fst (fst b0))
                [snd (fst b0)])
             [match snd (fst b0) with
              | inl a0 => inr a0
              | inr b => inl b
              end]) (snd b0) @
        ap (fun t : Words => word_concat t (snd b0))
          (word_concat_w_ww (map1 (c, b, d))
             (word_concat (fst (fst b0))
                [snd (fst b0)])
             [match snd (fst b0) with
              | inl a0 => inr a0
              | inr b => inl b
              end] @
           ap
             (fun t : Words =>
              word_concat t
                [match snd (fst b0) with
                 | inl a0 => inr a0
                 | inr b => inl b
                 end])
             (word_concat_w_ww (map1 (c, b, d))
                (fst (fst b0)) [snd (fst b0)]))) @
     (freegroup_tau
        (word_concat (map1 (c, b, d)) (fst (fst b0)))
        (snd (fst b0)) (snd b0) @
      ap freegroup_eta
        (word_concat_w_ww (map1 (c, b, d))
           (fst (fst b0)) (snd b0))^))%path) w =
 Coeq_rec freegroup_type
   (fun y : Words =>
    freegroup_eta (map2 (c, b, d) @ y))
   (fun b0 : Words * (A + A) * Words =>
    (ap freegroup_eta
       (word_concat_w_ww (map2 (c, b, d))
          (word_concat
             (word_concat (fst (fst b0))
                [snd (fst b0)])
             [match snd (fst b0) with
              | inl a0 => inr a0
              | inr b => inl b
              end]) (snd b0) @
        ap (fun t : Words => word_concat t (snd b0))
          (word_concat_w_ww (map2 (c, b, d))
             (word_concat (fst (fst b0))
                [snd (fst b0)])
             [match snd (fst b0) with
              | inl a0 => inr a0
              | inr b => inl b
              end] @
           ap
             (fun t : Words =>
              word_concat t
                [match snd (fst b0) with
                 | inl a0 => inr a0
                 | inr b => inl b
                 end])
             (word_concat_w_ww (map2 (c, b, d))
                (fst (fst b0)) [snd (fst b0)]))) @
     (freegroup_tau
        (word_concat (map2 (c, b, d)) (fst (fst b0)))
        (snd (fst b0)) (snd b0) @
      ap freegroup_eta
        (word_concat_w_ww (map2 (c, b, d))
           (fst (fst b0)) (snd b0))^))%path) w)
  (coeq a)
A: Type
c: Words
b: (A + A)%type
d: Words
forall b0 : Words * (A + A) * Words,
transport
  (fun w : Coeq map1 map2 =>
   Coeq_rec freegroup_type
     (fun y : Words =>
      freegroup_eta (map1 (c, b, d) @ y))
     (fun b1 : Words * (A + A) * Words =>
      (ap freegroup_eta
         (word_concat_w_ww (map1 (c, b, d))
            (word_concat
               (word_concat (fst (fst b1))
                  [snd (fst b1)])
               [match snd (fst b1) with
                | inl a => inr a
                | inr b => inl b
                end]) (snd b1) @
          ap (fun t : Words => word_concat t (snd b1))
            (word_concat_w_ww (map1 (c, b, d))
               (word_concat (fst (fst b1))
                  [snd (fst b1)])
               [match snd (fst b1) with
                | inl a => inr a
                | inr b => inl b
                end] @
             ap
               (fun t : Words =>
                word_concat t
                  [match snd (...) with
                   | inl a => inr a
                   | inr b => inl b
                   end])
               (word_concat_w_ww (map1 (c, b, d))
                  (fst (fst b1)) [snd (fst b1)]))) @
       (freegroup_tau
          (word_concat (map1 (c, b, d)) (fst (fst b1)))
          (snd (fst b1)) (snd b1) @
        ap freegroup_eta
          (word_concat_w_ww (map1 (c, b, d))
             (fst (fst b1)) (snd b1))^))%path) w =
   Coeq_rec freegroup_type
     (fun y : Words =>
      freegroup_eta (map2 (c, b, d) @ y))
     (fun b1 : Words * (A + A) * Words =>
      (ap freegroup_eta
         (word_concat_w_ww (map2 (c, b, d))
            (word_concat
               (word_concat (fst (fst b1))
                  [snd (fst b1)])
               [match snd (fst b1) with
                | inl a => inr a
                | inr b => inl b
                end]) (snd b1) @
          ap (fun t : Words => word_concat t (snd b1))
            (word_concat_w_ww (map2 (c, b, d))
               (word_concat (fst (fst b1))
                  [snd (fst b1)])
               [match snd (fst b1) with
                | inl a => inr a
                | inr b => inl b
                end] @
             ap
               (fun t : Words =>
                word_concat t
                  [match snd (...) with
                   | inl a => inr a
                   | inr b => inl b
                   end])
               (word_concat_w_ww (map2 (c, b, d))
                  (fst (fst b1)) [snd (fst b1)]))) @
       (freegroup_tau
          (word_concat (map2 (c, b, d)) (fst (fst b1)))
          (snd (fst b1)) (snd b1) @
        ap freegroup_eta
          (word_concat_w_ww (map2 (c, b, d))
             (fst (fst b1)) (snd b1))^))%path) w)
  (cglue b0) (?coeq' (map1 b0)) = ?coeq' (map2 b0)
    {
A: Type
c: Words
b: (A + A)%type
d: Words
forall a : Words,
(fun w : 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
       (word_concat_w_ww (map1 (c, b, d))
          (word_concat
             (word_concat (fst (fst b0))
                [snd (fst b0)])
             [match snd (fst b0) with
              | inl a0 => inr a0
              | inr b => inl b
              end]) (snd b0) @
        ap (fun t : Words => word_concat t (snd b0))
          (word_concat_w_ww (map1 (c, b, d))
             (word_concat (fst (fst b0))
                [snd (fst b0)])
             [match snd (fst b0) with
              | inl a0 => inr a0
              | inr b => inl b
              end] @
           ap
             (fun t : Words =>
              word_concat t
                [match snd (fst b0) with
                 | inl a0 => inr a0
                 | inr b => inl b
                 end])
             (word_concat_w_ww (map1 (c, b, d))
                (fst (fst b0)) [snd (fst b0)]))) @
     (freegroup_tau
        (word_concat (map1 (c, b, d)) (fst (fst b0)))
        (snd (fst b0)) (snd b0) @
      ap freegroup_eta
        (word_concat_w_ww (map1 (c, b, d))
           (fst (fst b0)) (snd b0))^))%path) w =
 Coeq_rec freegroup_type
   (fun y : Words =>
    freegroup_eta (map2 (c, b, d) @ y))
   (fun b0 : Words * (A + A) * Words =>
    (ap freegroup_eta
       (word_concat_w_ww (map2 (c, b, d))
          (word_concat
             (word_concat (fst (fst b0))
                [snd (fst b0)])
             [match snd (fst b0) with
              | inl a0 => inr a0
              | inr b => inl b
              end]) (snd b0) @
        ap (fun t : Words => word_concat t (snd b0))
          (word_concat_w_ww (map2 (c, b, d))
             (word_concat (fst (fst b0))
                [snd (fst b0)])
             [match snd (fst b0) with
              | inl a0 => inr a0
              | inr b => inl b
              end] @
           ap
             (fun t : Words =>
              word_concat t
                [match snd (fst b0) with
                 | inl a0 => inr a0
                 | inr b => inl b
                 end])
             (word_concat_w_ww (map2 (c, b, d))
                (fst (fst b0)) [snd (fst b0)]))) @
     (freegroup_tau
        (word_concat (map2 (c, b, d)) (fst (fst b0)))
        (snd (fst b0)) (snd b0) @
      ap freegroup_eta
        (word_concat_w_ww (map2 (c, b, d))
           (fst (fst b0)) (snd b0))^))%path) w)
  (coeq a) simpl.
A: Type
c: Words
b: (A + A)%type
d: Words
forall a : Words,
freegroup_eta (map1 (c, b, d) @ a) =
freegroup_eta (map2 (c, b, d) @ a)
      intro a.
A: Type
c: Words
b: (A + A)%type
d, a: Words
freegroup_eta (map1 (c, b, d) @ a) =
freegroup_eta (map2 (c, b, d) @ a)
      rewrite <- word_concat_w_ww.
A: Type
c: Words
b: (A + A)%type
d, a: Words
freegroup_eta (((c @ [b]) @ [b^]) @ (d @ a)) =
freegroup_eta (map2 (c, b, d) @ a)
      rewrite <- (word_concat_w_ww _ _ a).
A: Type
c: Words
b: (A + A)%type
d, a: Words
freegroup_eta (((c @ [b]) @ [b^]) @ (d @ a)) =
freegroup_eta (c @ (d @ a))
      rapply (freegroup_tau c b (d @ a)). }
A: Type
c: Words
b: (A + A)%type
d: Words
forall b0 : Words * (A + A) * Words,
transport
  (fun w : Coeq map1 map2 =>
   Coeq_rec freegroup_type
     (fun y : Words =>
      freegroup_eta (map1 (c, b, d) @ y))
     (fun b1 : Words * (A + A) * Words =>
      (ap freegroup_eta
         (word_concat_w_ww (map1 (c, b, d))
            (word_concat
               (word_concat (fst (fst b1))
                  [snd (fst b1)])
               [match snd (fst b1) with
                | inl a => inr a
                | inr b => inl b
                end]) (snd b1) @
          ap (fun t : Words => word_concat t (snd b1))
            (word_concat_w_ww (map1 (c, b, d))
               (word_concat (fst (fst b1))
                  [snd (fst b1)])
               [match snd (fst b1) with
                | inl a => inr a
                | inr b => inl b
                end] @
             ap
               (fun t : Words =>
                word_concat t
                  [match snd (...) with
                   | inl a => inr a
                   | inr b => inl b
                   end])
               (word_concat_w_ww (map1 (c, b, d))
                  (fst (fst b1)) [snd (fst b1)]))) @
       (freegroup_tau
          (word_concat (map1 (c, b, d)) (fst (fst b1)))
          (snd (fst b1)) (snd b1) @
        ap freegroup_eta
          (word_concat_w_ww (map1 (c, b, d))
             (fst (fst b1)) (snd b1))^))%path) w =
   Coeq_rec freegroup_type
     (fun y : Words =>
      freegroup_eta (map2 (c, b, d) @ y))
     (fun b1 : Words * (A + A) * Words =>
      (ap freegroup_eta
         (word_concat_w_ww (map2 (c, b, d))
            (word_concat
               (word_concat (fst (fst b1))
                  [snd (fst b1)])
               [match snd (fst b1) with
                | inl a => inr a
                | inr b => inl b
                end]) (snd b1) @
          ap (fun t : Words => word_concat t (snd b1))
            (word_concat_w_ww (map2 (c, b, d))
               (word_concat (fst (fst b1))
                  [snd (fst b1)])
               [match snd (fst b1) with
                | inl a => inr a
                | inr b => inl b
                end] @
             ap
               (fun t : Words =>
                word_concat t
                  [match snd (...) with
                   | inl a => inr a
                   | inr b => inl b
                   end])
               (word_concat_w_ww (map2 (c, b, d))
                  (fst (fst b1)) [snd (fst b1)]))) @
       (freegroup_tau
          (word_concat (map2 (c, b, d)) (fst (fst b1)))
          (snd (fst b1)) (snd b1) @
        ap freegroup_eta
          (word_concat_w_ww (map2 (c, b, d))
             (fst (fst b1)) (snd b1))^))%path) w)
  (cglue b0)
  (((fun a : Words =>
     internal_paths_rew
       (fun w : Words =>
        freegroup_eta w =
        freegroup_eta (map2 (c, b, d) @ a))
       (internal_paths_rew
          (fun w : Words =>
           freegroup_eta
             (((c @ [b]) @ [b^]) @ (d @ a)) =
           freegroup_eta w)
          (freegroup_tau c b (d @ a))
          (word_concat_w_ww c d a))
       (word_concat_w_ww ((c @ [b]) @ [b^]) d a))
    :
    forall a : Words,
    (fun w : Coeq map1 map2 =>
     Coeq_rec freegroup_type
       (fun y : Words =>
        freegroup_eta (map1 (c, b, d) @ y))
       (fun b1 : Words * (A + A) * Words =>
        (ap freegroup_eta
           (word_concat_w_ww (map1 (c, b, d))
              (word_concat
                 (word_concat (fst ...) [snd (...)])
                 [match ... with
                  | inl a0 => inr a0
                  | inr b => inl b
                  end]) (snd b1) @
            ap
              (fun t : Words => word_concat t (snd b1))
              (word_concat_w_ww (map1 (c, b, d))
                 (word_concat (...) [snd ...])
                 [match ... with
                  | ... => inr a0
                  | ... => inl b
                  end] @
               ap (fun ... => word_concat t [...])
                 (word_concat_w_ww (...) (...)
                    [snd ...]))) @
         (freegroup_tau
            (word_concat (map1 (c, b, d))
               (fst (fst b1))) (snd (fst b1)) (snd b1) @
          ap freegroup_eta
            (word_concat_w_ww (map1 (c, b, d))
               (fst (fst b1)) (snd b1))^))%path) w =
     Coeq_rec freegroup_type
       (fun y : Words =>
        freegroup_eta (map2 (c, b, d) @ y))
       (fun b1 : Words * (A + A) * Words =>
        (ap freegroup_eta
           (word_concat_w_ww (map2 (c, b, d))
              (word_concat
                 (word_concat (fst ...) [snd (...)])
                 [match ... with
                  | inl a0 => inr a0
                  | inr b => inl b
                  end]) (snd b1) @
            ap
              (fun t : Words => word_concat t (snd b1))
              (word_concat_w_ww (map2 (c, b, d))
                 (word_concat (...) [snd ...])
                 [match ... with
                  | ... => inr a0
                  | ... => inl b
                  end] @
               ap (fun ... => word_concat t [...])
                 (word_concat_w_ww (...) (...)
                    [snd ...]))) @
         (freegroup_tau
            (word_concat (map2 (c, b, d))
               (fst (fst b1))) (snd (fst b1)) (snd b1) @
          ap freegroup_eta
            (word_concat_w_ww (map2 (c, b, d))
               (fst (fst b1)) (snd b1))^))%path) w)
      (coeq a)) (map1 b0)) =
((fun a : Words =>
  internal_paths_rew
    (fun w : Words =>
     freegroup_eta w =
     freegroup_eta (map2 (c, b, d) @ a))
    (internal_paths_rew
       (fun w : Words =>
        freegroup_eta (((c @ [b]) @ [b^]) @ (d @ a)) =
        freegroup_eta w) (freegroup_tau c b (d @ a))
       (word_concat_w_ww c d a))
    (word_concat_w_ww ((c @ [b]) @ [b^]) d a))
 :
 forall a : Words,
 (fun w : Coeq map1 map2 =>
  Coeq_rec freegroup_type
    (fun y : Words =>
     freegroup_eta (map1 (c, b, d) @ y))
    (fun b1 : Words * (A + A) * Words =>
     (ap freegroup_eta
        (word_concat_w_ww (map1 (c, b, d))
           (word_concat
              (word_concat (fst (fst b1))
                 [snd (fst b1)])
              [match snd (...) with
               | inl a0 => inr a0
               | inr b => inl b
               end]) (snd b1) @
         ap (fun t : Words => word_concat t (snd b1))
           (word_concat_w_ww (map1 (c, b, d))
              (word_concat (fst (...)) [snd (fst b1)])
              [match snd ... with
               | inl a0 => inr a0
               | inr b => inl b
               end] @
            ap
              (fun t : Words =>
               word_concat t
                 [match ... with
                  | ... ...
                  | ... ...
                  end])
              (word_concat_w_ww (map1 (c, b, d))
                 (fst (...)) [snd (fst b1)]))) @
      (freegroup_tau
         (word_concat (map1 (c, b, d)) (fst (fst b1)))
         (snd (fst b1)) (snd b1) @
       ap freegroup_eta
         (word_concat_w_ww (map1 (c, b, d))
            (fst (fst b1)) (snd b1))^))%path) w =
  Coeq_rec freegroup_type
    (fun y : Words =>
     freegroup_eta (map2 (c, b, d) @ y))
    (fun b1 : Words * (A + A) * Words =>
     (ap freegroup_eta
        (word_concat_w_ww (map2 (c, b, d))
           (word_concat
              (word_concat (fst (fst b1))
                 [snd (fst b1)])
              [match snd (...) with
               | inl a0 => inr a0
               | inr b => inl b
               end]) (snd b1) @
         ap (fun t : Words => word_concat t (snd b1))
           (word_concat_w_ww (map2 (c, b, d))
              (word_concat (fst (...)) [snd (fst b1)])
              [match snd ... with
               | inl a0 => inr a0
               | inr b => inl b
               end] @
            ap
              (fun t : Words =>
               word_concat t
                 [match ... with
                  | ... ...
                  | ... ...
                  end])
              (word_concat_w_ww (map2 (c, b, d))
                 (fst (...)) [snd (fst b1)]))) @
      (freegroup_tau
         (word_concat (map2 (c, b, d)) (fst (fst b1)))
         (snd (fst b1)) (snd b1) @
       ap freegroup_eta
         (word_concat_w_ww (map2 (c, b, d))
            (fst (fst b1)) (snd b1))^))%path) w)
   (coeq a)) (map2 b0)
    intro; rapply path_ishprop.
  Defined.

  (** The unit of the free group is the empty word *)
  Global Instance monunit_freegroup_type : MonUnit freegroup_type.
A: Type
MonUnit freegroup_type
  Proof.
A: Type
MonUnit freegroup_type
    apply freegroup_eta.
A: Type
Words
    exact nil.
  Defined.

  (** We can change the sign of all the elements in a word and reverse the order. This will be the inversion in the group *)
  Fixpoint word_change_sign (x : Words) : Words.
A: Type
word_change_sign: Words -> Words
x: Words
Words
  Proof.
A: Type
word_change_sign: Words -> Words
x: Words
Words
    destruct x as [|x xs].
A: Type
word_change_sign: Words -> Words
Words
A: Type
word_change_sign: Words -> Words
x: (A + A)%type
xs: list (A + A)
Words
    1: exact nil.
A: Type
word_change_sign: Words -> Words
x: (A + A)%type
xs: list (A + A)
Words
    exact (word_change_sign xs @ [change_sign x]).
  Defined.

  (** 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
    induction x.
A: Type
y: Words
word_change_sign (nil @ y) =
word_change_sign y @ word_change_sign nil
A: Type
a: (A + A)%type
x: list (A + A)
y: Words
IHx: word_change_sign (x @ y) = word_change_sign y @ word_change_sign x
word_change_sign ((a :: x)%list @ y) =
word_change_sign y @ word_change_sign (a :: x)%list
    {
A: Type
y: Words
word_change_sign (nil @ y) =
word_change_sign y @ word_change_sign nil symmetry.
A: Type
y: Words
word_change_sign y @ word_change_sign nil =
word_change_sign (nil @ y)
      apply word_concat_w_nil. }
A: Type
a: (A + A)%type
x: list (A + A)
y: Words
IHx: word_change_sign (x @ y) = word_change_sign y @ word_change_sign x
word_change_sign ((a :: x)%list @ y) =
word_change_sign y @ word_change_sign (a :: x)%list
    simpl.
A: Type
a: (A + A)%type
x: list (A + A)
y: Words
IHx: word_change_sign (x @ y) = word_change_sign y @ word_change_sign x
word_change_sign (x @ y) @ [a^] =
word_change_sign y @ (word_change_sign x @ [a^])
    refine (concat _ (inverse (word_concat_w_ww _ _ _))).
A: Type
a: (A + A)%type
x: list (A + A)
y: Words
IHx: word_change_sign (x @ y) = word_change_sign y @ word_change_sign x
word_change_sign (x @ y) @ [a^] =
(word_change_sign y @ word_change_sign x) @ [a^]
    f_ap.
  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
    induction x.
A: Type
word_change_sign (word_change_sign nil) = nil
A: Type
a: (A + A)%type
x: list (A + A)
IHx: word_change_sign (word_change_sign x) = x
word_change_sign (word_change_sign (a :: x)%list) =
(a :: x)%list
    1: reflexivity.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: word_change_sign (word_change_sign x) = x
word_change_sign (word_change_sign (a :: x)%list) =
(a :: x)%list
    simpl.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: word_change_sign (word_change_sign x) = x
word_change_sign (word_change_sign x @ [a^]) =
(a :: x)%list
    rewrite word_change_sign_ww.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: word_change_sign (word_change_sign x) = x
word_change_sign [a^] @
word_change_sign (word_change_sign x) = (a :: x)%list
    cbn; f_ap.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: word_change_sign (word_change_sign x) = x
match
  match a with
  | inl a => inr a
  | inr b => inl b
  end
with
| inl a => inr a
| inr b => inl b
end = 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) = mon_unit
  Proof.
A: Type
x: Words
freegroup_eta (word_change_sign x @ x) = mon_unit
    induction x.
A: Type
freegroup_eta (word_change_sign nil @ nil) = mon_unit
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x @ x) = mon_unit
freegroup_eta
  (word_change_sign (a :: x)%list @ (a :: x)%list) =
mon_unit
    1: reflexivity.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x @ x) = mon_unit
freegroup_eta
  (word_change_sign (a :: x)%list @ (a :: x)%list) =
mon_unit
    simpl.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x @ x) = mon_unit
freegroup_eta
  ((word_change_sign x @ [a^]) @ (a :: x)%list) =
mon_unit
    set (a' := a^).
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x @ x) = mon_unit
a':= a^: A + A
freegroup_eta
  ((word_change_sign x @ [a']) @ (a :: x)%list) =
mon_unit
    rewrite <- (change_sign_inv a).
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x @ x) = mon_unit
a':= a^: A + A
freegroup_eta
  ((word_change_sign x @ [a']) @ ((a^)^ :: x)%list) =
mon_unit
    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) = mon_unit
a':= a^: A + A
freegroup_eta
  ((word_change_sign x @ [a']) @ ([a'^] @ x)) =
mon_unit
    rewrite word_concat_w_ww.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x @ x) = mon_unit
a':= a^: A + A
freegroup_eta
  (((word_change_sign x @ [a']) @ [a'^]) @ x) =
mon_unit
    rewrite freegroup_tau.
A: Type
a: (A + A)%type
x: list (A + A)
IHx: freegroup_eta (word_change_sign x @ x) = mon_unit
a':= a^: A + A
freegroup_eta (word_change_sign x @ x) = mon_unit
    apply 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: Words
freegroup_eta (x @ word_change_sign x) = mon_unit
  Proof.
A: Type
x: Words
freegroup_eta (x @ word_change_sign x) = mon_unit
    set (x' := word_change_sign x).
A: Type
x: Words
x':= word_change_sign x: Words
freegroup_eta (x @ x') = mon_unit
    rewrite <- (word_change_sign_inv x).
A: Type
x: Words
x':= word_change_sign x: Words
freegroup_eta
  (word_change_sign (word_change_sign x) @ x') =
mon_unit
    change (freegroup_eta (word_change_sign x' @ x') = mon_unit).
A: Type
x: Words
x':= word_change_sign x: Words
freegroup_eta (word_change_sign x' @ x') = mon_unit
    apply word_concat_Vw.
  Defined.

  (** Negation is 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. *)
  Global Instance negate_freegroup_type : Negate freegroup_type.
A: Type
Negate freegroup_type
  Proof.
A: Type
Negate 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))
    refine (concat _ (ap _ (inverse _))).
A: Type
b: Words
a: (A + A)%type
c: Words
freegroup_eta
  (word_change_sign (((b @ [a]) @ [a^]) @ c)) =
freegroup_eta ?Goal0
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign (b @ c) = ?Goal0
    2: apply word_change_sign_ww.
A: Type
b: Words
a: (A + A)%type
c: Words
freegroup_eta
  (word_change_sign (((b @ [a]) @ [a^]) @ c)) =
freegroup_eta
  (word_change_sign c @ word_change_sign b)
    refine (concat (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 c @ word_change_sign b)
    {
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign (((b @ [a]) @ [a^]) @ c) = ?Goal refine (concat (word_change_sign_ww _ _) _).
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign c @
word_change_sign ((b @ [a]) @ [a^]) = ?Goal
      apply ap.
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign ((b @ [a]) @ [a^]) = ?y
      refine (concat (ap _ (inverse (word_concat_w_ww _ _ _))) _).
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign (b @ ([a] @ [a^])) = ?y
      refine (concat (word_change_sign_ww _ _) _).
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign ([a] @ [a^]) @ word_change_sign b =
?y
      rapply (ap (fun t => t @ word_change_sign b)).
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign ([a] @ [a^]) = ?Goal0
      apply word_change_sign_ww. }
A: Type
b: Words
a: (A + A)%type
c: Words
freegroup_eta
  (word_change_sign c @
   ((word_change_sign [a^] @ word_change_sign [a]) @
    word_change_sign b)) =
freegroup_eta
  (word_change_sign c @ word_change_sign b)
    refine (concat _ (freegroup_tau _ a _)).
A: Type
b: Words
a: (A + A)%type
c: Words
freegroup_eta
  (word_change_sign c @
   ((word_change_sign [a^] @ word_change_sign [a]) @
    word_change_sign b)) =
freegroup_eta
  (((word_change_sign c @ [a]) @ [a^]) @
   word_change_sign b)
    apply ap.
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign c @
((word_change_sign [a^] @ word_change_sign [a]) @
 word_change_sign b) =
((word_change_sign c @ [a]) @ [a^]) @
word_change_sign b
    refine (concat (word_concat_w_ww _ _ _) _); f_ap.
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign c @
(word_change_sign [a^] @ word_change_sign [a]) =
(word_change_sign c @ [a]) @ [a^]
    refine (concat (word_concat_w_ww _ _ _) _); f_ap.
A: Type
b: Words
a: (A + A)%type
c: Words
word_change_sign c @ word_change_sign [a^] =
word_change_sign c @ [a]
    f_ap; cbn; f_ap.
A: Type
b: Words
a: (A + A)%type
c: Words
match
  match a with
  | inl a => inr a
  | inr b => inl b
  end
with
| inl a => inr a
| inr b => inl b
end = a
    apply change_sign_inv.
  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 *)
  Global 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; snrapply Coeq_ind; intro x; [ | apply path_ishprop].
A: Type
z, y: Coeq map1 map2
x: Words
(fun w : Coeq map1 map2 =>
 tr w * (tr y * tr z) = tr w * tr y * tr z) (coeq x)
    revert y; snrapply Coeq_ind; intro y; [ | apply path_ishprop].
A: Type
z: Coeq map1 map2
x, y: Words
(fun w : Coeq map1 map2 =>
 (fun w0 : Coeq map1 map2 =>
  tr w0 * (tr w * tr z) = tr w0 * tr w * tr z)
   (coeq x)) (coeq y)
    revert z; snrapply Coeq_ind; intro z; [ | apply path_ishprop].
A: Type
x, y, z: Words
(fun w : Coeq map1 map2 =>
 (fun w0 : Coeq map1 map2 =>
  (fun w1 : Coeq map1 map2 =>
   tr w1 * (tr w0 * tr w) = tr w1 * tr w0 * tr w)
    (coeq x)) (coeq y)) (coeq z)
    rapply (ap (tr o coeq)).
A: Type
x, y, z: Words
x @ (y @ z) = (x @ y) @ z
    apply word_concat_w_ww.
  Defined.

  (** Left identity *)
  Global Instance leftidentity_freegroup_type : LeftIdentity sg_op mon_unit.
A: Type
LeftIdentity sg_op mon_unit
  Proof.
A: Type
LeftIdentity sg_op mon_unit
    rapply Trunc_ind.
A: Type
forall a : Coeq map1 map2, mon_unit * tr a = tr a
    srapply Coeq_ind; intro x; [ | apply path_ishprop].
A: Type
x: Words
(fun w : Coeq map1 map2 => mon_unit * tr w = tr w)
  (coeq x)
    reflexivity.
  Defined.

  (** Right identity *)
  Global Instance rightidentity_freegroup_type : RightIdentity sg_op mon_unit.
A: Type
RightIdentity sg_op mon_unit
  Proof.
A: Type
RightIdentity sg_op mon_unit
    rapply Trunc_ind.
A: Type
forall a : Coeq map1 map2, tr a * mon_unit = tr a
    srapply Coeq_ind; intro x; [ | apply path_ishprop].
A: Type
x: Words
(fun w : Coeq map1 map2 => tr w * mon_unit = tr w)
  (coeq x)
    apply (ap tr), ap.
A: Type
x: Words
x @ nil = x
    apply word_concat_w_nil.
  Defined.

  (** Left inverse *)
  Global Instance leftinverse_freegroup_type : LeftInverse sg_op negate mon_unit.
A: Type
LeftInverse sg_op negate mon_unit
  Proof.
A: Type
LeftInverse sg_op negate mon_unit
    rapply Trunc_ind.
A: Type
forall a : Coeq map1 map2, - tr a * tr a = mon_unit
    srapply Coeq_ind; intro x; [ | apply path_ishprop].
A: Type
x: Words
(fun w : Coeq map1 map2 => - tr w * tr w = mon_unit)
  (coeq x)
    apply word_concat_Vw.
  Defined.

  (** Right inverse *)
  Global Instance rightinverse_freegroup_type : RightInverse sg_op negate mon_unit.
A: Type
RightInverse sg_op negate mon_unit
  Proof.
A: Type
RightInverse sg_op negate mon_unit
    rapply Trunc_ind.
A: Type
forall a : Coeq map1 map2, tr a * - tr a = mon_unit
    srapply Coeq_ind; intro x; [ | apply path_ishprop].
A: Type
x: Words
(fun w : Coeq map1 map2 => tr w * - tr w = mon_unit)
  (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
    snrapply (Build_Group freegroup_type); repeat split; exact _.
  Defined.

  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 x.
A: Type
G: Group
s: A -> G
x: Words
G
    induction x as [|x xs].
A: Type
G: Group
s: A -> G
G
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: list (A + A)
IHxs: G
G
    1: exact mon_unit.
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: list (A + A)
IHxs: G
G
    refine (_ * IHxs).
A: Type
G: Group
s: A -> G
x: (A + A)%type
xs: list (A + A)
IHxs: G
G
    destruct x as [x|x].
A: Type
G: Group
s: A -> G
x: A
xs: list (A + A)
IHxs: G
G
A: Type
G: Group
s: A -> G
x: A
xs: list (A + A)
IHxs: G
G
    1: exact (s x).
A: Type
G: Group
s: A -> G
x: A
xs: list (A + A)
IHxs: G
G
    exact (- s x).
  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.
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
a: (A + A)%type
x: list (A + A)
y: Words
IHx: words_rec G s (x @ y) = words_rec G s x * words_rec G s y
words_rec G s ((a :: x)%list @ y) =
words_rec G s (a :: x)%list * words_rec G s y
    1: symmetry; apply left_identity.
A: Type
G: Group
s: A -> G
a: (A + A)%type
x: list (A + A)
y: Words
IHx: words_rec G s (x @ y) = words_rec G s x * words_rec G s y
words_rec G s ((a :: x)%list @ y) =
words_rec G s (a :: x)%list * words_rec G s y
    cbn; rewrite <- simple_associativity.
A: Type
G: Group
s: A -> G
a: (A + A)%type
x: list (A + A)
y: Words
IHx: words_rec G s (x @ y) = words_rec G s x * words_rec G s y
match a with
| inl a => s a
| inr a => - s a
end *
list_rect (A + A) (fun _ : list (A + A) => G) mon_unit
  (fun (x : A + A) (_ : list (A + A)) (IHxs : G) =>
   match x with
   | inl a => s a
   | inr a => - s a
   end * IHxs) (x @ y) =
match a with
| inl a => s a
| inr a => - s a
end *
(list_rect (A + A) (fun _ : list (A + A) => G)
   mon_unit
   (fun (x : A + A) (_ : list (A + A)) (IHxs : G) =>
    match x with
    | inl a => s a
    | inr a => - s a
    end * IHxs) x * words_rec G s y)
    f_ap.
  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)
    refine (concat _ (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
    refine (concat (words_rec_pp G s _ _) _); f_ap.
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s ((b @ [a]) @ [a^]) = words_rec G s b
    refine (concat _ (right_identity _)).
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s ((b @ [a]) @ [a^]) =
words_rec G s b * mon_unit
    refine (concat (ap _ (word_concat_w_ww _ _ _)^) _).
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s (b @ ([a] @ [a^])) =
words_rec G s b * mon_unit
    refine (concat (words_rec_pp G s _ _) _); f_ap.
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
words_rec G s ([a] @ [a^]) = mon_unit
    refine (concat (concat (simple_associativity _ _ _) _) (left_identity mon_unit)).
A: Type
G: Group
s: A -> G
a: (A + A)%type
b, c: Words
match a with
| inl a => s a
| inr a => - s a
end *
match a^ with
| inl a => s a
| inr a => - s a
end * mon_unit = mon_unit * mon_unit
    destruct a; simpl; f_ap.
A: Type
G: Group
s: A -> G
a: A
b, c: Words
s a * - s a = mon_unit
A: Type
G: Group
s: A -> G
a: A
b, c: Words
- s a * s a = mon_unit
    +
A: Type
G: Group
s: A -> G
a: A
b, c: Words
s a * - s a = mon_unit apply right_inverse.
    +
A: Type
G: Group
s: A -> G
a: A
b, c: Words
- s a * s a = mon_unit apply left_inverse.
  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)
    : GroupHomomorphism FreeGroup G.
A: Type
G: Group
s: A -> G
GroupHomomorphism FreeGroup G
  Proof.
A: Type
G: Group
s: A -> G
GroupHomomorphism FreeGroup G
    snrapply Build_GroupHomomorphism.
A: Type
G: Group
s: A -> G
FreeGroup -> G
A: Type
G: Group
s: A -> G
IsSemiGroupPreserving ?f
    {
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; snrapply Coeq_ind; hnf; intro x; [ | apply path_ishprop ].
A: Type
G: Group
s: A -> G
y: Coeq map1 map2
x: Words
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 (coeq 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 (coeq 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 y; snrapply Coeq_ind; hnf; intro y; [ | apply path_ishprop ].
A: Type
G: Group
s: A -> G
x, y: Words
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 (coeq x) * tr (coeq 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 (coeq 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 (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.

  (** Now we need to prove that the free group satisifes the unviersal property of the free group. *)
  (** TODO: remove funext from here and universal property of free group *)
  Global Instance isfreegroupon_freegroup `{Funext}
    : IsFreeGroupOn A FreeGroup (freegroup_eta o word_sing o inl).
A: Type
H: Funext
IsFreeGroupOn A FreeGroup
  (freegroup_eta o word_sing o inl)
  Proof.
A: Type
H: Funext
IsFreeGroupOn A FreeGroup
  (freegroup_eta o word_sing o inl)
    intros G f.
A: Type
H: Funext
G: Group
f: A -> G
Contr
  (FactorsThroughFreeGroup A FreeGroup
     (fun x : A => freegroup_eta [inl x]) G f)
    snrapply Build_Contr.
A: Type
H: Funext
G: Group
f: A -> G
FactorsThroughFreeGroup A FreeGroup
  (fun x : A => freegroup_eta [inl x]) G f
A: Type
H: Funext
G: Group
f: A -> G
forall
y : FactorsThroughFreeGroup A FreeGroup
      (fun x : A => freegroup_eta [inl x]) G f,
?center = y
    {
A: Type
H: Funext
G: Group
f: A -> G
FactorsThroughFreeGroup A FreeGroup
  (fun x : A => freegroup_eta [inl x]) 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 (freegroup_eta [inl x])) == f
      1: apply FreeGroup_rec, f.
A: Type
H: Funext
G: Group
f: A -> G
(fun x : A =>
 FreeGroup_rec G f (freegroup_eta [inl x])) == f
      intro x; simpl.
A: Type
H: Funext
G: Group
f: A -> G
x: A
f x * mon_unit = f x
      apply right_identity. }
A: Type
H: Funext
G: Group
f: A -> G
forall
y : FactorsThroughFreeGroup A FreeGroup
      (fun x : A => freegroup_eta [inl x]) G f,
(FreeGroup_rec G f : FreeGroup $-> G;
((fun x : A =>
  right_identity (f x)
  :
  FreeGroup_rec G f (freegroup_eta [inl x]) = f x)
 :
 (fun x : A =>
  FreeGroup_rec G f (freegroup_eta [inl x])) == f)
:
(fun f0 : FreeGroup $-> G =>
 f0 o (fun x : A => freegroup_eta [inl x]) == f)
  (FreeGroup_rec G f : FreeGroup $-> G)) = y
    intros [g h].
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
(FreeGroup_rec G f; fun x : A => right_identity (f x)) =
(g; h)
    nrapply path_sigma_hprop; [ exact _ |].
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
(FreeGroup_rec G f; fun x : A => right_identity (f x)).1 =
(g; h).1
    simpl.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
FreeGroup_rec G f = g
    apply equiv_path_grouphomomorphism.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
FreeGroup_rec G f == g
    intro x.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
x: FreeGroup
FreeGroup_rec G f x = g x
    rewrite <- (path_forall _ _ h).
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
x: FreeGroup
FreeGroup_rec G
  (fun x : A => g (freegroup_eta [inl x])) x = g x
    strip_truncations; revert x.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
forall x : Coeq map1 map2,
FreeGroup_rec G
  (fun x0 : A => g (freegroup_eta [inl x0])) (tr x) =
g (tr x)
    snrapply Coeq_ind; intro x; [|apply path_ishprop].
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
x: Words
(fun w : Coeq map1 map2 =>
 FreeGroup_rec G
   (fun x : A => g (freegroup_eta [inl x])) (tr w) =
 g (tr w)) (coeq x)
    hnf; symmetry.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
x: Words
g (tr (coeq x)) =
FreeGroup_rec G
  (fun x : A => g (freegroup_eta [inl x]))
  (tr (coeq x))
    induction x.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
g (tr (coeq nil)) =
FreeGroup_rec G
  (fun x : A => g (freegroup_eta [inl x]))
  (tr (coeq nil))
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
a: (A + A)%type
x: list (A + A)
IHx: g (tr (coeq x)) =
FreeGroup_rec G (fun x : A => g (freegroup_eta [inl x])) (tr (coeq x))
g (tr (coeq (a :: x)%list)) =
FreeGroup_rec G
  (fun x : A => g (freegroup_eta [inl x]))
  (tr (coeq (a :: x)%list))
    1: apply (grp_homo_unit g).
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
a: (A + A)%type
x: list (A + A)
IHx: g (tr (coeq x)) =
FreeGroup_rec G (fun x : A => g (freegroup_eta [inl x])) (tr (coeq x))
g (tr (coeq (a :: x)%list)) =
FreeGroup_rec G
  (fun x : A => g (freegroup_eta [inl x]))
  (tr (coeq (a :: x)%list))
    refine (concat (grp_homo_op g (freegroup_eta [a]) (freegroup_eta x)) _).
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
a: (A + A)%type
x: list (A + A)
IHx: g (tr (coeq x)) =
FreeGroup_rec G (fun x : A => g (freegroup_eta [inl x])) (tr (coeq x))
g (freegroup_eta [a]) * g (freegroup_eta x) =
FreeGroup_rec G
  (fun x : A => g (freegroup_eta [inl x]))
  (tr (coeq (a :: x)%list))
    simpl.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
a: (A + A)%type
x: list (A + A)
IHx: g (tr (coeq x)) =
FreeGroup_rec G (fun x : A => g (freegroup_eta [inl x])) (tr (coeq x))
g (freegroup_eta [a]) * g (freegroup_eta x) =
match a with
| inl a => g (freegroup_eta [inl a])
| inr a => - g (freegroup_eta [inl a])
end *
words_rec G (fun x : A => g (freegroup_eta [inl x])) x
    f_ap.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
a: (A + A)%type
x: list (A + A)
IHx: g (tr (coeq x)) =
FreeGroup_rec G (fun x : A => g (freegroup_eta [inl x])) (tr (coeq x))
g (freegroup_eta [a]) =
match a with
| inl a => g (freegroup_eta [inl a])
| inr a => - g (freegroup_eta [inl a])
end
    destruct a.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
a: A
x: list (A + A)
IHx: g (tr (coeq x)) =
FreeGroup_rec G (fun x : A => g (freegroup_eta [inl x])) (tr (coeq x))
g (freegroup_eta [inl a]) = g (freegroup_eta [inl a])
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
a: A
x: list (A + A)
IHx: g (tr (coeq x)) =
FreeGroup_rec G (fun x : A => g (freegroup_eta [inl x])) (tr (coeq x))
g (freegroup_eta [inr a]) =
- g (freegroup_eta [inl a])
    1: reflexivity.
A: Type
H: Funext
G: Group
f: A -> G
g: FreeGroup $-> G
h: (fun x : A => g (freegroup_eta [inl x])) == f
a: A
x: list (A + A)
IHx: g (tr (coeq x)) =
FreeGroup_rec G (fun x : A => g (freegroup_eta [inl x])) (tr (coeq x))
g (freegroup_eta [inr a]) =
- g (freegroup_eta [inl a])
    exact (grp_homo_inv g (freegroup_eta [inl a])).
  Defined.

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

  Definition freegroup_in : A -> FreeGroup
    := freegroup_eta o word_sing o inl.

  Lemma FreeGroup_rec_beta {G : Group} (f : A -> G)
    : FreeGroup_rec _ f o freegroup_in == f.
A: Type
G: Group
f: A -> G
FreeGroup_rec G f o freegroup_in == f
  Proof.
A: Type
G: Group
f: A -> G
FreeGroup_rec G f o freegroup_in == f
    intros x.
A: Type
G: Group
f: A -> G
x: A
FreeGroup_rec G f (freegroup_in x) = f x
    apply grp_unit_r.
  Defined.

  Coercion freegroup_in : A >-> group_type.

End Reduction.

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.

Global 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.

Global 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))
  apply 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)
  snrapply 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 G 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)
    snrapply 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)
    snrapply 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) apply 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))
  ((let X :=
      grp_homo_map F_S (subgroup_generated (hfiber i))
        to_subgroup_generated in
    X) 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 F_S F_S) (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))) apply 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
    nrapply Build_GroupIsomorphism.
S: Type
F_S: Group
i: S -> F_S
H: IsFreeGroupOn S F_S i
IsEquiv ?Goal
    apply isequiv_subgroup_incl_freegroupon.
  Defined.

End FreeGroupGenerated.