From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
From HoTT.WildCat Require Import Core Universe Equiv PointedCat Yoneda.
Require Import Pointed.
Require Import Algebra.AbGroups.AbelianGroup.
Require Import Homotopy.Suspension.
Require Import Homotopy.ClassifyingSpace.Core.
Import ClassifyingSpaceNotation.
Require Import Homotopy.HSpace.Coherent.
Require Import Homotopy.HomotopyGroup.
Require Import Homotopy.Hopf.
Require Import Modalities.Descent.
Require Import Truncations.Core Truncations.Connectedness Truncations.SeparatedTrunc.

(** * Eilenberg-Mac Lane spaces *)

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

(** ** Maps from connected types to pointed types *)

(** Before specializing to Eilenberg-Mac Lane spaces, we show that when [X] is [n]-connected and [Y] is [n.+1]-truncated, [fmap (Pi n.+1)] is an equivalence.  The case [n=1] is [isequiv_fmap_pi1_pmap], and the inductive step follows from [isequiv_fmap_loops_pmap]. *)

(** Part of the inductive step is factored out here. *)
Local Definition isequiv_fmap_pi_pmap_succ `{Univalence} (n : nat) {X Y : pType}
  (el : IsEquiv (fmap loops (a:=X) (b:=Y)))
  (e : IsEquiv (fmap (Pi n.+1) (a:=loops X) (b:=loops Y)))
  : IsEquiv (fmap (Pi n.+2) (a:=X) (b:=Y)).
H: Univalence
n: nat
X, Y: pType
el: IsEquiv (fmap loops)
e: IsEquiv (fmap (Pi n.+1))
IsEquiv (fmap (Pi n.+2))
Proof.
H: Univalence
n: nat
X, Y: pType
el: IsEquiv (fmap loops)
e: IsEquiv (fmap (Pi n.+1))
IsEquiv (fmap (Pi n.+2))
  pose (a := groupiso_pi_loops n X).
H: Univalence
n: nat
X, Y: pType
el: IsEquiv (fmap loops)
e: IsEquiv (fmap (Pi n.+1))
a:= groupiso_pi_loops n X: Pi n.+2 X $<~> Pi n.+1 (loops X)
IsEquiv (fmap (Pi n.+2))
  pose (b := groupiso_pi_loops n Y).
H: Univalence
n: nat
X, Y: pType
el: IsEquiv (fmap loops)
e: IsEquiv (fmap (Pi n.+1))
a:= groupiso_pi_loops n X: Pi n.+2 X $<~> Pi n.+1 (loops X)
b:= groupiso_pi_loops n Y: Pi n.+2 Y $<~> Pi n.+1 (loops Y)
IsEquiv (fmap (Pi n.+2))
  pose (k := equiv_precompose_cat_equiv a
              oE equiv_postcompose_cat_equiv (x:=Pi n.+1 (loops X)) b^-1$).
H: Univalence
n: nat
X, Y: pType
el: IsEquiv (fmap loops)
e: IsEquiv (fmap (Pi n.+1))
a:= groupiso_pi_loops n X: Pi n.+2 X $<~> Pi n.+1 (loops X)
b:= groupiso_pi_loops n Y: Pi n.+2 Y $<~> Pi n.+1 (loops Y)
k:= equiv_precompose_cat_equiv a oE equiv_postcompose_cat_equiv b^-1$: (Pi n.+1 (loops X) $-> Pi n.+1 (loops Y)) <~> (Pi n.+2 X $-> Pi n.+2 Y)
IsEquiv (fmap (Pi n.+2))
  refine (isequiv_homotopic (k o fmap (Pi n.+1) o fmap loops (a:=X) (b:=Y)) _).
H: Univalence
n: nat
X, Y: pType
el: IsEquiv (fmap loops)
e: IsEquiv (fmap (Pi n.+1))
a:= groupiso_pi_loops n X: Pi n.+2 X $<~> Pi n.+1 (loops X)
b:= groupiso_pi_loops n Y: Pi n.+2 Y $<~> Pi n.+1 (loops Y)
k:= equiv_precompose_cat_equiv a oE equiv_postcompose_cat_equiv b^-1$: (Pi n.+1 (loops X) $-> Pi n.+1 (loops Y)) <~> (Pi n.+2 X $-> Pi n.+2 Y)
(fun x : X $-> Y => k (fmap (Pi1 o iterated_loops n) (fmap loops x))) ==
fmap (Pi n.+2)
  intro f.
H: Univalence
n: nat
X, Y: pType
el: IsEquiv (fmap loops)
e: IsEquiv (fmap (Pi n.+1))
a:= groupiso_pi_loops n X: Pi n.+2 X $<~> Pi n.+1 (loops X)
b:= groupiso_pi_loops n Y: Pi n.+2 Y $<~> Pi n.+1 (loops Y)
k:= equiv_precompose_cat_equiv a oE equiv_postcompose_cat_equiv b^-1$: (Pi n.+1 (loops X) $-> Pi n.+1 (loops Y)) <~> (Pi n.+2 X $-> Pi n.+2 Y)
f: X $-> Y
k (fmap (Pi1 o iterated_loops n) (fmap loops f)) = fmap (Pi n.+2) f
  rapply equiv_path_grouphomomorphism.
H: Univalence
n: nat
X, Y: pType
el: IsEquiv (fmap loops)
e: IsEquiv (fmap (Pi n.+1))
a:= groupiso_pi_loops n X: Pi n.+2 X $<~> Pi n.+1 (loops X)
b:= groupiso_pi_loops n Y: Pi n.+2 Y $<~> Pi n.+1 (loops Y)
k:= equiv_precompose_cat_equiv a oE equiv_postcompose_cat_equiv b^-1$: (Pi n.+1 (loops X) $-> Pi n.+1 (loops Y)) <~> (Pi n.+2 X $-> Pi n.+2 Y)
f: X $-> Y
k (fmap (Pi1 o iterated_loops n) (fmap loops f)) == fmap (Pi n.+2) f
  intro x.
H: Univalence
n: nat
X, Y: pType
el: IsEquiv (fmap loops)
e: IsEquiv (fmap (Pi n.+1))
a:= groupiso_pi_loops n X: Pi n.+2 X $<~> Pi n.+1 (loops X)
b:= groupiso_pi_loops n Y: Pi n.+2 Y $<~> Pi n.+1 (loops Y)
k:= equiv_precompose_cat_equiv a oE equiv_postcompose_cat_equiv b^-1$: (Pi n.+1 (loops X) $-> Pi n.+1 (loops Y)) <~> (Pi n.+2 X $-> Pi n.+2 Y)
f: X $-> Y
x: Pi n.+2 X
k (fmap (Pi1 o iterated_loops n) (fmap loops f)) x = fmap (Pi n.+2) f x
  exact (moveR_equiv_V (f:=b) _ _ (fmap_pi_loops n.+1 f x)^).
Defined.

(** For [X] [n]-connected and [Y] [n.+1]-truncated, [fmap (Pi n.+1)] is an equivalence from the pointed maps [X ->* Y] to the group homomorphisms [Pi n.+1 X $-> Pi n.+1 Y].  Neither connectivity of [Y] nor truncatedness of [X] is needed.  The induction is on [n]: the successor step is [isequiv_fmap_loops_pmap], which applies since [n.+2 <= n +2+ n], and the base case is [isequiv_fmap_pi1_pmap]. *)
Instance isequiv_fmap_pi_pmap `{Univalence} (n : nat) (X Y : pType)
  `{cX : IsConnected n X} `{tY : IsTrunc n.+1 Y}
  : IsEquiv (fmap (Pi n.+1) (a:=X) (b:=Y)).
H: Univalence
n: nat
X, Y: pType
cX: IsConnected (Tr n) X
tY: IsTrunc n.+1 Y
IsEquiv (fmap (Pi n.+1))
Proof.
H: Univalence
n: nat
X, Y: pType
cX: IsConnected (Tr n) X
tY: IsTrunc n.+1 Y
IsEquiv (fmap (Pi n.+1))
  induction n in X, Y, cX, tY |- *.
H: Univalence
X, Y: pType
cX: IsConnected (Tr 0%nat) X
tY: IsTrunc 0%nat.+1 Y
IsEquiv (fmap (Pi 1))
H: Univalence
n: nat
X, Y: pType
cX: IsConnected (Tr n.+1%nat) X
tY: IsTrunc n.+1%nat.+1 Y
IHn: forall X0 Y0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 Y0 -> IsEquiv (fmap (Pi n.+1))
IsEquiv (fmap (Pi n.+2))
  1: exact (isequiv_fmap_pi1_pmap X Y).
H: Univalence
n: nat
X, Y: pType
cX: IsConnected (Tr n.+1%nat) X
tY: IsTrunc n.+1%nat.+1 Y
IHn: forall X0 Y0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 Y0 -> IsEquiv (fmap (Pi n.+1))
IsEquiv (fmap (Pi n.+2))
  napply isequiv_fmap_pi_pmap_succ.
H: Univalence
n: nat
X, Y: pType
cX: IsConnected (Tr n.+1%nat) X
tY: IsTrunc n.+1%nat.+1 Y
IHn: forall X0 Y0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 Y0 -> IsEquiv (fmap (Pi n.+1))
IsEquiv (fmap loops)
H: Univalence
n: nat
X, Y: pType
cX: IsConnected (Tr n.+1%nat) X
tY: IsTrunc n.+1%nat.+1 Y
IHn: forall X0 Y0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 Y0 -> IsEquiv (fmap (Pi n.+1))
IsEquiv (fmap (Pi n.+1))
  -
H: Univalence
n: nat
X, Y: pType
cX: IsConnected (Tr n.+1%nat) X
tY: IsTrunc n.+1%nat.+1 Y
IHn: forall X0 Y0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 Y0 -> IsEquiv (fmap (Pi n.+1))
IsEquiv (fmap loops) napply (isequiv_fmap_loops_pmap (n:=n)).
H: Univalence
n: nat
X, Y: pType
cX: IsConnected (Tr n.+1%nat) X
tY: IsTrunc n.+1%nat.+1 Y
IHn: forall X0 Y0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 Y0 -> IsEquiv (fmap (Pi n.+1))
IsConnected (Tr n.+1) X
H: Univalence
n: nat
X, Y: pType
cX: IsConnected (Tr n.+1%nat) X
tY: IsTrunc n.+1%nat.+1 Y
IHn: forall X0 Y0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 Y0 -> IsEquiv (fmap (Pi n.+1))
IsTrunc (n +2+ n) Y
    +
H: Univalence
n: nat
X, Y: pType
cX: IsConnected (Tr n.+1%nat) X
tY: IsTrunc n.+1%nat.+1 Y
IHn: forall X0 Y0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 Y0 -> IsEquiv (fmap (Pi n.+1))
IsConnected (Tr n.+1) X exact _.
    +
H: Univalence
n: nat
X, Y: pType
cX: IsConnected (Tr n.+1%nat) X
tY: IsTrunc n.+1%nat.+1 Y
IHn: forall X0 Y0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 Y0 -> IsEquiv (fmap (Pi n.+1))
IsTrunc (n +2+ n) Y apply (istrunc_leq (trunc_index_leq_add_nat n n)).
  -
H: Univalence
n: nat
X, Y: pType
cX: IsConnected (Tr n.+1%nat) X
tY: IsTrunc n.+1%nat.+1 Y
IHn: forall X0 Y0 : pType,
IsConnected (Tr n) X0 -> IsTrunc n.+1 Y0 -> IsEquiv (fmap (Pi n.+1))
IsEquiv (fmap (Pi n.+1)) rapply IHn.
Defined.

Definition equiv_fmap_pi_pmap `{Univalence} (n : nat) (X Y : pType)
  `{IsConnected n X} `{IsTrunc n.+1 Y}
  : (X ->* Y) <~> (Pi n.+1 X $-> Pi n.+1 Y)
  := Build_Equiv _ _ _ (isequiv_fmap_pi_pmap n X Y).

(** Pointed maps from an [n]-connected type to an [n.+1]-truncated type which agree on [Pi n.+1] are equal. *)
Definition path_pmap_pi_connected `{Univalence} (n : nat) {X Y : pType}
  `{IsConnected n X} `{IsTrunc n.+1 Y}
  (phi psi : X ->* Y)
  (h : fmap (Pi n.+1) phi == fmap (Pi n.+1) psi)
  : phi = psi.
H: Univalence
n: nat
X, Y: pType
H0: IsConnected (Tr n) X
IsTrunc0: IsTrunc n.+1 Y
phi, psi: X ->* Y
h: fmap (Pi n.+1) phi == fmap (Pi n.+1) psi
phi = psi
Proof.
H: Univalence
n: nat
X, Y: pType
H0: IsConnected (Tr n) X
IsTrunc0: IsTrunc n.+1 Y
phi, psi: X ->* Y
h: fmap (Pi n.+1) phi == fmap (Pi n.+1) psi
phi = psi
  tapply (equiv_inj (fmap (Pi n.+1) (a:=X) (b:=Y))).
H: Univalence
n: nat
X, Y: pType
H0: IsConnected (Tr n) X
IsTrunc0: IsTrunc n.+1 Y
phi, psi: X ->* Y
h: fmap (Pi n.+1) phi == fmap (Pi n.+1) psi
fmap (Pi n.+1) phi = fmap (Pi n.+1) psi
  exact (equiv_path_grouphomomorphism h).
Defined.

(** Two [n]-connected [n.+1]-truncated pointed types with isomorphic [Pi n.+1] are pointed equivalent. *)
Definition pequiv_pi_connected_truncated `{Univalence} (n : nat) {X Y : pType}
  `{IsConnected n X} `{IsTrunc n.+1 X} `{IsConnected n Y} `{IsTrunc n.+1 Y}
  (phi : GroupIsomorphism (Pi n.+1 X) (Pi n.+1 Y))
  : X <~>* Y
  := cate_reflect_fmap (Pi n.+1) (x:=X) (y:=Y) phi.

(** The equivalence induces the given isomorphism on [Pi n.+1]. *)
Definition fmap_pi_pequiv_pi_connected_truncated `{Univalence} (n : nat) {X Y : pType}
  `{IsConnected n X} `{IsTrunc n.+1 X} `{IsConnected n Y} `{IsTrunc n.+1 Y}
  (phi : GroupIsomorphism (Pi n.+1 X) (Pi n.+1 Y))
  : fmap (Pi n.+1) (pequiv_pi_connected_truncated n phi) == phi
  := fmap_cate_reflect_fmap (Pi n.+1) (x:=X) (y:=Y) phi.

(** ** Definition and properties of Eilenberg-Mac Lane spaces *)

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

  (** [K(-, n)] as a functor from groups to pointed types.  [fmap B] and the WildCat functoriality of [psusp] and [pTr] constrain the two groups to a single universe. *)
  Definition K' (n : nat) (G : Group) : pType := K(G, n).

  #[export] Instance is0functor_em (n : nat) : Is0Functor (K' n).
H: Univalence
n: nat
Is0Functor (K' n)
  Proof.
H: Univalence
n: nat
Is0Functor (K' n)
    napply Build_Is0Functor.
H: Univalence
n: nat
forall a b : Group, (a $-> b) -> K' n a $-> K' n b
    intros G G' f.
H: Univalence
n: nat
G, G': Group
f: G $-> G'
K' n G $-> K' n G'
    induction n as [|n IHn].
H: Univalence
G, G': Group
f: G $-> G'
K' 0 G $-> K' 0 G'
H: Univalence
n: nat
G, G': Group
f: G $-> G'
IHn: K' n G $-> K' n G'
K' n.+1 G $-> K' n.+1 G'
    -
H: Univalence
G, G': Group
f: G $-> G'
K' 0 G $-> K' 0 G' exact f.
    -
H: Univalence
n: nat
G, G': Group
f: G $-> G'
IHn: K' n G $-> K' n G'
K' n.+1 G $-> K' n.+1 G' destruct n as [|m].
H: Univalence
G, G': Group
f: G $-> G'
IHn: K' 0 G $-> K' 0 G'
K' 1 G $-> K' 1 G'
H: Univalence
m: nat
G, G': Group
f: G $-> G'
IHn: K' m.+1 G $-> K' m.+1 G'
K' m.+2 G $-> K' m.+2 G'
      +
H: Univalence
G, G': Group
f: G $-> G'
IHn: K' 0 G $-> K' 0 G'
K' 1 G $-> K' 1 G' exact (fmap B f).
      +
H: Univalence
m: nat
G, G': Group
f: G $-> G'
IHn: K' m.+1 G $-> K' m.+1 G'
K' m.+2 G $-> K' m.+2 G' exact (fmap (pTr m.+2) (fmap psusp IHn)).
  Defined.

  #[export] Instance is1functor_em (n : nat) : Is1Functor (K' n).
H: Univalence
n: nat
Is1Functor (K' n)
  Proof.
H: Univalence
n: nat
Is1Functor (K' n)
    napply Build_Is1Functor.
H: Univalence
n: nat
forall (a b : Group) (f g : a $-> b),
f $== g -> fmap (K' n) f $== fmap (K' n) g
H: Univalence
n: nat
forall a : Group, fmap (K' n) (Id a) $== Id (K' n a)
H: Univalence
n: nat
forall (a b c : Group) (f : a $-> b) (g : b $-> c),
fmap (K' n) (g $o f) $== fmap (K' n) g $o fmap (K' n) f
    -
H: Univalence
n: nat
forall (a b : Group) (f g : a $-> b),
f $== g -> fmap (K' n) f $== fmap (K' n) g intros G G' f g p.
H: Univalence
n: nat
G, G': Group
f, g: G $-> G'
p: f $== g
fmap (K' n) f $== fmap (K' n) g
      exact (phomotopy_path (ap (fmap (K' n))
                               (equiv_path_grouphomomorphism p))).
    -
H: Univalence
n: nat
forall a : Group, fmap (K' n) (Id a) $== Id (K' n a) intros G.
H: Univalence
n: nat
G: Group
fmap (K' n) (Id G) $== Id (K' n G)
      induction n as [|[|m] IH].
H: Univalence
G: Group
fmap (K' 0) (Id G) $== Id (K' 0 G)
H: Univalence
G: Group
IH: fmap (K' 0) (Id G) $== Id (K' 0 G)
fmap (K' 1) (Id G) $== Id (K' 1 G)
H: Univalence
m: nat
G: Group
IH: fmap (K' m.+1) (Id G) $== Id (K' m.+1 G)
fmap (K' m.+2) (Id G) $== Id (K' m.+2 G)
      +
H: Univalence
G: Group
fmap (K' 0) (Id G) $== Id (K' 0 G) rapply phomotopy_homotopy_hset.
H: Univalence
G: Group
fmap (K' 0) (Id G) == Id (K' 0 G)
        reflexivity.
      +
H: Univalence
G: Group
IH: fmap (K' 0) (Id G) $== Id (K' 0 G)
fmap (K' 1) (Id G) $== Id (K' 1 G) exact (fmap_id B G).
      +
H: Univalence
m: nat
G: Group
IH: fmap (K' m.+1) (Id G) $== Id (K' m.+1 G)
fmap (K' m.+2) (Id G) $== Id (K' m.+2 G) change (fmap (pTr m.+2) (fmap psusp (fmap (K' m.+1) (Id G))) ==* Id (K' m.+2 G)).
H: Univalence
m: nat
G: Group
IH: fmap (K' m.+1) (Id G) $== Id (K' m.+1 G)
fmap (pTr m.+2) (fmap psusp (fmap (K' m.+1) (Id G))) ==* Id (K' m.+2 G)
        refine (_ @* fmap_id (pTr m.+2) _).
H: Univalence
m: nat
G: Group
IH: fmap (K' m.+1) (Id G) $== Id (K' m.+1 G)
fmap (pTr m.+2) (fmap psusp (fmap (K' m.+1) (Id G))) ==*
fmap (pTr m.+2) (Id (psusp (K' m.+1 G)))
        tapply (fmap2 (pTr m.+2)).
H: Univalence
m: nat
G: Group
IH: fmap (K' m.+1) (Id G) $== Id (K' m.+1 G)
fmap psusp (fmap (K' m.+1) (Id G)) $== Id (psusp (K' m.+1 G))
        refine (_ @* fmap_id psusp _).
H: Univalence
m: nat
G: Group
IH: fmap (K' m.+1) (Id G) $== Id (K' m.+1 G)
fmap psusp (fmap (K' m.+1) (Id G)) ==* fmap psusp (Id (K' m.+1 G))
        tapply (fmap2 psusp).
H: Univalence
m: nat
G: Group
IH: fmap (K' m.+1) (Id G) $== Id (K' m.+1 G)
fmap (K' m.+1) (Id G) $== Id (K' m.+1 G)
        exact IH.
    -
H: Univalence
n: nat
forall (a b c : Group) (f : a $-> b) (g : b $-> c),
fmap (K' n) (g $o f) $== fmap (K' n) g $o fmap (K' n) f intros G G' G'' f g.
H: Univalence
n: nat
G, G', G'': Group
f: G $-> G'
g: G' $-> G''
fmap (K' n) (g $o f) $== fmap (K' n) g $o fmap (K' n) f
      induction n as [|[|m] IH].
H: Univalence
G, G', G'': Group
f: G $-> G'
g: G' $-> G''
fmap (K' 0) (g $o f) $== fmap (K' 0) g $o fmap (K' 0) f
H: Univalence
G, G', G'': Group
f: G $-> G'
g: G' $-> G''
IH: fmap (K' 0) (g $o f) $== fmap (K' 0) g $o fmap (K' 0) f
fmap (K' 1) (g $o f) $== fmap (K' 1) g $o fmap (K' 1) f
H: Univalence
m: nat
G, G', G'': Group
f: G $-> G'
g: G' $-> G''
IH: fmap (K' m.+1) (g $o f) $== fmap (K' m.+1) g $o fmap (K' m.+1) f
fmap (K' m.+2) (g $o f) $== fmap (K' m.+2) g $o fmap (K' m.+2) f
      +
H: Univalence
G, G', G'': Group
f: G $-> G'
g: G' $-> G''
fmap (K' 0) (g $o f) $== fmap (K' 0) g $o fmap (K' 0) f rapply phomotopy_homotopy_hset.
H: Univalence
G, G', G'': Group
f: G $-> G'
g: G' $-> G''
fmap (K' 0) (g $o f) == fmap (K' 0) g $o fmap (K' 0) f
        reflexivity.
      +
H: Univalence
G, G', G'': Group
f: G $-> G'
g: G' $-> G''
IH: fmap (K' 0) (g $o f) $== fmap (K' 0) g $o fmap (K' 0) f
fmap (K' 1) (g $o f) $== fmap (K' 1) g $o fmap (K' 1) f exact (fmap_comp B f g).
      +
H: Univalence
m: nat
G, G', G'': Group
f: G $-> G'
g: G' $-> G''
IH: fmap (K' m.+1) (g $o f) $== fmap (K' m.+1) g $o fmap (K' m.+1) f
fmap (K' m.+2) (g $o f) $== fmap (K' m.+2) g $o fmap (K' m.+2) f change (fmap (K' m.+2) ?f) with (fmap (pTr m.+2) (fmap psusp (fmap (K' m.+1) f))).
H: Univalence
m: nat
G, G', G'': Group
f: G $-> G'
g: G' $-> G''
IH: fmap (K' m.+1) (g $o f) $== fmap (K' m.+1) g $o fmap (K' m.+1) f
fmap (pTr m.+2) (fmap psusp (fmap (K' m.+1) (g $o f))) $==
fmap (pTr m.+2) (fmap psusp (fmap (K' m.+1) g)) $o
fmap (pTr m.+2) (fmap psusp (fmap (K' m.+1) f))
        refine (_ @* fmap_comp (pTr m.+2) _ _).
H: Univalence
m: nat
G, G', G'': Group
f: G $-> G'
g: G' $-> G''
IH: fmap (K' m.+1) (g $o f) $== fmap (K' m.+1) g $o fmap (K' m.+1) f
fmap (pTr m.+2) (fmap psusp (fmap (K' m.+1) (g $o f))) ==*
fmap (pTr m.+2)
  (fmap psusp (fmap (K' m.+1) g) $o fmap psusp (fmap (K' m.+1) f))
        tapply (fmap2 (pTr m.+2)).
H: Univalence
m: nat
G, G', G'': Group
f: G $-> G'
g: G' $-> G''
IH: fmap (K' m.+1) (g $o f) $== fmap (K' m.+1) g $o fmap (K' m.+1) f
fmap psusp (fmap (K' m.+1) (g $o f)) $==
fmap psusp (fmap (K' m.+1) g) $o fmap psusp (fmap (K' m.+1) f)
        refine (_ @* fmap_comp psusp _ _).
H: Univalence
m: nat
G, G', G'': Group
f: G $-> G'
g: G' $-> G''
IH: fmap (K' m.+1) (g $o f) $== fmap (K' m.+1) g $o fmap (K' m.+1) f
fmap psusp (fmap (K' m.+1) (g $o f)) ==*
fmap psusp (fmap (K' m.+1) g $o fmap (K' m.+1) f)
        tapply (fmap2 psusp).
H: Univalence
m: nat
G, G', G'': Group
f: G $-> G'
g: G' $-> G''
IH: fmap (K' m.+1) (g $o f) $== fmap (K' m.+1) g $o fmap (K' m.+1) f
fmap (K' m.+1) (g $o f) $== fmap (K' m.+1) g $o fmap (K' m.+1) f
        exact IH.
  Defined.

  (** TODO: Many results in this file, such as [pi_em_fmap] and [em_fmap_loops_natural], have a large number of universe variables.  These can be reduced by ending various definitions with Qed, but it would be better to fix the source of the explosion of universe variables. *)

  (** At positive levels, [pequiv_loops_em_em] is the canonical comparison map: the loop-suspension unit followed by [loops] of the truncation map.  This presentation makes its naturality transparent, without reference to the Hopf-construction input used to show that it is an equivalence. *)
  Definition loops_em_em_ptr_unit (G : AbGroup) (n : nat)
    : pequiv_loops_em_em G n.+1
      ==* fmap loops ptr o* loop_susp_unit K(G, n.+1).
H: Univalence
G: AbGroup
n: nat
pequiv_loops_em_em G n.+1 ==* fmap loops ptr o* loop_susp_unit K( G, n.+1)
  Proof.
H: Univalence
G: AbGroup
n: nat
pequiv_loops_em_em G n.+1 ==* fmap loops ptr o* loop_susp_unit K( G, n.+1)
    destruct n as [|n].
H: Univalence
G: AbGroup
pequiv_loops_em_em G 1 ==* fmap loops ptr o* loop_susp_unit K( G, 1)
H: Univalence
G: AbGroup
n: nat
pequiv_loops_em_em G n.+2 ==* fmap loops ptr o* loop_susp_unit K( G, n.+2)
    all: refine (compose_cate_fun (A:=pType) _ _ @* _).
H: Univalence
G: AbGroup
ptr_loops 0%nat.+1 (psusp K( G, 1)) $o licata_finster K( G, 1) ==*
fmap loops ptr o* loop_susp_unit K( G, 1)
H: Univalence
G: AbGroup
n: nat
ptr_loops n.+1%nat.+1 (psusp K( G, n.+2)) $o
(pequiv_ptr_loop_psusp' K( G, n.+2) n o*E pequiv_ptr) ==*
fmap loops ptr o* loop_susp_unit K( G, n.+2)
    all: refine (pmap_postwhisker _ (compose_cate_fun (A:=pType) _ _) @* _).
H: Univalence
G: AbGroup
ptr_loops 0%nat.+1 (psusp K( G, 1))
o* (pequiv_O_inverts (Tr (-1 +2+ -1).+1) (loop_susp_unit K( G, 1)) $o
    pequiv_ptr) ==*
fmap loops ptr o* loop_susp_unit K( G, 1)
H: Univalence
G: AbGroup
n: nat
ptr_loops n.+1%nat.+1 (psusp K( G, n.+2))
o* (pequiv_ptr_loop_psusp' K( G, n.+2) n $o pequiv_ptr) ==*
fmap loops ptr o* loop_susp_unit K( G, n.+2)
    1: refine (pmap_postwhisker _ (pto_O_natural (Tr _) _) @* _).
H: Univalence
G: AbGroup
ptr_loops 0%nat.+1 (psusp K( G, 1))
o* (pto (Tr 0%nat.+1) (loops (psusp K( G, 1))) o* loop_susp_unit K( G, 1)) ==*
fmap loops ptr o* loop_susp_unit K( G, 1)
H: Univalence
G: AbGroup
n: nat
ptr_loops n.+1%nat.+1 (psusp K( G, n.+2))
o* (pequiv_ptr_loop_psusp' K( G, n.+2) n $o pequiv_ptr) ==*
fmap loops ptr o* loop_susp_unit K( G, n.+2)
    2: refine (pmap_postwhisker _ (ptr_natural _ _) @* _).
H: Univalence
G: AbGroup
ptr_loops 0%nat.+1 (psusp K( G, 1))
o* (pto (Tr 0%nat.+1) (loops (psusp K( G, 1))) o* loop_susp_unit K( G, 1)) ==*
fmap loops ptr o* loop_susp_unit K( G, 1)
H: Univalence
G: AbGroup
n: nat
ptr_loops n.+1%nat.+1 (psusp K( G, n.+2))
o* (ptr o* loop_susp_unit K( G, n.+2)) ==*
fmap loops ptr o* loop_susp_unit K( G, n.+2)
    all: refine ((pmap_compose_assoc _ _ _)^* @* _).
H: Univalence
G: AbGroup
ptr_loops 0%nat.+1 (psusp K( G, 1))
o* pto (Tr 0%nat.+1) (loops (psusp K( G, 1))) o* loop_susp_unit K( G, 1) ==*
fmap loops ptr o* loop_susp_unit K( G, 1)
H: Univalence
G: AbGroup
n: nat
ptr_loops n.+1%nat.+1 (psusp K( G, n.+2)) o* ptr
o* loop_susp_unit K( G, n.+2) ==*
fmap loops ptr o* loop_susp_unit K( G, n.+2)
    all: exact (pmap_prewhisker _ (ptr_loops_commutes _ _)).
  Defined.

  (** [fmap (K' n)] commutes with the loop-space identifications, so it is a map of spectra. *)
  Definition em_fmap_loops_natural {G G' : AbGroup}
    (f : GroupHomomorphism G G') (n : nat)
    : fmap loops (fmap (K' n.+1) f) o* pequiv_loops_em_em G n
      ==* pequiv_loops_em_em G' n o* fmap (K' n) f.
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap loops (fmap (K' n.+1) f) o* pequiv_loops_em_em G n ==*
pequiv_loops_em_em G' n o* fmap (K' n) f
  Proof.
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap loops (fmap (K' n.+1) f) o* pequiv_loops_em_em G n ==*
pequiv_loops_em_em G' n o* fmap (K' n) f
    destruct n as [|n].
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
fmap loops (fmap (K' 1) f) o* pequiv_loops_em_em G 0 ==*
pequiv_loops_em_em G' 0 o* fmap (K' 0) f
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap loops (fmap (K' n.+2) f) o* pequiv_loops_em_em G n.+1 ==*
pequiv_loops_em_em G' n.+1 o* fmap (K' n.+1) f
    -
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
fmap loops (fmap (K' 1) f) o* pequiv_loops_em_em G 0 ==*
pequiv_loops_em_em G' 0 o* fmap (K' 0) f exact (pbloop_natural G G' f).
    -
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap loops (fmap (K' n.+2) f) o* pequiv_loops_em_em G n.+1 ==*
pequiv_loops_em_em G' n.+1 o* fmap (K' n.+1) f refine (pmap_postwhisker _ (loops_em_em_ptr_unit G n) @* _).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap loops (fmap (K' n.+2) f)
o* (fmap loops ptr o* loop_susp_unit K( G, n.+1)) ==*
pequiv_loops_em_em G' n.+1 o* fmap (K' n.+1) f
      refine (_ @* pmap_prewhisker _ (loops_em_em_ptr_unit G' n)^*).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap loops (fmap (K' n.+2) f)
o* (fmap loops ptr o* loop_susp_unit K( G, n.+1)) ==*
fmap loops ptr o* loop_susp_unit K( G', n.+1) o* fmap (K' n.+1) f
      refine ((pmap_compose_assoc _ _ _)^* @* _).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap loops (fmap (K' n.+2) f) o* fmap loops ptr o* loop_susp_unit K( G, n.+1) ==*
fmap loops ptr o* loop_susp_unit K( G', n.+1) o* fmap (K' n.+1) f
      refine (pmap_prewhisker _ (fmap_comp loops _ _)^* @* _).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap loops (fmap (K' n.+2) f $o ptr) o* loop_susp_unit K( G, n.+1) ==*
fmap loops ptr o* loop_susp_unit K( G', n.+1) o* fmap (K' n.+1) f
      refine (pmap_prewhisker _ (fmap2 loops (ptr_natural _ _)) @* _).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap loops
  (ptr
   o* fmap psusp
        (match
           n as n0
           return ((K' n0 G $-> K' n0 G') -> K' n0.+1 G $-> K' n0.+1 G')
         with
         | 0%nat => fun _ : K' 0 G $-> K' 0 G' => fmap B f
         | n0.+1%nat =>
             fun IHn : K' n0.+1 G $-> K' n0.+1 G' =>
             fmap (pTr n0.+2) (fmap psusp IHn)
         end
           ((fix F (n0 : nat) : K' n0 G $-> K' n0 G' :=
               match n0 as n1 return (K' n1 G $-> K' n1 G') with
               | 0%nat => f
               | n1.+1%nat =>
                   match
                     n1 as n2
                     return
                       ((K' n2 G $-> K' n2 G') -> K' n2.+1 G $-> K' n2.+1 G')
                   with
                   | 0%nat => fun _ : K' 0 G $-> K' 0 G' => fmap B f
                   | n2.+1%nat =>
                       fun IHn : K' n2.+1 G $-> K' n2.+1 G' =>
                       fmap (pTr n2.+2) (fmap psusp IHn)
                   end (F n1)
               end)
              n)))
o* loop_susp_unit K( G, n.+1) ==*
fmap loops ptr o* loop_susp_unit K( G', n.+1) o* fmap (K' n.+1) f
      refine (pmap_prewhisker _ (fmap_comp loops _ _) @* _).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap loops ptr $o
fmap loops
  (fmap psusp
     (match
        n as n0 return ((K' n0 G $-> K' n0 G') -> K' n0.+1 G $-> K' n0.+1 G')
      with
      | 0%nat => fun _ : K' 0 G $-> K' 0 G' => fmap B f
      | n0.+1%nat =>
          fun IHn : K' n0.+1 G $-> K' n0.+1 G' =>
          fmap (pTr n0.+2) (fmap psusp IHn)
      end
        ((fix F (n0 : nat) : K' n0 G $-> K' n0 G' :=
            match n0 as n1 return (K' n1 G $-> K' n1 G') with
            | 0%nat => f
            | n1.+1%nat =>
                match
                  n1 as n2
                  return
                    ((K' n2 G $-> K' n2 G') -> K' n2.+1 G $-> K' n2.+1 G')
                with
                | 0%nat => fun _ : K' 0 G $-> K' 0 G' => fmap B f
                | n2.+1%nat =>
                    fun IHn : K' n2.+1 G $-> K' n2.+1 G' =>
                    fmap (pTr n2.+2) (fmap psusp IHn)
                end (F n1)
            end)
           n)))
o* loop_susp_unit K( G, n.+1) ==*
fmap loops ptr o* loop_susp_unit K( G', n.+1) o* fmap (K' n.+1) f
      refine (pmap_compose_assoc _ _ _ @* _).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap loops ptr
o* (fmap loops
      (fmap psusp
         (match
            n as n0
            return ((K' n0 G $-> K' n0 G') -> K' n0.+1 G $-> K' n0.+1 G')
          with
          | 0%nat => fun _ : K' 0 G $-> K' 0 G' => fmap B f
          | n0.+1%nat =>
              fun IHn : K' n0.+1 G $-> K' n0.+1 G' =>
              fmap (pTr n0.+2) (fmap psusp IHn)
          end
            ((fix F (n0 : nat) : K' n0 G $-> K' n0 G' :=
                match n0 as n1 return (K' n1 G $-> K' n1 G') with
                | 0%nat => f
                | n1.+1%nat =>
                    match
                      n1 as n2
                      return
                        ((K' n2 G $-> K' n2 G') -> K' n2.+1 G $-> K' n2.+1 G')
                    with
                    | 0%nat => fun _ : K' 0 G $-> K' 0 G' => fmap B f
                    | n2.+1%nat =>
                        fun IHn : K' n2.+1 G $-> K' n2.+1 G' =>
                        fmap (pTr n2.+2) (fmap psusp IHn)
                    end (F n1)
                end)
               n)))
    o* loop_susp_unit K( G, n.+1)) ==*
fmap loops ptr o* loop_susp_unit K( G', n.+1) o* fmap (K' n.+1) f
      refine (pmap_postwhisker _ (loop_susp_unit_natural _)^* @* _).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap loops ptr
o* (loop_susp_unit
      match n with
      | 0%nat => pClassifyingSpace G'
      | _.+1%nat =>
          pTr n.+1
            (psusp
               ((fix EilenbergMacLane (G0 : Group) (n1 : nat) {struct n1} :
                     pType :=
                   match n1 with
                   | 0%nat => G0
                   | 1%nat => pClassifyingSpace G0
                   | (_.+1 as m).+1%nat =>
                       pTr m.+1 (psusp (EilenbergMacLane G0 m))
                   end)
                  G' n))
      end
    o* match
         n as n0
         return ((K' n0 G $-> K' n0 G') -> K' n0.+1 G $-> K' n0.+1 G')
       with
       | 0%nat => fun _ : K' 0 G $-> K' 0 G' => fmap B f
       | n0.+1%nat =>
           fun IHn : K' n0.+1 G $-> K' n0.+1 G' =>
           fmap (pTr n0.+2) (fmap psusp IHn)
       end
         ((fix F (n0 : nat) : K' n0 G $-> K' n0 G' :=
             match n0 as n1 return (K' n1 G $-> K' n1 G') with
             | 0%nat => f
             | n1.+1%nat =>
                 match
                   n1 as n2
                   return
                     ((K' n2 G $-> K' n2 G') -> K' n2.+1 G $-> K' n2.+1 G')
                 with
                 | 0%nat => fun _ : K' 0 G $-> K' 0 G' => fmap B f
                 | n2.+1%nat =>
                     fun IHn : K' n2.+1 G $-> K' n2.+1 G' =>
                     fmap (pTr n2.+2) (fmap psusp IHn)
                 end (F n1)
             end)
            n)) ==*
fmap loops ptr o* loop_susp_unit K( G', n.+1) o* fmap (K' n.+1) f
      exact (pmap_compose_assoc _ _ _)^*.
  Defined.

  (** [equiv_g_pi_n_em] at level [n.+1] unfolds to the level-[n] map conjugated by [groupiso_pi_loops] and [pequiv_loops_em_em]. *)
  Local Definition equiv_g_pi_n_em_succ (G : AbGroup) (n : nat) (x : G)
    : equiv_g_pi_n_em G n.+1 x
      = grp_iso_inverse (groupiso_pi_loops _ _)
          (groupiso_pi_functor _ (pequiv_loops_em_em G n.+1)
            (equiv_g_pi_n_em G n x))
    := idpath.

  (** The action of [fmap (K' n.+1) f] on [Pi n.+1] agrees with [f] under the identifications [equiv_g_pi_n_em]. *)
  Definition pi_em_fmap {G G' : AbGroup}
    (f : GroupHomomorphism G G') (n : nat)
    : fmap (Pi n.+1) (fmap (K' n.+1) f) o equiv_g_pi_n_em G n
      == equiv_g_pi_n_em G' n o f.
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap (Pi n.+1) (fmap (K' n.+1) f) o equiv_g_pi_n_em G n ==
equiv_g_pi_n_em G' n o f
  Proof.
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
fmap (Pi n.+1) (fmap (K' n.+1) f) o equiv_g_pi_n_em G n ==
equiv_g_pi_n_em G' n o f
    induction n as [|n IHn]; intro g.
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
g: G
fmap (Pi 1) (fmap (K' 1) f) (equiv_g_pi_n_em G 0 g) =
equiv_g_pi_n_em G' 0 (f g)
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
IHn: (fun x : G => fmap (Pi n.+1) (fmap (K' n.+1) f) (equiv_g_pi_n_em G n x)) ==
(fun x : G => equiv_g_pi_n_em G' n (f x))
g: G
fmap (Pi n.+2) (fmap (K' n.+2) f) (equiv_g_pi_n_em G n.+1 g) =
equiv_g_pi_n_em G' n.+1 (f g)
    -
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
g: G
fmap (Pi 1) (fmap (K' 1) f) (equiv_g_pi_n_em G 0 g) =
equiv_g_pi_n_em G' 0 (f g) exact (ap tr (bloop_natural G G' f g)).
    -
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
IHn: (fun x : G => fmap (Pi n.+1) (fmap (K' n.+1) f) (equiv_g_pi_n_em G n x)) ==
(fun x : G => equiv_g_pi_n_em G' n (f x))
g: G
fmap (Pi n.+2) (fmap (K' n.+2) f) (equiv_g_pi_n_em G n.+1 g) =
equiv_g_pi_n_em G' n.+1 (f g) lhs napply (ap _ (equiv_g_pi_n_em_succ G n g)).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
IHn: (fun x : G => fmap (Pi n.+1) (fmap (K' n.+1) f) (equiv_g_pi_n_em G n x)) ==
(fun x : G => equiv_g_pi_n_em G' n (f x))
g: G
fmap (Pi n.+2) (fmap (K' n.+2) f)
  (grp_iso_inverse (groupiso_pi_loops n K( G, n.+2))
     (groupiso_pi_functor n (pequiv_loops_em_em G n.+1)
        (equiv_g_pi_n_em G n g))) =
equiv_g_pi_n_em G' n.+1 (f g)
      rhs napply (equiv_g_pi_n_em_succ G' n (f g)).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
IHn: (fun x : G => fmap (Pi n.+1) (fmap (K' n.+1) f) (equiv_g_pi_n_em G n x)) ==
(fun x : G => equiv_g_pi_n_em G' n (f x))
g: G
fmap (Pi n.+2) (fmap (K' n.+2) f)
  (grp_iso_inverse (groupiso_pi_loops n K( G, n.+2))
     (groupiso_pi_functor n (pequiv_loops_em_em G n.+1)
        (equiv_g_pi_n_em G n g))) =
grp_iso_inverse (groupiso_pi_loops n K( G', n.+2))
  (groupiso_pi_functor n (pequiv_loops_em_em G' n.+1)
     (equiv_g_pi_n_em G' n (f g)))
      apply (equiv_inj (groupiso_pi_loops n _)).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
IHn: (fun x : G => fmap (Pi n.+1) (fmap (K' n.+1) f) (equiv_g_pi_n_em G n x)) ==
(fun x : G => equiv_g_pi_n_em G' n (f x))
g: G
groupiso_pi_loops n K( G', n.+2)
  (fmap (Pi n.+2) (fmap (K' n.+2) f)
     (grp_iso_inverse (groupiso_pi_loops n K( G, n.+2))
        (groupiso_pi_functor n (pequiv_loops_em_em G n.+1)
           (equiv_g_pi_n_em G n g)))) =
groupiso_pi_loops n K( G', n.+2)
  (grp_iso_inverse (groupiso_pi_loops n K( G', n.+2))
     (groupiso_pi_functor n (pequiv_loops_em_em G' n.+1)
        (equiv_g_pi_n_em G' n (f g))))
      rhs napply (eisretr (groupiso_pi_loops n _) _).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
IHn: (fun x : G => fmap (Pi n.+1) (fmap (K' n.+1) f) (equiv_g_pi_n_em G n x)) ==
(fun x : G => equiv_g_pi_n_em G' n (f x))
g: G
groupiso_pi_loops n K( G', n.+2)
  (fmap (Pi n.+2) (fmap (K' n.+2) f)
     (grp_iso_inverse (groupiso_pi_loops n K( G, n.+2))
        (groupiso_pi_functor n (pequiv_loops_em_em G n.+1)
           (equiv_g_pi_n_em G n g)))) =
groupiso_pi_functor n (pequiv_loops_em_em G' n.+1)
  (equiv_g_pi_n_em G' n (f g))
      lhs refine (fmap_pi_loops n.+1 (fmap (K' n.+2) f) _).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
IHn: (fun x : G => fmap (Pi n.+1) (fmap (K' n.+1) f) (equiv_g_pi_n_em G n x)) ==
(fun x : G => equiv_g_pi_n_em G' n (f x))
g: G
(fmap (pPi n.+1 o loops) (fmap (K' n.+2) f) o* pi_loops n.+1 (K' n.+2 G))
  (grp_iso_inverse (groupiso_pi_loops n K( G, n.+2))
     (groupiso_pi_functor n (pequiv_loops_em_em G n.+1)
        (equiv_g_pi_n_em G n g))) =
groupiso_pi_functor n (pequiv_loops_em_em G' n.+1)
  (equiv_g_pi_n_em G' n (f g))
      lhs napply (ap _ (eisretr (groupiso_pi_loops n _) _)).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
IHn: (fun x : G => fmap (Pi n.+1) (fmap (K' n.+1) f) (equiv_g_pi_n_em G n x)) ==
(fun x : G => equiv_g_pi_n_em G' n (f x))
g: G
fmap (pPi n.+1 o loops) (fmap (K' n.+2) f)
  (groupiso_pi_functor n (pequiv_loops_em_em G n.+1) (equiv_g_pi_n_em G n g)) =
groupiso_pi_functor n (pequiv_loops_em_em G' n.+1)
  (equiv_g_pi_n_em G' n (f g))
      lhs_V exact (fmap_comp (pPi n.+1)
          (pequiv_loops_em_em G n.+1 : _ ->* _)
          (fmap loops (fmap (K' n.+2) f)) (equiv_g_pi_n_em G n g)).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
IHn: (fun x : G => fmap (Pi n.+1) (fmap (K' n.+1) f) (equiv_g_pi_n_em G n x)) ==
(fun x : G => equiv_g_pi_n_em G' n (f x))
g: G
fmap (pPi n.+1) (fmap loops (fmap (K' n.+2) f) $o pequiv_loops_em_em G n.+1)
  (equiv_g_pi_n_em G n g) =
groupiso_pi_functor n (pequiv_loops_em_em G' n.+1)
  (equiv_g_pi_n_em G' n (f g))
      lhs exact (fmap2 (pPi n.+1) (em_fmap_loops_natural f n.+1)
          (equiv_g_pi_n_em G n g)).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
IHn: (fun x : G => fmap (Pi n.+1) (fmap (K' n.+1) f) (equiv_g_pi_n_em G n x)) ==
(fun x : G => equiv_g_pi_n_em G' n (f x))
g: G
fmap (pPi n.+1) (pequiv_loops_em_em G' n.+1 o* fmap (K' n.+1) f)
  (equiv_g_pi_n_em G n g) =
groupiso_pi_functor n (pequiv_loops_em_em G' n.+1)
  (equiv_g_pi_n_em G' n (f g))
      lhs exact (fmap_comp (pPi n.+1)
          (fmap (K' n.+1) f) (pequiv_loops_em_em G' n.+1 : _ ->* _)
          (equiv_g_pi_n_em G n g)).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
n: nat
IHn: (fun x : G => fmap (Pi n.+1) (fmap (K' n.+1) f) (equiv_g_pi_n_em G n x)) ==
(fun x : G => equiv_g_pi_n_em G' n (f x))
g: G
(fmap (pPi n.+1) (pequiv_loops_em_em G' n.+1) $o
 fmap (pPi n.+1) (fmap (K' n.+1) f)) (equiv_g_pi_n_em G n g) =
groupiso_pi_functor n (pequiv_loops_em_em G' n.+1)
  (equiv_g_pi_n_em G' n (f g))
      exact (ap _ (IHn g)).
  Defined.

  (** Equivalently, the composite is conjugation by the identifications [equiv_g_pi_n_em]. *)
  Definition pi_em_fmap' {G G' : AbGroup}
    (f : GroupHomomorphism G G') (n : nat)
    : fmap (Pi n.+1) (fmap (K' n.+1) f)
      == equiv_g_pi_n_em G' n o f o (equiv_g_pi_n_em G n)^-1
    := cate_moveL_eV (A:=Group) _ _ (equiv_g_pi_n_em G' n $o f) (pi_em_fmap f n).

  (** Eilenberg-Mac Lane spaces of a contractible group are contractible. *)
  #[export] Instance contr_em_contr {G : Group} `{Contr G} (n : nat)
    : Contr K(G, n).
H: Univalence
G: Group
Contr0: Contr G
n: nat
Contr K( G, n)
  Proof.
H: Univalence
G: Group
Contr0: Contr G
n: nat
Contr K( G, n)
    induction n as [|[|n] IHn].
H: Univalence
G: Group
Contr0: Contr G
Contr K( G, 0)
H: Univalence
G: Group
Contr0: Contr G
IHn: Contr K( G, 0)
Contr K( G, 1)
H: Univalence
G: Group
Contr0: Contr G
n: nat
IHn: Contr K( G, n.+1)
Contr K( G, n.+2)
    -
H: Univalence
G: Group
Contr0: Contr G
Contr K( G, 0) exact _.
    -
H: Univalence
G: Group
Contr0: Contr G
IHn: Contr K( G, 0)
Contr K( G, 1) exact _.
    -
H: Univalence
G: Group
Contr0: Contr G
n: nat
IHn: Contr K( G, n.+1)
Contr K( G, n.+2) rapply contr_O_contr.
  Defined.

  (** [K(-,n)] is a pointed functor. *)
  #[export] Instance ispointedfunctor_em (n : nat)
    : IsPointedFunctor (K' n).
H: Univalence
n: nat
IsPointedFunctor (K' n)
  Proof.
H: Univalence
n: nat
IsPointedFunctor (K' n)
    rapply Build_IsPointedFunctor'; cbn.
H: Univalence
n: nat
K' n grp_trivial $<~> pUnit
    snapply Build_pEquiv.
H: Univalence
n: nat
K' n grp_trivial ->* pUnit
H: Univalence
n: nat
IsEquiv ?pointed_equiv_fun
    1: exact pconst.
H: Univalence
n: nat
IsEquiv pconst
    rapply isequiv_contr_contr.
  Defined.


  (** [fmap (K' n.+1) f] of a surjective homomorphism is an [n]-connected map.  Both surjectivity of the map and of its [ap]s reduce to the previous level through the loop-space identifications. *)
  #[export] Instance isconnmap_em_fmap {G G' : AbGroup}
    (f : GroupHomomorphism G G') `{!IsSurjection f} (n : nat)
    : IsConnMap n (fmap (K' n.+1) f).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IsConnMap (Tr n) (fmap (K' n.+1) f)
  Proof.
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IsConnMap (Tr n) (fmap (K' n.+1) f)
    induction n as [|n IHn].
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
IsConnMap (Tr 0%nat) (fmap (K' 1) f)
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
IsConnMap (Tr n.+1%nat) (fmap (K' n.+2) f)
    -
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
IsConnMap (Tr 0%nat) (fmap (K' 1) f) exact (isconnmap_fmap_pclassifyingspace f).
    -
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
IsConnMap (Tr n.+1%nat) (fmap (K' n.+2) f) snapply isconnmap_isconnmap_ap_surj.
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
IsConnMap (Tr (-1)) (fmap (K' n.+2) f)
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
forall x y : K' n.+2 G,
IsConnMap (Tr (trunc_index_inc (-2) n.+1).+1) (ap (fmap (K' n.+2) f))
      +
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
IsConnMap (Tr (-1)) (fmap (K' n.+2) f) rapply (isconnmap_isconnected (-1)).
      +
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
forall x y : K' n.+2 G,
IsConnMap (Tr (trunc_index_inc (-2) n.+1).+1) (ap (fmap (K' n.+2) f)) assert (c : IsConnMap n (fmap loops (fmap (K' n.+2) f))).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
IsConnMap (Tr n) (fmap loops (fmap (K' n.+2) f))
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
c: IsConnMap (Tr n) (fmap loops (fmap (K' n.+2) f))
forall x y : K' n.+2 G,
IsConnMap (Tr (trunc_index_inc (-2) n.+1).+1) (ap (fmap (K' n.+2) f))
        {
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
IsConnMap (Tr n) (fmap loops (fmap (K' n.+2) f)) refine (conn_map_homotopic _
            ((pequiv_loops_em_em G' n.+1 o* fmap (K' n.+1) f)
             o* (pequiv_loops_em_em G n.+1)^-1*) _
            (fun p =>
              (moveL_pequiv_fV _ _ _ (em_fmap_loops_natural f n.+1))^* p) _). }
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
c: IsConnMap (Tr n) (fmap loops (fmap (K' n.+2) f))
forall x y : K' n.+2 G,
IsConnMap (Tr (trunc_index_inc (-2) n.+1).+1) (ap (fmap (K' n.+2) f))
        rapply (conn_point_elim (-1) (A:=K(G, n.+2))).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
c: IsConnMap (Tr n) (fmap loops (fmap (K' n.+2) f))
forall y : K' n.+2 G,
IsConnMap (Tr (trunc_index_inc (-2) n.+1).+1) (ap (fmap (K' n.+2) f))
        rapply (conn_point_elim (-1) (A:=K(G, n.+2))).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
c: IsConnMap (Tr n) (fmap loops (fmap (K' n.+2) f))
IsConnMap (Tr (trunc_index_inc (-2) n.+1).+1) (ap (fmap (K' n.+2) f))
        intro q.
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
c: IsConnMap (Tr n) (fmap loops (fmap (K' n.+2) f))
q: fmap (K' n.+2) f pt = fmap (K' n.+2) f pt
IsConnected (Tr (trunc_index_inc (-2) n.+1).+1)
  (hfiber (ap (fmap (K' n.+2) f)) q)
        pose (e2 := equiv_concat_l (point_eq (fmap (K' n.+2) f))^ _
                    oE equiv_concat_r (point_eq (fmap (K' n.+2) f)) _).
H: Univalence
G, G': AbGroup
f: GroupHomomorphism G G'
IsSurjection0: IsConnMap (Tr (-1)) f
n: nat
IHn: IsConnMap (Tr n) (fmap (K' n.+1) f)
c: IsConnMap (Tr n) (fmap loops (fmap (K' n.+2) f))
q: fmap (K' n.+2) f pt = fmap (K' n.+2) f pt
e2:= equiv_concat_l (point_eq (fmap (K' n.+2) f))^ pt
oE equiv_concat_r (point_eq (fmap (K' n.+2) f)) (fmap (K' n.+2) f pt): fmap (K' n.+2) f pt = fmap (K' n.+2) f pt <~> pt = pt
IsConnected (Tr (trunc_index_inc (-2) n.+1).+1)
  (hfiber (ap (fmap (K' n.+2) f)) q)
        exact (isconnected_equiv' n _
                 (equiv_functor_sigma_id (fun p => equiv_ap e2 _ _))^-1%equiv
                 (c _)).
  Defined.

  (** [fmap (K' n.+1)] is an equivalence from group homomorphisms to pointed maps.  Since [K(G, n.+1)] is [n]-connected and [K(G', n.+1)] is [n.+1]-truncated, [fmap (Pi n.+1)] is an equivalence from the pointed maps to the group homomorphisms [Pi n.+1 K(G, n.+1) $-> Pi n.+1 K(G', n.+1)], and by [pi_em_fmap'] the composite with [fmap (K' n.+1)] is conjugation by the identifications [equiv_g_pi_n_em], which is also an equivalence.  In particular, pointed maps between Eilenberg-Mac Lane spaces of the same level are determined by their effect on homotopy groups. *)
  #[export] Instance isequiv_em_fmap (G G' : AbGroup) (n : nat)
    : IsEquiv (fun f : GroupHomomorphism G G' => fmap (K' n.+1) f).
H: Univalence
G, G': AbGroup
n: nat
IsEquiv (fun f : GroupHomomorphism G G' => fmap (K' n.+1) f)
  Proof.
H: Univalence
G, G': AbGroup
n: nat
IsEquiv (fun f : GroupHomomorphism G G' => fmap (K' n.+1) f)
    refine (isequiv_commsq' _
              (equiv_precompose_cat_equiv (A:=Group)
                 (grp_iso_inverse (equiv_g_pi_n_em G n)))
              (equiv_postcompose_cat_equiv (A:=Group) (equiv_g_pi_n_em G' n))
              (fmap (Pi n.+1)) _).
H: Univalence
G, G': AbGroup
n: nat
(fun x : G $-> G' =>
 equiv_precompose_cat_equiv (grp_iso_inverse (equiv_g_pi_n_em G n))
   (equiv_postcompose_cat_equiv (equiv_g_pi_n_em G' n) x)) ==
(fun x : G $-> G' => fmap (Pi n.+1) (fmap (K' n.+1) x))
    intro f.
H: Univalence
G, G': AbGroup
n: nat
f: G $-> G'
equiv_precompose_cat_equiv (grp_iso_inverse (equiv_g_pi_n_em G n))
  (equiv_postcompose_cat_equiv (equiv_g_pi_n_em G' n) f) =
fmap (Pi n.+1) (fmap (K' n.+1) f)
    apply equiv_path_grouphomomorphism; symmetry.
H: Univalence
G, G': AbGroup
n: nat
f: G $-> G'
fmap (Pi n.+1) (fmap (K' n.+1) f) ==
equiv_precompose_cat_equiv (grp_iso_inverse (equiv_g_pi_n_em G n))
  (equiv_postcompose_cat_equiv (equiv_g_pi_n_em G' n) f)
    apply pi_em_fmap'.
  Defined.

  (** The equivalence between group homomorphisms and pointed maps of Eilenberg-Mac Lane spaces. *)
  Definition equiv_em_fmap (G G' : AbGroup) (n : nat)
    : GroupHomomorphism G G' <~> (K(G, n.+1) ->* K(G', n.+1))
    := Build_Equiv _ _ _ (isequiv_em_fmap G G' n).

  (** The canonical identification of [Pi n.+1 K(Pi n.+1 X, n.+1)] with [Pi n.+1 X].  For [n = 0] this is [grp_iso_g_pi1_bg], and for positive [n] it is [equiv_g_pi_n_em] applied to the abelian group [Pi n.+1 X]. *)
  Definition grp_iso_pi_em_pi (X : pType) (n : nat)
    : GroupIsomorphism (Pi n.+1 K(Pi n.+1 X, n.+1)) (Pi n.+1 X).
H: Univalence
X: pType
n: nat
GroupIsomorphism (Pi n.+1 K( Pi n.+1 X, n.+1)) (Pi n.+1 X)
  Proof.
H: Univalence
X: pType
n: nat
GroupIsomorphism (Pi n.+1 K( Pi n.+1 X, n.+1)) (Pi n.+1 X)
    symmetry.
H: Univalence
X: pType
n: nat
GroupIsomorphism (Pi n.+1 X) (Pi n.+1 K( Pi n.+1 X, n.+1))
    destruct n as [|m].
H: Univalence
X: pType
GroupIsomorphism (Pi 1 X) (Pi 1 K( Pi 1 X, 1))
H: Univalence
X: pType
m: nat
GroupIsomorphism (Pi m.+2 X) (Pi m.+2 K( Pi m.+2 X, m.+2))
    -
H: Univalence
X: pType
GroupIsomorphism (Pi 1 X) (Pi 1 K( Pi 1 X, 1)) exact grp_iso_g_pi1_bg.
    -
H: Univalence
X: pType
m: nat
GroupIsomorphism (Pi m.+2 X) (Pi m.+2 K( Pi m.+2 X, m.+2)) exact (equiv_g_pi_n_em (Build_AbGroup (Pi m.+2 X) _) m.+1).
  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
    := pequiv_pi_connected_truncated n (grp_iso_pi_em_pi X n).

  (** It induces [grp_iso_pi_em_pi] on [Pi n.+1]. *)
  Definition fmap_pi_pequiv_em_connected_truncated (X : pType)
    (n : nat) `{IsConnected n X} `{IsTrunc n.+1 X}
    : fmap (Pi n.+1) (pequiv_em_connected_truncated X n) == grp_iso_pi_em_pi X n
    := fmap_pi_pequiv_pi_connected_truncated n (grp_iso_pi_em_pi X n).

End EilenbergMacLane.

(** ** Delooping Eilenberg-Mac Lane mapping types *)

Section Deloop.
  Context `{Univalence} (B A : AbGroup@{u}) (n : nat).

  (** [Pi n.+4 (psusp K(B,n.+2))] is trivial. *)
  Local Instance contr_pi_psusp_em : Contr (Pi n.+4 (psusp K(B, n.+2))).
H: Univalence
B, A: AbGroup
n: nat
Contr (Pi n.+4 (psusp K( B, n.+2)))
  Proof.
H: Univalence
B, A: AbGroup
n: nat
Contr (Pi n.+4 (psusp K( B, n.+2)))
    nrefine (contr_equiv' (Pi n.+3 (loops (psusp K(B, n.+2)))) _).
H: Univalence
B, A: AbGroup
n: nat
Pi n.+3 (loops (psusp K( B, n.+2))) <~> Pi n.+4 (psusp K( B, n.+2))
H: Univalence
B, A: AbGroup
n: nat
Contr (Pi n.+3 (loops (psusp K( B, n.+2))))
    1: exact (groupiso_pi_loops n.+2 (psusp K(B, n.+2)))^-1%equiv.
H: Univalence
B, A: AbGroup
n: nat
Contr (Pi n.+3 (loops (psusp K( B, n.+2))))
    (* Since [Pi n.+3] is a set, it's enough to show it's 0-connected. *)
    napply (contr_trunc_conn 0); only 1: exact _.
H: Univalence
B, A: AbGroup
n: nat
IsConnected (Tr 0%nat) (Pi n.+3 (loops (psusp K( B, n.+2))))
    (* And for that, it's enough to show it's the target of a (-1)-connected map from a 0-connected type. *)
    pose (fu := fmap (pPi n.+3) (loop_susp_unit K(B, n.+2))).
H: Univalence
B, A: AbGroup
n: nat
fu:= fmap (pPi n.+3) (loop_susp_unit K( B, n.+2)): pPi n.+3 K( B, n.+2) $-> pPi n.+3 (loops (psusp K( B, n.+2)))
IsConnected (Tr 0%nat) (Pi n.+3 (loops (psusp K( B, n.+2))))
    napply (OO_isconnected_from_conn_map 0 (Tr (-1)) fu).
H: Univalence
B, A: AbGroup
n: nat
fu:= fmap (pPi n.+3) (loop_susp_unit K( B, n.+2)): pPi n.+3 K( B, n.+2) $-> pPi n.+3 (loops (psusp K( B, n.+2)))
Tr (-1) <= Tr 0%nat
H: Univalence
B, A: AbGroup
n: nat
fu:= fmap (pPi n.+3) (loop_susp_unit K( B, n.+2)): pPi n.+3 K( B, n.+2) $-> pPi n.+3 (loops (psusp K( B, n.+2)))
Tr 0%nat <= Sep (Tr (-1))
H: Univalence
B, A: AbGroup
n: nat
fu:= fmap (pPi n.+3) (loop_susp_unit K( B, n.+2)): pPi n.+3 K( B, n.+2) $-> pPi n.+3 (loops (psusp K( B, n.+2)))
IsConnected (Tr 0%nat) (pPi n.+3 K( B, n.+2))
H: Univalence
B, A: AbGroup
n: nat
fu:= fmap (pPi n.+3) (loop_susp_unit K( B, n.+2)): pPi n.+3 K( B, n.+2) $-> pPi n.+3 (loops (psusp K( B, n.+2)))
IsConnMap (Tr (-1)) fu
    1, 2: exact _.
H: Univalence
B, A: AbGroup
n: nat
fu:= fmap (pPi n.+3) (loop_susp_unit K( B, n.+2)): pPi n.+3 K( B, n.+2) $-> pPi n.+3 (loops (psusp K( B, n.+2)))
IsConnected (Tr 0%nat) (pPi n.+3 K( B, n.+2))
H: Univalence
B, A: AbGroup
n: nat
fu:= fmap (pPi n.+3) (loop_susp_unit K( B, n.+2)): pPi n.+3 K( B, n.+2) $-> pPi n.+3 (loops (psusp K( B, n.+2)))
IsConnMap (Tr (-1)) fu
    -
H: Univalence
B, A: AbGroup
n: nat
fu:= fmap (pPi n.+3) (loop_susp_unit K( B, n.+2)): pPi n.+3 K( B, n.+2) $-> pPi n.+3 (loops (psusp K( B, n.+2)))
IsConnected (Tr 0%nat) (pPi n.+3 K( B, n.+2)) napply isconnected_contr.
H: Univalence
B, A: AbGroup
n: nat
fu:= fmap (pPi n.+3) (loop_susp_unit K( B, n.+2)): pPi n.+3 K( B, n.+2) $-> pPi n.+3 (loops (psusp K( B, n.+2)))
Contr (pPi n.+3 K( B, n.+2))
      rapply contr_pi_succ_istrunc.
    -
H: Univalence
B, A: AbGroup
n: nat
fu:= fmap (pPi n.+3) (loop_susp_unit K( B, n.+2)): pPi n.+3 K( B, n.+2) $-> pPi n.+3 (loops (psusp K( B, n.+2)))
IsConnMap (Tr (-1)) fu apply (issurj_pi_connmap n.+2).
H: Univalence
B, A: AbGroup
n: nat
fu:= fmap (pPi n.+3) (loop_susp_unit K( B, n.+2)): pPi n.+3 K( B, n.+2) $-> pPi n.+3 (loops (psusp K( B, n.+2)))
IsConnMap (Tr n.+2%nat) (loop_susp_unit K( B, n.+2))
      napply (isconnmap_pred_add n.-2).
H: Univalence
B, A: AbGroup
n: nat
fu:= fmap (pPi n.+3) (loop_susp_unit K( B, n.+2)): pPi n.+3 K( B, n.+2) $-> pPi n.+3 (loops (psusp K( B, n.+2)))
IsConnMap (Tr (n.-2 +2+ n.+2%nat)) (loop_susp_unit K( B, n.+2))
      rewrite 2 trunc_index_add_succ.
H: Univalence
B, A: AbGroup
n: nat
fu:= fmap (pPi n.+3) (loop_susp_unit K( B, n.+2)): pPi n.+3 K( B, n.+2) $-> pPi n.+3 (loops (psusp K( B, n.+2)))
IsConnMap (Tr (n.-2 +2+ trunc_index_inc (-2) n.+2).+2)
  (loop_susp_unit K( B, n.+2))
      exact (conn_map_loop_susp_unit n K(B, n.+2)).
  Defined.

  (** [pTr n.+4 (psusp K(B,n.+2))] is [n.+3]-truncated. *)
  Local Instance istrunc_ptr_psusp_em
    : IsTrunc n.+3 (pTr n.+4 (psusp K(B, n.+2))).
H: Univalence
B, A: AbGroup
n: nat
IsTrunc n.+3 (pTr n.+4 (psusp K( B, n.+2)))
  Proof.
H: Univalence
B, A: AbGroup
n: nat
IsTrunc n.+3 (pTr n.+4 (psusp K( B, n.+2)))
    napply (istrunc_contr_pi n.+3).
H: Univalence
B, A: AbGroup
n: nat
IsConnected (Tr 0%nat) (pTr n.+4 (psusp K( B, n.+2)))
H: Univalence
B, A: AbGroup
n: nat
IsTrunc n.+3%nat.+1 (pTr n.+4 (psusp K( B, n.+2)))
H: Univalence
B, A: AbGroup
n: nat
Contr (Pi n.+4 (pTr n.+4 (psusp K( B, n.+2))))
    1,2: exact _.
H: Univalence
B, A: AbGroup
n: nat
Contr (Pi n.+4 (pTr n.+4 (psusp K( B, n.+2))))
    exact (contr_equiv' _ (grp_iso_pi_Tr n.+3 (psusp K(B, n.+2)))).
  Defined.

  (** [K(B, n.+3)] is the [n.+3]-truncation of [pTr n.+4 (psusp K(B, n.+2))]. *)
  Local Definition pequiv_ptr_ptr_psusp_em
    : K(B, n.+3) <~>* pTr n.+3 (pTr n.+4 (psusp K(B, n.+2))).
H: Univalence
B, A: AbGroup
n: nat
K( B, n.+3) <~>* pTr n.+3 (pTr n.+4 (psusp K( B, n.+2)))
  Proof.
H: Univalence
B, A: AbGroup
n: nat
K( B, n.+3) <~>* pTr n.+3 (pTr n.+4 (psusp K( B, n.+2)))
    snapply Build_pEquiv'.
H: Univalence
B, A: AbGroup
n: nat
K( B, n.+3) <~> pTr n.+3 (pTr n.+4 (psusp K( B, n.+2)))
H: Univalence
B, A: AbGroup
n: nat
?f pt = pt
    -
H: Univalence
B, A: AbGroup
n: nat
K( B, n.+3) <~> pTr n.+3 (pTr n.+4 (psusp K( B, n.+2))) rapply equiv_O_functor_to_O_O_leq.
    -
H: Univalence
B, A: AbGroup
n: nat
equiv_O_functor_to_O_O_leq (Tr n.+2%nat.+1) (Tr n.+4)
  (psusp
     ((fix EilenbergMacLane (G : Group) (n0 : nat) {struct n0} : pType :=
         match n0 with
         | 0 => G
         | 1 => pClassifyingSpace G
         | (_.+1 as m).+1 => pTr m.+1 (psusp (EilenbergMacLane G m))
         end)
        B n.+2))
  pt =
pt reflexivity.
  Defined.

  (** The canonical equivalence between the [n.+4]- and [n.+3]-truncations. *)
  Local Definition pequiv_ptr_psusp_em
    : pTr n.+4 (psusp K(B, n.+2)) <~>* K(B, n.+3)
    := pequiv_ptr_ptr_psusp_em^-1* o*E pequiv_ptr.

  (** [pequiv_ptr_psusp_em] commutes with the truncation unit [ptr]. *)
  Local Definition tau_ptr_psusp_em
    : pequiv_ptr_psusp_em o* ptr ==* ptr.
H: Univalence
B, A: AbGroup
n: nat
pequiv_ptr_psusp_em o* ptr ==* ptr
  Proof.
H: Univalence
B, A: AbGroup
n: nat
pequiv_ptr_psusp_em o* ptr ==* ptr
    unfold pequiv_ptr_psusp_em.
H: Univalence
B, A: AbGroup
n: nat
pequiv_ptr_ptr_psusp_em^-1* o*E pequiv_ptr o* ptr ==* ptr
    lhs' napply pmap_compose_assoc.
H: Univalence
B, A: AbGroup
n: nat
pequiv_ptr_ptr_psusp_em^-1* o* (pequiv_ptr o* ptr) ==* ptr
    rapply (cate_moveR_Ve (H0:=hasequivs_ptype)).
H: Univalence
B, A: AbGroup
n: nat
pequiv_ptr o* ptr $== pequiv_ptr_ptr_psusp_em $o ptr
    apply ptr_natural.
  Qed.

  (** Pointed maps [K(B,n.+3) ->* K(A,n.+4)] are equivalent to pointed maps [K(B,n.+2) ->* K(A,n.+3)].  This is an instance of the stabilization theorem, Buchholtz-van Doorn-Rijke, Theorem 6.7; as there, it follows from the truncated suspension-loops adjunction, with the Freudenthal input carried by [pequiv_loops_em_em]. *)
  Definition equiv_deloop_em_pmap
    : (K(B, n.+3) ->* K(A, n.+4)) <~> (K(B, n.+2) ->* K(A, n.+3))
    := pequiv_pequiv_postcompose (pequiv_loops_em_em A n.+3)^-1*
       oE loop_susp_adjoint K(B, n.+2) K(A, n.+4)
       oE pequiv_ptr_rec
       oE pequiv_pequiv_precompose pequiv_ptr_psusp_em.

  (** [equiv_deloop_em_pmap] as looping conjugated by the loop identifications. *)
  Definition equiv_deloop_em_pmap_unfold (psi : K(B, n.+3) ->* K(A, n.+4))
    : equiv_deloop_em_pmap psi
      ==* (pequiv_loops_em_em A n.+3)^-1*
          o* (fmap loops psi o* pequiv_loops_em_em B n.+2).
H: Univalence
B, A: AbGroup
n: nat
psi: K( B, n.+3) ->* K( A, n.+4)
equiv_deloop_em_pmap psi ==*
(pequiv_loops_em_em A n.+3)^-1*
o* (fmap loops psi o* pequiv_loops_em_em B n.+2)
  Proof.
H: Univalence
B, A: AbGroup
n: nat
psi: K( B, n.+3) ->* K( A, n.+4)
equiv_deloop_em_pmap psi ==*
(pequiv_loops_em_em A n.+3)^-1*
o* (fmap loops psi o* pequiv_loops_em_em B n.+2)
    change (equiv_deloop_em_pmap psi) with
      ((pequiv_loops_em_em A n.+3)^-1*
         o* (fmap loops (psi o* pequiv_ptr_psusp_em o* ptr)
               o* loop_susp_unit K(B, n.+2))).
H: Univalence
B, A: AbGroup
n: nat
psi: K( B, n.+3) ->* K( A, n.+4)
(pequiv_loops_em_em A n.+3)^-1*
o* (fmap loops (psi o* pequiv_ptr_psusp_em o* ptr)
    o* loop_susp_unit K( B, n.+2)) ==*
(pequiv_loops_em_em A n.+3)^-1*
o* (fmap loops psi o* pequiv_loops_em_em B n.+2)
    napply pmap_postwhisker.
H: Univalence
B, A: AbGroup
n: nat
psi: K( B, n.+3) ->* K( A, n.+4)
fmap loops (psi o* pequiv_ptr_psusp_em o* ptr) o* loop_susp_unit K( B, n.+2) ==*
fmap loops psi o* pequiv_loops_em_em B n.+2
    rhs' napply (pmap_postwhisker _ (loops_em_em_ptr_unit B n.+1)).
H: Univalence
B, A: AbGroup
n: nat
psi: K( B, n.+3) ->* K( A, n.+4)
fmap loops (psi o* pequiv_ptr_psusp_em o* ptr) o* loop_susp_unit K( B, n.+2) ==*
fmap loops psi o* (fmap loops ptr o* loop_susp_unit K( B, n.+2))
    rhs_V' napply pmap_compose_assoc.
H: Univalence
B, A: AbGroup
n: nat
psi: K( B, n.+3) ->* K( A, n.+4)
fmap loops (psi o* pequiv_ptr_psusp_em o* ptr) o* loop_susp_unit K( B, n.+2) ==*
fmap loops psi o* fmap loops ptr o* loop_susp_unit K( B, n.+2)
    refine (pmap_prewhisker _ (_ @* fmap_comp loops _ _)).
H: Univalence
B, A: AbGroup
n: nat
psi: K( B, n.+3) ->* K( A, n.+4)
fmap loops (psi o* pequiv_ptr_psusp_em o* ptr) ==* fmap loops (psi $o ptr)
    tapply (fmap2 loops).
H: Univalence
B, A: AbGroup
n: nat
psi: K( B, n.+3) ->* K( A, n.+4)
psi o* pequiv_ptr_psusp_em o* ptr $== psi $o ptr
    exact (pmap_compose_assoc psi _ ptr
           @* pmap_postwhisker psi tau_ptr_psusp_em).
  Qed.

End Deloop.