From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
From HoTT.WildCat Require Import Core Induced.
Require Import Colimits.Quotient.
Require Import Pointed.
Require Import Truncations.Core Truncations.Connectedness.
Require Import Homotopy.ClassifyingSpace.
Require Import Algebra.Groups.Group.

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

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; exact (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:= [{x0 : X & merely (x0 = 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:= [{x0 : X & merely (x0 = pt)}, (pt; tr 1)]: pType
x: X
p: x = pt
pt = (x; tr p)
  apply path_sigma_hprop; simpl.
X: pType
BG:= [{x0 : X & merely (x0 = 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)
  snapply 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)
{x0 : Y & Tr (-1) (x0 = 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 : {x0 : X & Tr (-1) (x0 = 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 : {x0 : X & Tr (-1) (x0 = 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 : {x0 : X & Tr (-1) (x0 = 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 : {x0 : X & Tr (-1) (x0 = 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 : {x0 : X & Tr (-1) (x0 = 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 : {x0 : X & Tr (-1) (x0 = 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; exact (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 x0 : {x0 : X & merely (x0 = pt)} => x0.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; tapply (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^).

  #[export] 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.

  #[export] 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.

  #[export] 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^
    exact (grouphom_V incl h @ inverse2 p @ inv_pp _ _ @ whiskerR (inv_V _) _).
  Defined.

  #[export] 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^
    exact (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 *)

Instance isgraph_oogroup : IsGraph ooGroup
  := Build_IsGraph _ ooGroupHom.
Instance is01cat_oogroup : Is01Cat ooGroup
  := Build_Is01Cat _ _ grouphom_idmap (@grouphom_compose).
Instance is2graph_oogroup : Is2Graph ooGroup
  := is2graph_induced classifying_space.
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) _.

Instance is0functor_group_to_oogroup : Is0Functor group_to_oogroup.
Is0Functor group_to_oogroup
Proof.
Is0Functor group_to_oogroup
  snapply 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 tapply (fmap pClassifyingSpace).
Defined.

Instance is1functor_group_to_oogroup : Is1Functor group_to_oogroup.
Is1Functor group_to_oogroup
Proof.
Is1Functor group_to_oogroup
  snapply 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 tapply (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 tapply (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 tapply (fmap_comp pClassifyingSpace).
Defined.