Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.Core.
Require Import Algebra.Groups.Group.
Require Import Algebra.Groups.FreeGroup.
Require Import Algebra.Groups.GroupCoeq.
Require Import Spaces.Finite.
Require Import WildCat.


Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.

(** In this file we develop presentations of groups. *)

(** The data of a group presentation *)
Record GroupPresentation := {
  (** We have a type of generators *)
  gp_generators : Type ;
  (** An indexing type for relators *)
  gp_rel_index : Type ;
  (** The relators are picked out amongst elements of the free group on the generators. *)
  gp_relators : gp_rel_index -> FreeGroup gp_generators;
}.

(** Note: A relator is a relation in the form of "w = 1", any relation "w = v" can become a relator "wv^-1 = 1" for words v and w. *)

(** Given the data of a group presentation we can construct the group. This is sometimes called the presented group. *)
Definition group_gp : GroupPresentation -> Group.
GroupPresentation -> Group
Proof.
GroupPresentation -> Group
  intros [X I R].
X, I: Type
R: I -> FreeGroup X
Group
  exact (GroupCoeq
    (FreeGroup_rec I (FreeGroup X) R)
    (FreeGroup_rec I (FreeGroup X) (fun x => @group_unit (FreeGroup X)))).
Defined.

(** A group [G] has a presentation if there exists a group presentation whose presented group is isomorphic to [G]. *)
Class HasPresentation (G : Group) := {
  presentation : GroupPresentation;
  grp_iso_presentation : GroupIsomorphism (group_gp presentation) G;
}.

Coercion presentation : HasPresentation >-> GroupPresentation.

(** Here are a few finiteness properties of group presentations. *)

(** A group presentation is finitely generated if its generating set is finite. *)
Class FinitelyGeneratedPresentation (P : GroupPresentation)
  := finite_gp_generators : Finite (gp_generators P).

(** A group presentation is finitely related if its relators indexing set is finite. *)
Class FinitelyRelatedPresentation (P : GroupPresentation)
  := finite_gp_relators : Finite (gp_rel_index P).

(** A group presentation is a finite presentation if it is finitely generated and related. *)
Class FinitePresentation (P : GroupPresentation) := {
  fp_generators : FinitelyGeneratedPresentation P;
  fp_relators : FinitelyRelatedPresentation P;
}.

(** These directly translate into properties of groups. *)

(** A group is finitely generated if it has a finitely generated presentation. *)
Class IsFinitelyGenerated (G : Group) := {
  fg_presentation : HasPresentation G;
  fg_presentation_fg : FinitelyGeneratedPresentation fg_presentation;
}.

(** A group is finitely related if it has a finitely related presentation. *)
Class IsFinitelyRelated (G : Group) := {
  fr_presentation : HasPresentation G;
  fr_presentation_fr : FinitelyRelatedPresentation fr_presentation;
}.

Class IsFinitelyPresented (G : Group) := {
  fp_presentation : HasPresentation G;
  fp_presentation_fp : FinitePresentation fp_presentation;
}.

(** ** Fundamental theorem of presentations of groups *)

(** A group homomorphism from a presented group is determined with how the underlying map acts on generators subject to the condition that relators are sent to the unit. *)
Theorem grp_pres_rec {funext : Funext} (G : Group) (P : HasPresentation G) (H : Group)
  : {f : gp_generators P -> H & forall r,
      FreeGroup_rec _ _ f (gp_relators P r) = group_unit}
    <~> GroupHomomorphism G H.
funext: Funext
G: Group
P: HasPresentation G
H: Group
{f : gp_generators P -> H &
forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit} <~> GroupHomomorphism G H
Proof.
funext: Funext
G: Group
P: HasPresentation G
H: Group
{f : gp_generators P -> H &
forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit} <~> GroupHomomorphism G H
  refine ((equiv_precompose_cat_equiv grp_iso_presentation)^-1 oE _).
funext: Funext
G: Group
P: HasPresentation G
H: Group
{f : gp_generators P -> H &
forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit} <~> (group_gp P $-> H)
  refine (equiv_groupcoeq_rec _ _ oE _).
funext: Funext
G: Group
P: HasPresentation G
H: Group
{f : gp_generators P -> H &
forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit} <~>
{h : FreeGroup (gp_generators P) $-> H &
(fun x : FreeGroup (gp_rel_index P) =>
 h
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(fun x : FreeGroup (gp_rel_index P) =>
 h
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P))
      (fun _ : gp_rel_index P => group_unit) x))}
  srefine (equiv_functor_sigma_pb _ oE _).
funext: Funext
G: Group
P: HasPresentation G
H: Group
Type
funext: Funext
G: Group
P: HasPresentation G
H: Group
?A <~> (FreeGroup (gp_generators P) $-> H)
funext: Funext
G: Group
P: HasPresentation G
H: Group
{f : gp_generators P -> H &
forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit} <~>
{x : _ &
((fun h : FreeGroup (gp_generators P) $-> H =>
  (fun x : FreeGroup (gp_rel_index P) =>
   h
     (FreeGroup_rec (gp_rel_index P)
        (FreeGroup (gp_generators P)) 
        (gp_relators P) x)) ==
  (fun x : FreeGroup (gp_rel_index P) =>
   h
     (FreeGroup_rec (gp_rel_index P)
        (FreeGroup (gp_generators P))
        (fun _ : gp_rel_index P => group_unit) x)))
 o ?f) x}
  2: apply equiv_freegroup_rec.
funext: Funext
G: Group
P: HasPresentation G
H: Group
{f : gp_generators P -> H &
forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit} <~>
{x : _ &
((fun h : FreeGroup (gp_generators P) $-> H =>
  (fun x : FreeGroup (gp_rel_index P) =>
   h
     (FreeGroup_rec (gp_rel_index P)
        (FreeGroup (gp_generators P)) (gp_relators P)
        x)) ==
  (fun x : FreeGroup (gp_rel_index P) =>
   h
     (FreeGroup_rec (gp_rel_index P)
        (FreeGroup (gp_generators P))
        (fun _ : gp_rel_index P => group_unit) x)))
 o equiv_freegroup_rec H (gp_generators P)) x}
  apply equiv_functor_sigma_id.
funext: Funext
G: Group
P: HasPresentation G
H: Group
forall a : gp_generators P -> H,
(forall r : gp_rel_index P,
 FreeGroup_rec (gp_generators P) H a (gp_relators P r) =
 group_unit) <~>
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) a
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) a
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P))
      (fun _ : gp_rel_index P => group_unit) x))
  intros f.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
(forall r : gp_rel_index P,
 FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
 group_unit) <~>
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P))
      (fun _ : gp_rel_index P => group_unit) x))
  srapply equiv_iff_hprop.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
(forall r : gp_rel_index P,
 FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
 group_unit) ->
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P))
      (fun _ : gp_rel_index P => group_unit) x))
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P)) 
      (gp_relators P) x)) ==
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P))
      (fun _ : gp_rel_index P => group_unit) x)) ->
forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
  {
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
(forall r : gp_rel_index P,
 FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
 group_unit) ->
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P))
      (fun _ : gp_rel_index P => group_unit) x)) intros p.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P))
      (fun _ : gp_rel_index P => group_unit) x))
    hnf.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
forall x : FreeGroup (gp_rel_index P),
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) (gp_relators P) x) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit) x)
    rapply Trunc_ind.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
forall
a : Coeq.Coeq (FreeGroup.map1 (gp_rel_index P))
      (FreeGroup.map2 (gp_rel_index P)),
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) (gp_relators P)
     (tr a)) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit) (tr a))
    srapply Coeq.Coeq_ind.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
forall a : FreeGroup.Words (gp_rel_index P),
(fun
   w : Coeq.Coeq (FreeGroup.map1 (gp_rel_index P))
         (FreeGroup.map2 (gp_rel_index P)) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P)) (gp_relators P)
      (tr w)) =
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P))
      (fun _ : gp_rel_index P => group_unit) (tr w)))
  (Coeq.coeq a)
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
forall
b : FreeGroup.Words (gp_rel_index P) *
    (gp_rel_index P + gp_rel_index P) *
    FreeGroup.Words (gp_rel_index P),
transport
  (fun
     w : Coeq.Coeq (FreeGroup.map1 (gp_rel_index P))
           (FreeGroup.map2 (gp_rel_index P)) =>
   equiv_freegroup_rec H 
     (gp_generators P) f
     (FreeGroup_rec (gp_rel_index P)
        (FreeGroup (gp_generators P)) 
        (gp_relators P) 
        (tr w)) =
   equiv_freegroup_rec H 
     (gp_generators P) f
     (FreeGroup_rec (gp_rel_index P)
        (FreeGroup (gp_generators P))
        (fun _ : gp_rel_index P => group_unit) 
        (tr w))) (Coeq.cglue b)
  (?coeq' (FreeGroup.map1 (gp_rel_index P) b)) =
?coeq' (FreeGroup.map2 (gp_rel_index P) b)
    2: intros; apply path_ishprop.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
forall a : FreeGroup.Words (gp_rel_index P),
(fun
   w : Coeq.Coeq (FreeGroup.map1 (gp_rel_index P))
         (FreeGroup.map2 (gp_rel_index P)) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P)) (gp_relators P)
      (tr w)) =
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P))
      (fun _ : gp_rel_index P => group_unit) (tr w)))
  (Coeq.coeq a)
    intros w; hnf.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
w: FreeGroup.Words (gp_rel_index P)
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) (gp_relators P)
     (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq w)))
    induction w.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) (gp_relators P)
     (tr (Coeq.coeq Core.nil))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq Core.nil)))
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
a: (gp_rel_index P + gp_rel_index P)%type
w: Core.list (gp_rel_index P + gp_rel_index P)
IHw: equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq w)))
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) 
     (gp_relators P) (tr (Coeq.coeq (Core.cons a w)))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq (Core.cons a w))))
    1: reflexivity.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
a: (gp_rel_index P + gp_rel_index P)%type
w: Core.list (gp_rel_index P + gp_rel_index P)
IHw: equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq w)))
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) (gp_relators P)
     (tr (Coeq.coeq (Core.cons a w)))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq (Core.cons a w))))
    simpl.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
a: (gp_rel_index P + gp_rel_index P)%type
w: Core.list (gp_rel_index P + gp_rel_index P)
IHw: equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq w)))
Trunc_rec
  (Coeq.Coeq_rec H (words_rec (gp_generators P) H f)
     (fun
        b0 : FreeGroup.Words (gp_generators P) *
             (gp_generators P + gp_generators P) *
             FreeGroup.Words (gp_generators P) =>
      words_rec_coh (gp_generators P) H f
        (snd (fst b0)) (fst (fst b0)) (snd b0)))
  (match a with
   | inl a => gp_relators P a
   | inr a => - gp_relators P a
   end *
   words_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) (gp_relators P) w) =
Trunc_rec
  (Coeq.Coeq_rec H (words_rec (gp_generators P) H f)
     (fun
        b0 : FreeGroup.Words (gp_generators P) *
             (gp_generators P + gp_generators P) *
             FreeGroup.Words (gp_generators P) =>
      words_rec_coh (gp_generators P) H f
        (snd (fst b0)) (fst (fst b0)) (snd b0)))
  (match a with
   | inl _ => monunit_freegroup_type (gp_generators P)
   | inr _ =>
       - monunit_freegroup_type (gp_generators P)
   end *
   words_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P =>
      monunit_freegroup_type (gp_generators P)) w)
    refine (_ @ _ @ _^).
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
a: (gp_rel_index P + gp_rel_index P)%type
w: Core.list (gp_rel_index P + gp_rel_index P)
IHw: equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq w)))
Trunc_rec
  (Coeq.Coeq_rec H (words_rec (gp_generators P) H f)
     (fun
        b0 : FreeGroup.Words (gp_generators P) *
             (gp_generators P + gp_generators P) *
             FreeGroup.Words (gp_generators P) =>
      words_rec_coh (gp_generators P) H f
        (snd (fst b0)) (fst (fst b0)) (snd b0)))
  (match a with
   | inl a => gp_relators P a
   | inr a => - gp_relators P a
   end *
   words_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) (gp_relators P) w) =
?Goal1
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
a: (gp_rel_index P + gp_rel_index P)%type
w: Core.list (gp_rel_index P + gp_rel_index P)
IHw: equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq w)))
?Goal1 = ?Goal0
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
a: (gp_rel_index P + gp_rel_index P)%type
w: Core.list (gp_rel_index P + gp_rel_index P)
IHw: equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq w)))
Trunc_rec
  (Coeq.Coeq_rec H (words_rec (gp_generators P) H f)
     (fun
        b0 : FreeGroup.Words (gp_generators P) *
             (gp_generators P + gp_generators P) *
             FreeGroup.Words (gp_generators P) =>
      words_rec_coh (gp_generators P) H f
        (snd (fst b0)) (fst (fst b0)) 
        (snd b0)))
  (match a with
   | inl _ => monunit_freegroup_type (gp_generators P)
   | inr _ =>
       - monunit_freegroup_type (gp_generators P)
   end *
   words_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P =>
      monunit_freegroup_type (gp_generators P)) w) =
?Goal0
    1,3: exact (grp_homo_op (FreeGroup_rec _ _ _) _ _).
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
a: (gp_rel_index P + gp_rel_index P)%type
w: Core.list (gp_rel_index P + gp_rel_index P)
IHw: equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq w)))
FreeGroup_rec (gp_generators P) H f
  match a with
  | inl a => gp_relators P a
  | inr a => - gp_relators P a
  end *
FreeGroup_rec (gp_generators P) H f
  (words_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) (gp_relators P) w) =
FreeGroup_rec (gp_generators P) H f
  match a with
  | inl _ => monunit_freegroup_type (gp_generators P)
  | inr _ =>
      - monunit_freegroup_type (gp_generators P)
  end *
FreeGroup_rec (gp_generators P) H f
  (words_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P =>
      monunit_freegroup_type (gp_generators P)) w)
    f_ap.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
a: (gp_rel_index P + gp_rel_index P)%type
w: Core.list (gp_rel_index P + gp_rel_index P)
IHw: equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq w)))
FreeGroup_rec (gp_generators P) H f
  match a with
  | inl a => gp_relators P a
  | inr a => - gp_relators P a
  end =
FreeGroup_rec (gp_generators P) H f
  match a with
  | inl _ => monunit_freegroup_type (gp_generators P)
  | inr _ =>
      - monunit_freegroup_type (gp_generators P)
  end
    destruct a.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
g: gp_rel_index P
w: Core.list (gp_rel_index P + gp_rel_index P)
IHw: equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq w)))
FreeGroup_rec (gp_generators P) H f (gp_relators P g) =
FreeGroup_rec (gp_generators P) H f
  (monunit_freegroup_type (gp_generators P))
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
g: gp_rel_index P
w: Core.list (gp_rel_index P + gp_rel_index P)
IHw: equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq w)))
FreeGroup_rec (gp_generators P) H f
  (- gp_relators P g) =
FreeGroup_rec (gp_generators P) H f
  (- monunit_freegroup_type (gp_generators P))
    1: refine (p _ @ (grp_homo_unit _)^).
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
g: gp_rel_index P
w: Core.list (gp_rel_index P + gp_rel_index P)
IHw: equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq w)))
FreeGroup_rec (gp_generators P) H f
  (- gp_relators P g) =
FreeGroup_rec (gp_generators P) H f
  (- monunit_freegroup_type (gp_generators P))
    refine (grp_homo_inv _ _ @ ap _ _ @ (grp_homo_inv _ _)^).
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
  (gp_relators P r) = group_unit
g: gp_rel_index P
w: Core.list (gp_rel_index P + gp_rel_index P)
IHw: equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (tr (Coeq.coeq w)))
FreeGroup_rec (gp_generators P) H f (gp_relators P g) =
FreeGroup_rec (gp_generators P) H f
  (monunit_freegroup_type (gp_generators P))
    refine (p _ @ (grp_homo_unit _)^). }
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P))
      (fun _ : gp_rel_index P => group_unit) x)) ->
forall r : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
  intros p r.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: (fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P))
      (gp_relators P) x)) ==
(fun x : FreeGroup (gp_rel_index P) =>
 equiv_freegroup_rec H (gp_generators P) f
   (FreeGroup_rec (gp_rel_index P)
      (FreeGroup (gp_generators P))
      (fun _ : gp_rel_index P => group_unit) x))
r: gp_rel_index P
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
  hnf in p.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall x : FreeGroup (gp_rel_index P),
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) 
     (gp_relators P) x) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit) x)
r: gp_rel_index P
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
  pose (p' := p o freegroup_eta).
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall x : FreeGroup (gp_rel_index P),
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) 
     (gp_relators P) x) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit) x)
r: gp_rel_index P
p':= p o freegroup_eta: forall x : FreeGroup.Words (gp_rel_index P),
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (freegroup_eta x)) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (freegroup_eta x))
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
  clearbody p'; clear p.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
r: gp_rel_index P
p': forall x : FreeGroup.Words (gp_rel_index P),
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P) (freegroup_eta x)) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (freegroup_eta x))
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
  specialize (p' (FreeGroup.word_sing _ (inl r))).
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
r: gp_rel_index P
p': equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P)
     (freegroup_eta
        (FreeGroup.word_sing 
           (gp_rel_index P) 
           (inl r)))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (freegroup_eta
        (FreeGroup.word_sing 
           (gp_rel_index P) 
           (inl r))))
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
  refine (_ @ p').
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
r: gp_rel_index P
p': equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (gp_relators P)
     (freegroup_eta
        (FreeGroup.word_sing 
           (gp_rel_index P) 
           (inl r)))) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P))
     (fun _ : gp_rel_index P => group_unit)
     (freegroup_eta
        (FreeGroup.word_sing 
           (gp_rel_index P) 
           (inl r))))
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) (gp_relators P)
     (freegroup_eta
        (FreeGroup.word_sing (gp_rel_index P) (inl r))))
  clear p'.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
r: gp_rel_index P
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) (gp_relators P)
     (freegroup_eta
        (FreeGroup.word_sing (gp_rel_index P) (inl r))))
  symmetry.
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
r: gp_rel_index P
equiv_freegroup_rec H (gp_generators P) f
  (FreeGroup_rec (gp_rel_index P)
     (FreeGroup (gp_generators P)) (gp_relators P)
     (freegroup_eta
        (FreeGroup.word_sing (gp_rel_index P) (inl r)))) =
FreeGroup_rec (gp_generators P) H f (gp_relators P r)
  refine (grp_homo_op _ _ _ @ _).
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
r: gp_rel_index P
equiv_freegroup_rec H (gp_generators P) f
  (gp_relators P r) *
equiv_freegroup_rec H (gp_generators P) f mon_unit =
FreeGroup_rec (gp_generators P) H f (gp_relators P r)
  refine (_ @ right_identity _).
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
r: gp_rel_index P
equiv_freegroup_rec H (gp_generators P) f
  (gp_relators P r) *
equiv_freegroup_rec H (gp_generators P) f mon_unit =
FreeGroup_rec (gp_generators P) H f (gp_relators P r) *
mon_unit
  f_ap.
Defined.

(** ** Constructors for finite presentations *)

Definition Build_Finite_GroupPresentation n m
  (f : FinSeq m (FreeGroup (Fin n)))
  : GroupPresentation.
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
GroupPresentation
Proof.
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
GroupPresentation
  snrapply Build_GroupPresentation.
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
Type
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
Type
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
?gp_rel_index -> FreeGroup ?gp_generators
  -
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
Type exact (Fin n).
  -
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
Type exact (Fin m).
  -
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
Fin m -> FreeGroup (Fin n) exact f.
Defined.

Global Instance FinitelyGeneratedPresentation_Build_Finite_GroupPresentation
  {n m f}
  : FinitelyGeneratedPresentation (Build_Finite_GroupPresentation n m f).
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
FinitelyGeneratedPresentation
  (Build_Finite_GroupPresentation n m f)
Proof.
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
FinitelyGeneratedPresentation
  (Build_Finite_GroupPresentation n m f)
  unshelve econstructor.
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
nat
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
merely
  (gp_generators
     (Build_Finite_GroupPresentation n m f) <~>
   Fin ?fcard)
  2: simpl; apply tr; reflexivity.
Defined.

Global Instance FinitelyRelatedPresentation_Build_Finite_GroupPresentation
  {n m f}
  : FinitelyRelatedPresentation (Build_Finite_GroupPresentation n m f).
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
FinitelyRelatedPresentation
  (Build_Finite_GroupPresentation n m f)
Proof.
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
FinitelyRelatedPresentation
  (Build_Finite_GroupPresentation n m f)
  unshelve econstructor.
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
nat
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
merely
  (gp_rel_index (Build_Finite_GroupPresentation n m f) <~>
   Fin ?fcard)
  2: simpl; apply tr; reflexivity.
Defined.

(** ** Notations for presentations *)

(** Convenient abbreviation when defining notations. *)
Local Notation ff := (freegroup_in o fin_nat).

(** TODO: I haven't worked out how to generalize to any number of binders, so we explicitly list the first few levels. *)

Local Open Scope nat_scope.

(** One generator *)
Notation "⟨ x | F , .. , G ⟩" :=
  (Build_Finite_GroupPresentation 1 _
    (fscons ((fun (x : FreeGroup (Fin 1))
      => F : FreeGroup (Fin _)) (ff 0%nat))
    .. (fscons ((fun (x : FreeGroup (Fin 1))
      => G : FreeGroup (Fin _)) (ff 0)) fsnil) ..))
  (at level 200, x binder).

(** Two generators *)
Notation "⟨ x , y | F , .. , G ⟩" :=
  (Build_Finite_GroupPresentation 2 _
    (fscons ((fun (x y : FreeGroup (Fin 2))
      => F : FreeGroup (Fin _)) (ff 0) (ff 1))
    .. (fscons ((fun (x y : FreeGroup (Fin 2))
      => G : FreeGroup (Fin _)) (ff 0) (ff 1)) fsnil) ..))
  (at level 200, x binder, y binder).

(** Three generators *)
Notation "⟨ x , y , z | F , .. , G ⟩" :=
  (Build_Finite_GroupPresentation 3 _
    (fscons ((fun (x y z : FreeGroup (Fin 3))
      => F : FreeGroup (Fin _)) (ff 0) (ff 1) (ff 2))
    .. (fscons ((fun (x y z : FreeGroup (Fin 3))
      => G : FreeGroup (Fin _)) (ff 0) (ff 1) (ff 2)) fsnil) ..))
  (at level 200, x binder, y binder, z binder).