(* -*- mode: coq; mode: visual-line -*-  *)
Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Pointed.
Require Import Truncations.Core Truncations.Connectedness.
Require Import Homotopy.ClassifyingSpace.
Require Import Algebra.Groups.
Require Import WildCat.

Local Open Scope trunc_scope.
Local Open Scope path_scope.
Local Open Scope pointed_scope.

(** Keyed unification makes [rewrite !loops_functor_group] take a really long time.  See https://coq.inria.fr/bugs/show_bug.cgi?id=4544 for more discussion. *)
Local Unset Keyed Unification.

(** * oo-Groups *)

(** We want a workable definition of "oo-group" (what a classical homotopy theorist would call a "grouplike Aoo-space"). The classical definitions using operads or Segal spaces involve infinitely much data, which we don't know how to handle in HoTT. But instead, we can invoke the theorem (which is a theorem in classical homotopy theory, and also in any oo-topos) that every oo-group is the loop space of some pointed connected object, and use it instead as a definition: we define an oo-group to be a pointed connected type (its classifying space or delooping). Then we make subsidiary definitions to allow us to treat such an object in the way we would expect, e.g. an oo-group homomorphism is a pointed map between classifying spaces. *)

(** ** Definition *)

Record ooGroup :=
  { classifying_space : pType ;
    isconn_classifying_space : IsConnected 0 classifying_space
  }.

Global Existing Instance isconn_classifying_space.

Local Notation B := classifying_space.

Definition group_type (G : ooGroup) : Type
  := point (B G) = point (B G).

(** The following is fundamental: we declare a coercion from oo-groups to types which takes a pointed connected type not to its underlying type, but to its loop space. Thus, if [G : ooGroup], then [g : G] means that [g] is an element of the oo-group that [G] is intended to denote, which is the loop space of the pointed connected type that is technically the data of which [G : ooGroup] consists. This makes it easier to really think of [G] as "really being" an oo-group rather than its classifying space.

This is also convenient because elements of oo-groups are, definitionally, loops in some type. Thus, the oo-group operations like multiplication, inverse, associativity, higher associativity, etc. are simply special cases of the corresponding operations for paths. *)

Coercion group_type : ooGroup >-> Sortclass.

(** Every pointed type has a loop space that is an oo-group. *)
Definition group_loops (X : pType)
  : ooGroup.
X: pType
ooGroup
Proof.
X: pType
ooGroup
  pose (BG := [{ x:X & merely (x = pt) },
               exist (fun x:X => merely (x = pt)) pt (tr 1)]).
X: pType
BG:= [{x : X & merely (x = pt)}, (pt; tr 1)]: pType
ooGroup
  (** Using [cut] prevents Coq from looking for these facts with typeclass search, which is slow and (for some reason) introduces scads of extra universes. *)
  cut (IsConnected 0 BG).
X: pType
BG:= [{x : X & merely (x = pt)}, (pt; tr 1)]: pType
IsConnected (Tr 0) BG -> ooGroup
X: pType
BG:= [{x : X & merely (x = pt)}, (pt; tr 1)]: pType
IsConnected (Tr 0) BG
  {
X: pType
BG:= [{x : X & merely (x = pt)}, (pt; tr 1)]: pType
IsConnected (Tr 0) BG -> ooGroup exact (Build_ooGroup BG). }
X: pType
BG:= [{x : X & merely (x = pt)}, (pt; tr 1)]: pType
IsConnected (Tr 0) BG
  cut (IsSurjection (unit_name (point BG))).
X: pType
BG:= [{x : X & merely (x = pt)}, (pt; tr 1)]: pType
IsConnMap (Tr (-1)) (unit_name pt) ->
IsConnected (Tr 0) BG
X: pType
BG:= [{x : X & merely (x = pt)}, (pt; tr 1)]: pType
IsConnMap (Tr (-1)) (unit_name pt)
  {
X: pType
BG:= [{x : X & merely (x = pt)}, (pt; tr 1)]: pType
IsConnMap (Tr (-1)) (unit_name pt) ->
IsConnected (Tr 0) BG intros; refine (conn_pointed_type pt). }
X: pType
BG:= [{x : X & merely (x = pt)}, (pt; tr 1)]: pType
IsConnMap (Tr (-1)) (unit_name pt)
  apply BuildIsSurjection; simpl; intros [x p].
X: pType
BG:= [{x : X & merely (x = pt)}, (pt; tr 1)]: pType
x: X
p: Tr (-1) (x = pt)
Tr (-1) (hfiber (unit_name pt) (x; p))
  strip_truncations; apply tr; exists tt.
X: pType
BG:= [{x : X & merely (x = pt)}, (pt; tr 1)]: pType
x: X
p: x = pt
pt = (x; tr p)
  apply path_sigma_hprop; simpl.
X: pType
BG:= [{x : X & merely (x = pt)}, (pt; tr 1)]: pType
x: X
p: x = pt
pt = x
  exact (p^).
Defined.

(** Unfortunately, the underlying type of that oo-group is not *definitionally* the same as the ordinary loop space, but it is equivalent to it. *)
Definition loops_group (X : pType)
  : loops X <~> group_loops X.
X: pType
loops X <~> group_loops X
Proof.
X: pType
loops X <~> group_loops X
  unfold loops, group_type.
X: pType
[pt = pt, 1] <~> pt = pt simpl.
X: pType
pt = pt <~> pt = pt
  exact (equiv_path_sigma_hprop (point X ; tr 1) (point X ; tr 1)).
Defined.

(** ** Homomorphisms *)

(** *** Definition *)

Definition ooGroupHom (G H : ooGroup)
  := B G ->* B H.

Definition grouphom_fun {G H} (phi : ooGroupHom G H) : G -> H
  := fmap loops phi.

Coercion grouphom_fun : ooGroupHom >-> Funclass.

(** The loop group functor takes values in oo-group homomorphisms. *)
Definition group_loops_functor
           {X Y : pType} (f : X ->* Y)
: ooGroupHom (group_loops X) (group_loops Y).
X, Y: pType
f: X ->* Y
ooGroupHom (group_loops X) (group_loops Y)
Proof.
X, Y: pType
f: X ->* Y
ooGroupHom (group_loops X) (group_loops Y)
  simple refine (Build_pMap _ _ _ _); simpl.
X, Y: pType
f: X ->* Y
{x : X & Tr (-1) (x = pt)} ->
{x : Y & Tr (-1) (x = pt)}
X, Y: pType
f: X ->* Y
?Goal pt = pt
  -
X, Y: pType
f: X ->* Y
{x : X & Tr (-1) (x = pt)} ->
{x : Y & Tr (-1) (x = pt)} intros [x p].
X, Y: pType
f: X ->* Y
x: X
p: Tr (-1) (x = pt)
{x : Y & Tr (-1) (x = pt)}
    exists (f x).
X, Y: pType
f: X ->* Y
x: X
p: Tr (-1) (x = pt)
Tr (-1) (f x = pt)
    strip_truncations; apply tr.
X, Y: pType
f: X ->* Y
x: X
p: x = pt
f x = pt
    exact (ap f p @ point_eq f).
  -
X, Y: pType
f: X ->* Y
(fun X0 : {x : X & Tr (-1) (x = pt)} =>
 (fun (x : X) (p : Tr (-1) (x = pt)) =>
  (f x;
  Trunc_ind
    (fun _ : Trunc (-1) (x = pt) => Tr (-1) (f x = pt))
    (fun p0 : x = pt => tr (ap f p0 @ point_eq f)) p))
   X0.1 X0.2) pt = pt apply path_sigma_hprop; simpl.
X, Y: pType
f: X ->* Y
f pt = pt
    apply point_eq.
Defined.

(** And this functor "is" the same as the ordinary loop space functor. *)
Definition loops_functor_group
           {X Y : pType} (f : X ->* Y)
: fmap loops (group_loops_functor f) o loops_group X
  == loops_group Y o fmap loops f.
X, Y: pType
f: X ->* Y
fmap loops (group_loops_functor f) o loops_group X ==
loops_group Y o fmap loops f
Proof.
X, Y: pType
f: X ->* Y
fmap loops (group_loops_functor f) o loops_group X ==
loops_group Y o fmap loops f
  intros x.
X, Y: pType
f: X ->* Y
x: loops X
fmap loops (group_loops_functor f) (loops_group X x) =
loops_group Y (fmap loops f x)
  apply (equiv_inj (equiv_path_sigma_hprop _ _)^-1).
X, Y: pType
f: X ->* Y
x: loops X
(equiv_path_sigma_hprop pt pt)^-1
  (fmap loops (group_loops_functor f)
     (loops_group X x)) =
(equiv_path_sigma_hprop pt pt)^-1
  (loops_group Y (fmap loops f x))
  simpl.
X, Y: pType
f: X ->* Y
x: loops X
((path_sigma_hprop (f pt; tr (1 @ point_eq f)) pt
    (point_eq f))^ @
 (ap
    (fun X0 : {x : X & Tr (-1) (x = pt)} =>
     (f X0.1;
     Trunc_ind
       (fun _ : Trunc (-1) (X0.1 = pt) =>
        Tr (-1) (f X0.1 = pt))
       (fun p : X0.1 = pt => tr (ap f p @ point_eq f))
       X0.2))
    (path_sigma_hprop (pt; tr 1) (pt; tr 1) x) @
  path_sigma_hprop (f pt; tr (1 @ point_eq f)) pt
    (point_eq f))) ..1 =
(path_sigma_hprop (pt; tr 1) (pt; tr 1)
   ((point_eq f)^ @ (ap f x @ point_eq f))) ..1
  unfold pr1_path; rewrite !ap_pp.
X, Y: pType
f: X ->* Y
x: loops X
ap pr1
  (path_sigma_hprop (f pt; tr (1 @ point_eq f)) pt
     (point_eq f))^ @
(ap pr1
   (ap
      (fun X0 : {x : X & Tr (-1) (x = pt)} =>
       (f X0.1;
       Trunc_ind
         (fun _ : Trunc (-1) (X0.1 = pt) =>
          Tr (-1) (f X0.1 = pt))
         (fun p : X0.1 = pt =>
          tr (ap f p @ point_eq f)) X0.2))
      (path_sigma_hprop (pt; tr 1) (pt; tr 1) x)) @
 ap pr1
   (path_sigma_hprop (f pt; tr (1 @ point_eq f)) pt
      (point_eq f))) =
ap pr1
  (path_sigma_hprop (pt; tr 1) (pt; tr 1)
     ((point_eq f)^ @ (ap f x @ point_eq f)))
  rewrite ap_V, !ap_pr1_path_sigma_hprop.
X, Y: pType
f: X ->* Y
x: loops X
(point_eq f)^ @
(ap pr1
   (ap
      (fun X0 : {x : X & Tr (-1) (x = pt)} =>
       (f X0.1;
       Trunc_ind
         (fun _ : Trunc (-1) (X0.1 = pt) =>
          Tr (-1) (f X0.1 = pt))
         (fun p : X0.1 = pt =>
          tr (ap f p @ point_eq f)) X0.2))
      (path_sigma_hprop (pt; tr 1) (pt; tr 1) x)) @
 point_eq f) = (point_eq f)^ @ (ap f x @ point_eq f)
  apply whiskerL, whiskerR.
X, Y: pType
f: X ->* Y
x: loops X
ap pr1
  (ap
     (fun X0 : {x : X & Tr (-1) (x = pt)} =>
      (f X0.1;
      Trunc_ind
        (fun _ : Trunc (-1) (X0.1 = pt) =>
         Tr (-1) (f X0.1 = pt))
        (fun p : X0.1 = pt => tr (ap f p @ point_eq f))
        X0.2))
     (path_sigma_hprop (pt; tr 1) (pt; tr 1) x)) =
ap f x
  transitivity (ap (fun X0 : {x0 : X & merely (x0 = point X)} => f X0.1)
                   (path_sigma_hprop (point X; tr 1) (point X; tr 1) x)).
X, Y: pType
f: X ->* Y
x: loops X
ap pr1
  (ap
     (fun X0 : {x : X & Tr (-1) (x = pt)} =>
      (f X0.1;
      Trunc_ind
        (fun _ : Trunc (-1) (X0.1 = pt) =>
         Tr (-1) (f X0.1 = pt))
        (fun p : X0.1 = pt => tr (ap f p @ point_eq f))
        X0.2))
     (path_sigma_hprop (pt; tr 1) (pt; tr 1) x)) =
ap (fun X0 : {x0 : X & merely (x0 = pt)} => f X0.1)
  (path_sigma_hprop (pt; tr 1) (pt; tr 1) x)
X, Y: pType
f: X ->* Y
x: loops X
ap (fun X0 : {x0 : X & merely (x0 = pt)} => f X0.1)
  (path_sigma_hprop (pt; tr 1) (pt; tr 1) x) = ap f x
  -
X, Y: pType
f: X ->* Y
x: loops X
ap pr1
  (ap
     (fun X0 : {x : X & Tr (-1) (x = pt)} =>
      (f X0.1;
      Trunc_ind
        (fun _ : Trunc (-1) (X0.1 = pt) =>
         Tr (-1) (f X0.1 = pt))
        (fun p : X0.1 = pt => tr (ap f p @ point_eq f))
        X0.2))
     (path_sigma_hprop (pt; tr 1) (pt; tr 1) x)) =
ap (fun X0 : {x0 : X & merely (x0 = pt)} => f X0.1)
  (path_sigma_hprop (pt; tr 1) (pt; tr 1) x) match goal with
        |- ap ?f (ap ?g ?p) = ?z =>
        symmetry; refine (ap_compose g f p)
    end.
  -
X, Y: pType
f: X ->* Y
x: loops X
ap (fun X0 : {x0 : X & merely (x0 = pt)} => f X0.1)
  (path_sigma_hprop (pt; tr 1) (pt; tr 1) x) = ap f x rewrite ap_compose; apply ap.
X, Y: pType
f: X ->* Y
x: loops X
ap (fun x : {x0 : X & merely (x0 = pt)} => x.1)
  (path_sigma_hprop (pt; tr 1) (pt; tr 1) x) = x
    apply ap_pr1_path_sigma_hprop.
Qed.

Definition grouphom_compose {G H K : ooGroup}
           (psi : ooGroupHom H K) (phi : ooGroupHom G H)
: ooGroupHom G K
  := pmap_compose psi phi.

(** *** Functoriality *)

Definition group_loops_functor_compose
           {X Y Z : pType}
           (psi : Y ->* Z) (phi : X ->* Y)
: grouphom_compose (group_loops_functor psi) (group_loops_functor phi)
  == group_loops_functor (pmap_compose psi phi).
X, Y, Z: pType
psi: Y ->* Z
phi: X ->* Y
grouphom_compose (group_loops_functor psi)
  (group_loops_functor phi) ==
group_loops_functor (psi o* phi)
Proof.
X, Y, Z: pType
psi: Y ->* Z
phi: X ->* Y
grouphom_compose (group_loops_functor psi)
  (group_loops_functor phi) ==
group_loops_functor (psi o* phi)
  intros g.
X, Y, Z: pType
psi: Y ->* Z
phi: X ->* Y
g: group_loops X
grouphom_compose (group_loops_functor psi)
  (group_loops_functor phi) g =
group_loops_functor (psi o* phi) g
  unfold grouphom_fun, grouphom_compose.
X, Y, Z: pType
psi: Y ->* Z
phi: X ->* Y
g: group_loops X
fmap loops
  (group_loops_functor psi o* group_loops_functor phi)
  g = fmap loops (group_loops_functor (psi o* phi)) g
  refine (pointed_htpy (fmap_comp loops _ _) g @ _).
X, Y, Z: pType
psi: Y ->* Z
phi: X ->* Y
g: group_loops X
(fmap loops (group_loops_functor psi) $o
 fmap loops (group_loops_functor phi)) g =
fmap loops (group_loops_functor (psi o* phi)) g
  pose (p := eisretr (loops_group X) g).
X, Y, Z: pType
psi: Y ->* Z
phi: X ->* Y
g: group_loops X
p:= eisretr (loops_group X) g: (loops_group X o (loops_group X)^-1) g = idmap g
(fmap loops (group_loops_functor psi) $o
 fmap loops (group_loops_functor phi)) g =
fmap loops (group_loops_functor (psi o* phi)) g
  change (fmap loops (group_loops_functor psi)
            (fmap loops (group_loops_functor phi) g)
          = fmap loops (group_loops_functor
                                 (pmap_compose psi phi)) g).
X, Y, Z: pType
psi: Y ->* Z
phi: X ->* Y
g: group_loops X
p:= eisretr (loops_group X) g: (loops_group X o (loops_group X)^-1) g = idmap g
fmap loops (group_loops_functor psi)
  (fmap loops (group_loops_functor phi) g) =
fmap loops (group_loops_functor (psi o* phi)) g
  rewrite <- p.
X, Y, Z: pType
psi: Y ->* Z
phi: X ->* Y
g: group_loops X
p:= eisretr (loops_group X) g: (loops_group X o (loops_group X)^-1) g = idmap g
fmap loops (group_loops_functor psi)
  (fmap loops (group_loops_functor phi)
     (loops_group X ((loops_group X)^-1 g))) =
fmap loops (group_loops_functor (psi o* phi))
  (loops_group X ((loops_group X)^-1 g))
  rewrite !loops_functor_group.
X, Y, Z: pType
psi: Y ->* Z
phi: X ->* Y
g: group_loops X
p:= eisretr (loops_group X) g: (loops_group X o (loops_group X)^-1) g = idmap g
loops_group Z
  (fmap loops psi
     (fmap loops phi ((loops_group X)^-1 g))) =
loops_group Z
  (fmap loops (psi o* phi) ((loops_group X)^-1 g))
  apply ap.
X, Y, Z: pType
psi: Y ->* Z
phi: X ->* Y
g: group_loops X
p:= eisretr (loops_group X) g: (loops_group X o (loops_group X)^-1) g = idmap g
fmap loops psi (fmap loops phi ((loops_group X)^-1 g)) =
fmap loops (psi o* phi) ((loops_group X)^-1 g)
  symmetry; rapply (fmap_comp loops).
Qed.

Definition grouphom_idmap (G : ooGroup) : ooGroupHom G G
  := pmap_idmap.

Definition group_loops_functor_idmap {X : pType}
: grouphom_idmap (group_loops X)
  == group_loops_functor (Id (A:=pType) _).
X: pType
grouphom_idmap (group_loops X) ==
group_loops_functor (Id X)
Proof.
X: pType
grouphom_idmap (group_loops X) ==
group_loops_functor (Id X)
  intros g.
X: pType
g: group_loops X
grouphom_idmap (group_loops X) g =
group_loops_functor (Id X) g
  refine (fmap_id loops _ g @ _).
X: pType
g: group_loops X
Id (loops (B (group_loops X))) g =
group_loops_functor (Id X) g
  rewrite <- (eisretr (loops_group X) g).
X: pType
g: group_loops X
Id (loops (B (group_loops X)))
  (loops_group X ((loops_group X)^-1 g)) =
group_loops_functor (Id X)
  (loops_group X ((loops_group X)^-1 g))
  unfold grouphom_fun, grouphom_idmap.
X: pType
g: group_loops X
Id (loops (B (group_loops X)))
  (loops_group X ((loops_group X)^-1 g)) =
fmap loops (group_loops_functor (Id X))
  (loops_group X ((loops_group X)^-1 g))
  rewrite !loops_functor_group.
X: pType
g: group_loops X
Id (loops (B (group_loops X)))
  (loops_group X ((loops_group X)^-1 g)) =
loops_group X
  (fmap loops (Id X) ((loops_group X)^-1 g))
  exact (ap (loops_group X) (fmap_id loops _ _)^).
Qed.

(** *** Homomorphic properties *)

(** The following tactic often allows us to "pretend" that phi preserves basepoints strictly.  This is basically a simple extension of [pointed_reduce_rewrite] (see Pointed.v). *)
Ltac grouphom_reduce :=
  unfold grouphom_fun; cbn;
  repeat match goal with
           | [ G : ooGroup |- _ ] => destruct G as [G ?]
           | [ phi : ooGroupHom ?G ?H |- _ ] => destruct phi as [phi ?]
         end;
  pointed_reduce_rewrite.

Definition compose_grouphom {G H K : ooGroup}
           (psi : ooGroupHom H K) (phi : ooGroupHom G H)
: grouphom_compose psi phi == psi o phi.
G, H, K: ooGroup
psi: ooGroupHom H K
phi: ooGroupHom G H
grouphom_compose psi phi == psi o phi
Proof.
G, H, K: ooGroup
psi: ooGroupHom H K
phi: ooGroupHom G H
grouphom_compose psi phi == psi o phi
  intros g; grouphom_reduce.
G: Type
point1: IsPointed G
isconn_classifying_space2: IsConnected (Tr 0) G
H: Type
isconn_classifying_space1: IsConnected (Tr 0) H
K: Type
isconn_classifying_space0: IsConnected (Tr 0) K
psi: H -> K
phi: G -> H
g: {|
  classifying_space := [G, point1];
  isconn_classifying_space :=
    isconn_classifying_space2
|}
ap (fun x : G => psi (phi x)) g = ap psi (ap phi g)
  exact (ap_compose phi psi g).
Qed.

Definition idmap_grouphom (G : ooGroup)
: grouphom_idmap G == idmap.
G: ooGroup
grouphom_idmap G == idmap
Proof.
G: ooGroup
grouphom_idmap G == idmap
  intros g; grouphom_reduce.
G: Type
point: IsPointed G
isconn_classifying_space0: IsConnected (Tr 0) G
g: {|
  classifying_space := [G, point];
  isconn_classifying_space :=
    isconn_classifying_space0
|}
ap idmap g = g
  exact (ap_idmap g).
Qed.

Definition grouphom_pp {G H} (phi : ooGroupHom G H) (g1 g2 : G)
: phi (g1 @ g2) = phi g1 @ phi g2.
G, H: ooGroup
phi: ooGroupHom G H
g1, g2: G
phi (g1 @ g2) = phi g1 @ phi g2
Proof.
G, H: ooGroup
phi: ooGroupHom G H
g1, g2: G
phi (g1 @ g2) = phi g1 @ phi g2
  grouphom_reduce.
G: Type
point0: IsPointed G
isconn_classifying_space1: IsConnected (Tr 0) G
H: Type
isconn_classifying_space0: IsConnected (Tr 0) H
phi: G -> H
g1, g2: {|
  classifying_space := [G, point0];
  isconn_classifying_space :=
    isconn_classifying_space1
|}
ap phi (g1 @ g2) = ap phi g1 @ ap phi g2
  exact (ap_pp phi g1 g2).
Qed.

Definition grouphom_V {G H} (phi : ooGroupHom G H) (g : G)
: phi g^ = (phi g)^.
G, H: ooGroup
phi: ooGroupHom G H
g: G
phi g^ = (phi g)^
Proof.
G, H: ooGroup
phi: ooGroupHom G H
g: G
phi g^ = (phi g)^
  grouphom_reduce.
G: Type
point0: IsPointed G
isconn_classifying_space1: IsConnected (Tr 0) G
H: Type
isconn_classifying_space0: IsConnected (Tr 0) H
phi: G -> H
g: {|
  classifying_space := [G, point0];
  isconn_classifying_space :=
    isconn_classifying_space1
|}
ap phi g^ = (ap phi g)^
  exact (ap_V phi g).
Qed.

Definition grouphom_1 {G H} (phi : ooGroupHom G H)
: phi 1 = 1.
G, H: ooGroup
phi: ooGroupHom G H
phi 1 = 1
Proof.
G, H: ooGroup
phi: ooGroupHom G H
phi 1 = 1
  grouphom_reduce.
G: Type
point0: IsPointed G
isconn_classifying_space1: IsConnected (Tr 0) G
H: Type
isconn_classifying_space0: IsConnected (Tr 0) H
phi: G -> H
1 = 1
  reflexivity.
Qed.

Definition grouphom_pp_p {G H} (phi : ooGroupHom G H) (g1 g2 g3 : G)
: grouphom_pp phi (g1 @ g2) g3
  @ whiskerR (grouphom_pp phi g1 g2) (phi g3)
  @ concat_pp_p (phi g1) (phi g2) (phi g3)
  = ap phi (concat_pp_p g1 g2 g3)
    @ grouphom_pp phi g1 (g2 @ g3)
    @ whiskerL (phi g1) (grouphom_pp phi g2 g3).
G, H: ooGroup
phi: ooGroupHom G H
g1, g2, g3: G
(grouphom_pp phi (g1 @ g2) g3 @
 whiskerR (grouphom_pp phi g1 g2) (phi g3)) @
concat_pp_p (phi g1) (phi g2) (phi g3) =
(ap phi (concat_pp_p g1 g2 g3) @
 grouphom_pp phi g1 (g2 @ g3)) @
whiskerL (phi g1) (grouphom_pp phi g2 g3)
Proof.
G, H: ooGroup
phi: ooGroupHom G H
g1, g2, g3: G
(grouphom_pp phi (g1 @ g2) g3 @
 whiskerR (grouphom_pp phi g1 g2) (phi g3)) @
concat_pp_p (phi g1) (phi g2) (phi g3) =
(ap phi (concat_pp_p g1 g2 g3) @
 grouphom_pp phi g1 (g2 @ g3)) @
whiskerL (phi g1) (grouphom_pp phi g2 g3)
  grouphom_reduce.
G: Type
point0: IsPointed G
isconn_classifying_space1: IsConnected (Tr 0) G
H: Type
isconn_classifying_space0: IsConnected (Tr 0) H
phi: G -> H
g1, g2, g3: {|
  classifying_space := [G, point0];
  isconn_classifying_space :=
    isconn_classifying_space1
|}
(grouphom_pp {| pointed_fun := phi; dpoint_eq := 1 |}
   (g1 @ g2) g3 @
 whiskerR
   (grouphom_pp
      {| pointed_fun := phi; dpoint_eq := 1 |} g1 g2)
   (1 @ (ap phi g3 @ 1))) @
concat_pp_p (1 @ (ap phi g1 @ 1))
  (1 @ (ap phi g2 @ 1)) (1 @ (ap phi g3 @ 1)) =
(ap (fun p : point0 = point0 => 1 @ (ap phi p @ 1))
   (concat_pp_p g1 g2 g3) @
 grouphom_pp {| pointed_fun := phi; dpoint_eq := 1 |}
   g1 (g2 @ g3)) @
whiskerL (1 @ (ap phi g1 @ 1))
  (grouphom_pp
     {| pointed_fun := phi; dpoint_eq := 1 |} g2 g3)
Abort.

(** ** Subgroups *)

Section Subgroups.
  Context {G H : ooGroup} (incl : ooGroupHom H G) `{IsEmbedding incl}.

  (** A subgroup induces an equivalence relation on the ambient group, whose equivalence classes are called "cosets". *)
  Definition in_coset : G -> G -> Type
    := fun g1 g2 => hfiber incl (g1 @ g2^).

  Global Instance ishprop_in_coset : is_mere_relation G in_coset.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
is_mere_relation G in_coset
  Proof.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
is_mere_relation G in_coset
    exact _.
  Defined.

  Global Instance reflexive_coset : Reflexive in_coset.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
Reflexive in_coset
  Proof.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
Reflexive in_coset
    intros g.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g: G
in_coset g g
    exact (1 ; grouphom_1 incl @ (concat_pV g)^).
  Defined.

  Global Instance symmetric_coset : Symmetric in_coset.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
Symmetric in_coset
  Proof.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
Symmetric in_coset
    intros g1 g2 [h p].
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g1, g2: G
h: H
p: incl h = g1 @ g2^
in_coset g2 g1
    exists (h^).
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g1, g2: G
h: H
p: incl h = g1 @ g2^
incl h^ = g2 @ g1^
    refine (grouphom_V incl h @ inverse2 p @ inv_pp _ _ @ whiskerR (inv_V _) _).
  Defined.

  Global Instance transitive_coset : Transitive in_coset.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
Transitive in_coset
  Proof.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
Transitive in_coset
    intros g1 g2 g3 [h1 p1] [h2 p2].
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g1, g2, g3: G
h1: H
p1: incl h1 = g1 @ g2^
h2: H
p2: incl h2 = g2 @ g3^
in_coset g1 g3
    exists (h1 @ h2).
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g1, g2, g3: G
h1: H
p1: incl h1 = g1 @ g2^
h2: H
p2: incl h2 = g2 @ g3^
incl (h1 @ h2) = g1 @ g3^
    refine (grouphom_pp incl h1 h2
            @ (p1 @@ p2)
            @ concat_p_pp _ _ _
            @ whiskerR (concat_pV_p _ _) _).
  Defined.

  (** Every coset is equivalent (as a type) to the subgroup itself. *)
  Definition equiv_coset_subgroup (g : G)
  : { g' : G & in_coset g g'} <~> H.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g: G
{g' : G & in_coset g g'} <~> H
  Proof.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g: G
{g' : G & in_coset g g'} <~> H
    simple refine (equiv_adjointify _ _ _ _).
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g: G
{g' : G & in_coset g g'} -> H
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g: G
H -> {g' : G & in_coset g g'}
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g: G
?f o ?g == idmap
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g: G
?g o ?f == idmap
    -
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g: G
{g' : G & in_coset g g'} -> H intros [? [h ?]]; exact h.
    -
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g: G
H -> {g' : G & in_coset g g'} intros h; exists (incl h^ @ g); exists h; simpl.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g: G
h: H
incl h = g @ (incl h^ @ g)^
      abstract (rewrite inv_pp, grouphom_V, inv_V, concat_p_Vp; reflexivity).
    -
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g: G
(fun X : {g' : G & in_coset g g'} =>
 (fun (proj1 : G) (proj2 : in_coset g proj1) =>
  (fun (h : H) (_ : incl h = g @ proj1^) => h) proj2.1
    proj2.2) X.1 X.2)
o (fun h : H =>
   (incl h^ @ g; h;
   equiv_coset_subgroup_subproof g h
   :
   incl h = g @ (incl h^ @ g)^)) == idmap intros h; reflexivity.
    -
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g: G
(fun h : H =>
 (incl h^ @ g; h;
 equiv_coset_subgroup_subproof g h
 :
 incl h = g @ (incl h^ @ g)^))
o (fun X : {g' : G & in_coset g g'} =>
   (fun (proj1 : G) (proj2 : in_coset g proj1) =>
    (fun (h : H) (_ : incl h = g @ proj1^) => h)
      proj2.1 proj2.2) X.1 X.2) == idmap intros [g' [h p]].
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g, g': G
h: H
p: incl h = g @ g'^
(incl h^ @ g; h; equiv_coset_subgroup_subproof g h) =
(g'; h; p)
      apply path_sigma_hprop; simpl.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g, g': G
h: H
p: incl h = g @ g'^
incl h^ @ g = g'
      refine ((grouphom_V incl h @@ 1) @ _).
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g, g': G
h: H
p: incl h = g @ g'^
(incl h)^ @ g = g'
      apply moveR_Vp, moveL_pM.
G, H: ooGroup
incl: ooGroupHom H G
IsEmbedding0: IsEmbedding incl
g, g': G
h: H
p: incl h = g @ g'^
g @ g'^ = incl h exact (p^).
  Defined.

  Definition cosets := Quotient in_coset.

End Subgroups.

(** The wild category of oo-groups is induced by the wild category of pTypes *)

Global Instance isgraph_oogroup : IsGraph ooGroup
  := Build_IsGraph _ ooGroupHom.
Global Instance is01cat_oogroup : Is01Cat ooGroup
  := Build_Is01Cat _ _ grouphom_idmap (@grouphom_compose).
Global Instance is2graph_oogroup : Is2Graph ooGroup
  := is2graph_induced classifying_space.
Global Instance is1cat_oogroup : Is1Cat ooGroup
  := is1cat_induced classifying_space.

(** ** 1-groups as oo-groups *)

Definition group_to_oogroup : Group -> ooGroup
  := fun G => Build_ooGroup (pClassifyingSpace G) _.

Global Instance is0functor_group_to_oogroup : Is0Functor group_to_oogroup.
Is0Functor group_to_oogroup
Proof.
Is0Functor group_to_oogroup
  snrapply Build_Is0Functor.
forall a b : Group,
(a $-> b) -> group_to_oogroup a $-> group_to_oogroup b
  intros G H f.
G, H: Group
f: G $-> H
group_to_oogroup G $-> group_to_oogroup H
  by rapply (fmap pClassifyingSpace).
Defined.

Global Instance is1functor_group_to_oogroup : Is1Functor group_to_oogroup.
Is1Functor group_to_oogroup
Proof.
Is1Functor group_to_oogroup
  snrapply Build_Is1Functor; hnf; intros.
a, b: Group
f, g: a $-> b
X: f $== g
fmap group_to_oogroup f $== fmap group_to_oogroup g
a: Group
fmap group_to_oogroup (Id a) $==
Id (group_to_oogroup a)
a, b, c: Group
f: a $-> b
g: b $-> c
fmap group_to_oogroup (g $o f) $==
fmap group_to_oogroup g $o fmap group_to_oogroup f
  1: by rapply (fmap2 pClassifyingSpace).
a: Group
fmap group_to_oogroup (Id a) $==
Id (group_to_oogroup a)
a, b, c: Group
f: a $-> b
g: b $-> c
fmap group_to_oogroup (g $o f) $==
fmap group_to_oogroup g $o fmap group_to_oogroup f
  1: by rapply (fmap_id pClassifyingSpace).
a, b, c: Group
f: a $-> b
g: b $-> c
fmap group_to_oogroup (g $o f) $==
fmap group_to_oogroup g $o fmap group_to_oogroup f
  by rapply (fmap_comp pClassifyingSpace).
Defined.