Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Pointed.
Require Import Cubical.DPath.
Require Import Algebra.AbGroups.
Require Import Homotopy.Suspension.
Require Import Homotopy.ClassifyingSpace.
Require Import Homotopy.HSpace.Coherent.
Require Import Homotopy.HomotopyGroup.
Require Import Homotopy.Hopf.
Require Import Truncations.Core Truncations.Connectedness.
Require Import WildCat.

(* Formalisation of Eilenberg-MacLane spaces *)

Local Open Scope pointed_scope.
Local Open Scope nat_scope.
Local Open Scope mc_mult_scope.

(** The definition of the Eilenberg-Mac Lane spaces.  Note that while we allow [G] to be non-abelian for [n > 1], later results will need to assume that [G] is abelian. *)
Fixpoint EilenbergMacLane (G : Group) (n : nat) : pType
  := match n with
      | 0    => G
      | 1    => pClassifyingSpace G
      | m.+1 => pTr m.+1 (psusp (EilenbergMacLane G m))
     end.

Notation "'K(' G , n )" := (EilenbergMacLane G n).

Section EilenbergMacLane.
  Context `{Univalence}.

  Global Instance istrunc_em {G : Group} {n : nat} : IsTrunc n K(G, n).
H: Univalence
G: Group
n: nat
IsTrunc n K( G, n)
  Proof.
H: Univalence
G: Group
n: nat
IsTrunc n K( G, n)
    destruct n as [|[]]; exact _.
  Defined.

  (** This is subsumed by the next result, but Coq doesn't always find the next result when it should. *)
  Global Instance isconnected_em {G : Group} (n : nat)
    : IsConnected n K(G, n.+1).
H: Univalence
G: Group
n: nat
IsConnected (Tr n) K( G, n.+1)
  Proof.
H: Univalence
G: Group
n: nat
IsConnected (Tr n) K( G, n.+1)
    induction n; exact _.
  Defined.

  Global Instance isconnected_em' {G : Group} (n : nat)
    : IsConnected n.-1 K(G, n).
H: Univalence
G: Group
n: nat
IsConnected (Tr n.-1) K( G, n)
  Proof.
H: Univalence
G: Group
n: nat
IsConnected (Tr n.-1) K( G, n)
    destruct n.
H: Univalence
G: Group
IsConnected (Tr 0%nat.-1) K( G, 0)
H: Univalence
G: Group
n: nat
IsConnected (Tr (n.+1)%nat.-1) K( G, n.+1)
    1: exact (is_minus_one_connected_pointed _).
H: Univalence
G: Group
n: nat
IsConnected (Tr (n.+1)%nat.-1) K( G, n.+1)
    apply isconnected_em.
  Defined.

  Global Instance is0connected_em {G : Group} (n : nat)
    : IsConnected 0 K(G, n.+1).
H: Univalence
G: Group
n: nat
IsConnected (Tr 0%nat) K( G, n.+1)
  Proof.
H: Univalence
G: Group
n: nat
IsConnected (Tr 0%nat) K( G, n.+1)
    rapply (is0connected_isconnected n.-2).
  Defined.

  Local Open Scope trunc_scope.

  (* This is a variant of [pequiv_ptr_loop_psusp] from pSusp.v. All we are really using is that [n.+2 <= n +2+ n], but because of the use of [isconnmap_pred_add], the proof is a bit more specific to this case. *)
  Local Lemma pequiv_ptr_loop_psusp' (X : pType) (n : nat) `{IsConnected n.+1 X}
    : pTr n.+2 X <~>* pTr n.+2 (loops (psusp X)).
H: Univalence
X: pType
n: nat
H0: IsConnected (Tr n.+1) X
pTr n.+2 X <~>* pTr n.+2 (loops (psusp X))
  Proof.
H: Univalence
X: pType
n: nat
H0: IsConnected (Tr n.+1) X
pTr n.+2 X <~>* pTr n.+2 (loops (psusp X))
    snrapply Build_pEquiv.
H: Univalence
X: pType
n: nat
H0: IsConnected (Tr n.+1) X
pTr n.+2 X ->* pTr n.+2 (loops (psusp X))
H: Univalence
X: pType
n: nat
H0: IsConnected (Tr n.+1) X
IsEquiv ?pointed_equiv_fun
    1: rapply (fmap (pTr _) (loop_susp_unit _)).
H: Univalence
X: pType
n: nat
H0: IsConnected (Tr n.+1) X
IsEquiv (fmap (pTr n.+2) (loop_susp_unit X))
    nrapply O_inverts_conn_map.
H: Univalence
X: pType
n: nat
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr n.+2) (loop_susp_unit X)
    nrapply (isconnmap_pred_add n.-2).
H: Univalence
X: pType
n: nat
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr (n.-2 +2+ n.+2)) (loop_susp_unit X)
    rewrite 2 trunc_index_add_succ.
H: Univalence
X: pType
n: nat
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr (n.-2 +2+ n).+2) (loop_susp_unit X)
    apply (conn_map_loop_susp_unit n X).
  Defined.

  Lemma pequiv_loops_em_em (G : AbGroup) (n : nat)
    : K(G, n) <~>* loops K(G, n.+1).
H: Univalence
G: AbGroup
n: nat
K( G, n) <~>* loops K( G, n.+1)
  Proof.
H: Univalence
G: AbGroup
n: nat
K( G, n) <~>* loops K( G, n.+1)
    destruct n.
H: Univalence
G: AbGroup
K( G, 0) <~>* loops K( G, 1)
H: Univalence
G: AbGroup
n: nat
K( G, n.+1) <~>* loops K( G, n.+2)
    1: apply pequiv_g_loops_bg.
H: Univalence
G: AbGroup
n: nat
K( G, n.+1) <~>* loops K( G, n.+2)
    change (K(G, n.+1) <~>* loops (pTr n.+2 (psusp (K(G, n.+1))))).
H: Univalence
G: AbGroup
n: nat
K( G, n.+1) <~>* loops (pTr n.+2 (psusp K( G, n.+1)))
    refine (ptr_loops _ _ o*E _).
H: Univalence
G: AbGroup
n: nat
K( G, n.+1) <~>* pTr n.+1 (loops (psusp K( G, n.+1)))
    destruct n.
H: Univalence
G: AbGroup
K( G, 1) <~>* pTr 0%nat.+1 (loops (psusp K( G, 1)))
H: Univalence
G: AbGroup
n: nat
K( G, n.+2) <~>*
pTr (n.+1)%nat.+1 (loops (psusp K( G, n.+2)))
    1: srapply (licata_finster (m:=-2)).
H: Univalence
G: AbGroup
n: nat
K( G, n.+2) <~>*
pTr (n.+1)%nat.+1 (loops (psusp K( G, n.+2)))
    refine (_ o*E pequiv_ptr (n:=n.+2)).
H: Univalence
G: AbGroup
n: nat
pTr n.+2 K( G, n.+2) <~>*
pTr (n.+1)%nat.+1 (loops (psusp K( G, n.+2)))
    rapply pequiv_ptr_loop_psusp'.
  Defined.

  Definition pequiv_loops_em_g (G : AbGroup) (n : nat)
    : G <~>* iterated_loops n K(G, n).
H: Univalence
G: AbGroup
n: nat
G <~>* iterated_loops n K( G, n)
  Proof.
H: Univalence
G: AbGroup
n: nat
G <~>* iterated_loops n K( G, n)
    induction n.
H: Univalence
G: AbGroup
G <~>* iterated_loops 0 K( G, 0)
H: Univalence
G: AbGroup
n: nat
IHn: G <~>* iterated_loops n K( G, n)
G <~>* iterated_loops n.+1 K( G, n.+1)
    -
H: Univalence
G: AbGroup
G <~>* iterated_loops 0 K( G, 0) reflexivity.
    -
H: Univalence
G: AbGroup
n: nat
IHn: G <~>* iterated_loops n K( G, n)
G <~>* iterated_loops n.+1 K( G, n.+1) refine ((unfold_iterated_loops' _ _)^-1* o*E _ o*E IHn).
H: Univalence
G: AbGroup
n: nat
IHn: G <~>* iterated_loops n K( G, n)
iterated_loops n K( G, n) <~>*
iterated_loops n (loops K( G, n.+1))
      exact (emap (iterated_loops n) (pequiv_loops_em_em _ _)).
  Defined.

  (* For positive indices, we in fact get a group isomorphism. *)
  Definition equiv_g_pi_n_em (G : AbGroup) (n : nat)
    : GroupIsomorphism G (Pi n.+1 K(G, n.+1)).
H: Univalence
G: AbGroup
n: nat
GroupIsomorphism G (Pi n.+1 K( G, n.+1))
  Proof.
H: Univalence
G: AbGroup
n: nat
GroupIsomorphism G (Pi n.+1 K( G, n.+1))
    induction n.
H: Univalence
G: AbGroup
GroupIsomorphism G (Pi 1 K( G, 1))
H: Univalence
G: AbGroup
n: nat
IHn: GroupIsomorphism G (Pi n.+1 K( G, n.+1))
GroupIsomorphism G (Pi n.+2 K( G, n.+2))
    -
H: Univalence
G: AbGroup
GroupIsomorphism G (Pi 1 K( G, 1)) apply grp_iso_g_pi1_bg.
    -
H: Univalence
G: AbGroup
n: nat
IHn: GroupIsomorphism G (Pi n.+1 K( G, n.+1))
GroupIsomorphism G (Pi n.+2 K( G, n.+2)) nrefine (grp_iso_compose _ IHn).
H: Univalence
G: AbGroup
n: nat
IHn: GroupIsomorphism G (Pi n.+1 K( G, n.+1))
GroupIsomorphism (Pi n.+1 K( G, n.+1))
  (Pi n.+2 K( G, n.+2))
      nrefine (grp_iso_compose _ (groupiso_pi_functor _ (pequiv_loops_em_em _ _))).
H: Univalence
G: AbGroup
n: nat
IHn: GroupIsomorphism G (Pi n.+1 K( G, n.+1))
GroupIsomorphism (Pi n.+1 (loops K( G, n.+2)))
  (Pi n.+2 K( G, n.+2))
      symmetry; apply (groupiso_pi_loops _ _).
  Defined.

  Definition iscohhspace_em {G : AbGroup} (n : nat)
    : IsCohHSpace K(G, n).
H: Univalence
G: AbGroup
n: nat
IsCohHSpace K( G, n)
  Proof.
H: Univalence
G: AbGroup
n: nat
IsCohHSpace K( G, n)
    nrapply iscohhspace_equiv_cohhspace.
H: Univalence
G: AbGroup
n: nat
IsCohHSpace ?Goal
H: Univalence
G: AbGroup
n: nat
K( G, n) <~>* ?Goal
    2: apply pequiv_loops_em_em.
H: Univalence
G: AbGroup
n: nat
IsCohHSpace (loops K( G, n.+1))
    apply iscohhspace_loops.
  Defined.

End EilenbergMacLane.