From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
From HoTT.WildCat Require Import Core Universe Equiv.
Require Import Pointed.
Require Import Cubical.DPath.
Require Import Algebra.AbGroups.AbelianGroup.
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.

(** * Eilenberg-Mac Lane 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@{u v | u <= v} (G : Group@{u}) (n : nat) : pType@{v}
  := match n with
      | 0    => G
      | 1    => pClassifyingSpace@{u v} G
      | m.+1 => pTr m.+1 (psusp (EilenbergMacLane G m))
     end.

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

Section EilenbergMacLane.
  Context `{Univalence}.

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

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

  #[export] 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))
    snapply 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: exact (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))
    napply O_inverts_conn_map.
H: Univalence
X: pType
n: nat
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr n.+2) (loop_susp_unit X)
    napply (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)
    exact (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: exact 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) exact pequiv_pmap_idmap.
    -
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)) exact 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; exact (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)
    napply 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))
    exact iscohhspace_loops.
  Defined.

  (** If [G] and [G'] are isomorphic, then [K(G,n)] and [K(G',n)] are equivalent.  TODO:  We should show that [K(-,n)] is a functor, which implies this. *)
  Definition pequiv_em_group_iso {G G' : Group} (n : nat)
    (e : G $<~> G')
    : K(G, n) <~>* K(G', n).
H: Univalence
G, G': Group
n: nat
e: G $<~> G'
K( G, n) <~>* K( G', n)
  Proof.
H: Univalence
G, G': Group
n: nat
e: G $<~> G'
K( G, n) <~>* K( G', n)
    by destruct (equiv_path_group e).
  Defined.

  (** Every pointed (n-1)-connected n-type is an Eilenberg-Mac Lane space. *)
  Definition pequiv_em_connected_truncated (X : pType)
    (n : nat) `{IsConnected n X} `{IsTrunc n.+1 X}
    : K(Pi n.+1 X, n.+1) <~>* X.
H: Univalence
X: pType
n: nat
H0: IsConnected (Tr n) X
IsTrunc0: IsTrunc n.+1 X
K( Pi n.+1 X, n.+1) <~>* X
  Proof.
H: Univalence
X: pType
n: nat
H0: IsConnected (Tr n) X
IsTrunc0: IsTrunc n.+1 X
K( Pi n.+1 X, n.+1) <~>* X
    generalize dependent X; induction n; intros X isC isT.
H: Univalence
X: pType
isC: IsConnected (Tr 0%nat) X
isT: IsTrunc 0%nat.+1 X
K( Pi 1 X, 1) <~>* X
H: Univalence
n: nat
IHn: forall X0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 X0 -> K( Pi n.+1 X0, n.+1) <~>* X0
X: pType
isC: IsConnected (Tr n.+1%nat) X
isT: IsTrunc n.+1%nat.+1 X
K( Pi n.+2 X, n.+2) <~>* X
    1: rapply pequiv_pclassifyingspace_pi1.
H: Univalence
n: nat
IHn: forall X0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 X0 -> K( Pi n.+1 X0, n.+1) <~>* X0
X: pType
isC: IsConnected (Tr n.+1%nat) X
isT: IsTrunc n.+1%nat.+1 X
K( Pi n.+2 X, n.+2) <~>* X
    (* The equivalence will be the composite
<<
      K( (Pi n.+2 X) n.+2)
   <~>* K( (Pi n.+1 (loops X)), n.+2)
   = pTr n.+2 (psusp K( (Pi n.+1 (loops X)), n.+1))  [by definition]
   <~>* pTr n.+2 (psusp (loops X))                   [by induction]
   <~>* pTr n.+2 X
   <~>* X
>>
    and we'll work from right to left.
*)
    refine ((pequiv_ptr (n:=n.+2))^-1* o*E _).
H: Univalence
n: nat
IHn: forall X0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 X0 -> K( Pi n.+1 X0, n.+1) <~>* X0
X: pType
isC: IsConnected (Tr n.+1%nat) X
isT: IsTrunc n.+1%nat.+1 X
K( Pi n.+2 X, n.+2) <~>* pTr n.+2 X
    refine (pequiv_ptr_psusp_loops X n o*E _).
H: Univalence
n: nat
IHn: forall X0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 X0 -> K( Pi n.+1 X0, n.+1) <~>* X0
X: pType
isC: IsConnected (Tr n.+1%nat) X
isT: IsTrunc n.+1%nat.+1 X
K( Pi n.+2 X, n.+2) <~>* pTr n.+2 (psusp (loops X))
    change (K(?G, n.+2)) with (pTr n.+2 (psusp K( G, n.+1 ))).
H: Univalence
n: nat
IHn: forall X0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 X0 -> K( Pi n.+1 X0, n.+1) <~>* X0
X: pType
isC: IsConnected (Tr n.+1%nat) X
isT: IsTrunc n.+1%nat.+1 X
pTr n.+2 (psusp K( Pi n.+2 X, n.+1)) <~>* pTr n.+2 (psusp (loops X))
    refine (emap (pTr n.+2 o psusp) _).
H: Univalence
n: nat
IHn: forall X0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 X0 -> K( Pi n.+1 X0, n.+1) <~>* X0
X: pType
isC: IsConnected (Tr n.+1%nat) X
isT: IsTrunc n.+1%nat.+1 X
K( Pi n.+2 X, n.+1) $<~> loops X
    refine ((IHn (loops X) _ _) o*E _).
H: Univalence
n: nat
IHn: forall X0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 X0 -> K( Pi n.+1 X0, n.+1) <~>* X0
X: pType
isC: IsConnected (Tr n.+1%nat) X
isT: IsTrunc n.+1%nat.+1 X
K( Pi n.+2 X, n.+1) <~>* K( Pi n.+1 (loops X), n.+1)
    apply pequiv_em_group_iso.
H: Univalence
n: nat
IHn: forall X0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 X0 -> K( Pi n.+1 X0, n.+1) <~>* X0
X: pType
isC: IsConnected (Tr n.+1%nat) X
isT: IsTrunc n.+1%nat.+1 X
Pi n.+2 X $<~> Pi n.+1 (loops X)
    apply groupiso_pi_loops.
  Defined.

End EilenbergMacLane.