Library HoTT.Homotopy.EMSpace

From HoTT Require Import Basics Types.
From HoTT.WildCat Require Import Core Universe Equiv PointedCat Yoneda.
Require Import Pointed.
Require Import HSet.
Require Import Spaces.Nat.Core.
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 Homotopy.ExactSequence.
Require Import Homotopy.Hopf.
Require Import Modalities.Identity.
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.

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)).
Proof.
  pose (a := groupiso_pi_loops n X).
  pose (b := groupiso_pi_loops n Y).
  pose (k := equiv_precompose_cat_equiv a
              oE equiv_postcompose_cat_equiv (x:=Pi n.+1 (loops X)) b^-1$).
  refine (isequiv_homotopic (k o fmap (Pi n.+1) o fmap loops (a:=X) (b:=Y)) _).
  intro f.
  rapply equiv_path_grouphomomorphism.
  intro 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)).
Proof.
  induction n in X, Y, cX, tY |- ×.
  1: exact (isequiv_fmap_pi1_pmap X Y).
  napply isequiv_fmap_pi_pmap_succ.
  - napply (isequiv_fmap_loops_pmap (n:=n)).
    + exact _.
    + apply (istrunc_leq (trunc_index_leq_add_nat n n)).
  - 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 homotopic. (It's even easier to show they are equal, but downstream users most often want a homotopy.)
Definition phomotopy_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.
Proof.
  apply phomotopy_path.
  tapply (equiv_inj (fmap (Pi n.+1) (a:=X) (b:=Y))).
  exact (equiv_path_grouphomomorphism h).
Defined.

Pointed maps out of an n-connected type into an n.+1-truncated type are determined by their composite with a map that is an embedding on Pi n.+1.
Definition phomotopy_pmap_isembedding_pi `{Univalence} {W X Y : pType} (n : nat)
  `{IsConnected n W} `{IsTrunc n.+1 X}
  (g : X ->* Y) (e : IsEmbedding (fmap (pPi n.+1) g))
  {u v : W ->* X} (p : g o× u ==* g o× v)
  : u ==* v.
Proof.
  rapply (phomotopy_pmap_pi_connected n).
  intro x.
  napply (isinj_embedding _ e).
  lhs_V tapply (fmap_comp (Pi n.+1)).
  rhs_V tapply (fmap_comp (Pi n.+1)).
  exact (fmap2 (Pi n.+1) p x).
Defined.

Two commuting squares between purely exact sequences form a map of fiber sequences, in the sense needed by connecting_map_natural_isexact, whenever F is n-connected and X' and Y' are n.+1-truncated. This is because the two sides agree after composing with pfib f', which is an embedding on Pi n.+1.
Definition phomotopy_functor_pfiber_cxfib `{Univalence} (n : nat)
  {F X Y F' X' Y' : pType}
  {i : F ->* X} {f : X ->* Y} `{IsExact purely F X Y i f}
  {i' : F' ->* X'} {f' : X' ->* Y'} `{IsExact purely F' X' Y' i' f'}
  {g : F ->* F'} {h : X ->* X'} {k : Y ->* Y'}
  `{IsConnected n F} `{IsTrunc n.+1 X'} `{IsTrunc n.+1 Y'}
  (p : h o× i ==* i' o× g) (q : k o× f ==* f' o× h)
  : functor_pfiber q o× pequiv_cxfib ==* pequiv_cxfib o× g.
Proof.
  rapply (phomotopy_pmap_isembedding_pi n (pfib f')
            (isembedding_fmap_pi_isexact _ _ n
               (c := contr_pi_istrunc n.+1 _))).
  lhs_V' napply pmap_compose_assoc.
  lhs_V' napply (pmap_prewhisker _ (square_functor_pfiber q)).
  lhs' napply pmap_compose_assoc.
  lhs' napply (pmap_postwhisker _ (pfib_cxfib _)).
  rhs_V' napply pmap_compose_assoc.
  rhs' napply (pmap_prewhisker _ (pfib_cxfib _)).
  exact p.
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).
  Proof.
    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).
  Proof.
    induction n; exact _.
  Defined.

  #[export] Instance isconnected_em' {G : Group} (n : nat)
    : IsConnected n.-1 K(G, n).
  Proof.
    destruct n.
    1: exact (is_minus_one_connected_pointed _).
    apply isconnected_em.
  Defined.

  #[export] Instance is0connected_em {G : Group} (n : nat)
    : IsConnected 0 K(G, n.+1).
  Proof.
    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)).
  Proof.
    snapply Build_pEquiv.
    1: exact (fmap (pTr _) (loop_susp_unit _)).
    napply O_inverts_conn_map.
    napply (conn_map_O_leq _ (Tr (n +2+ n))).
    1: exact (O_leq_Tr_leq (trunc_index_leq_add_nat n n)).
    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).
  Proof.
    destruct n.
    1: exact pequiv_g_loops_bg.
    change (K(G, n.+1) <~>* loops (pTr n.+2 (psusp (K(G, n.+1))))).
    refine (ptr_loops _ _ o×E _).
    destruct n.
    1: srapply (licata_finster (m:=-2)).
    refine (_ o×E pequiv_ptr (n:=n.+2)).
    rapply pequiv_ptr_loop_psusp'.
  Defined.

  Definition pequiv_loops_em_g (G : AbGroup) (n : nat)
    : G <~>* iterated_loops n K(G, n).
  Proof.
    induction n.
    - exact pequiv_pmap_idmap.
    - refine ((unfold_iterated_loops' _ _)^-1* o×E _ o×E IHn).
      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)).
  Proof.
    induction n.
    - exact grp_iso_g_pi1_bg.
    - nrefine (grp_iso_compose _ IHn).
      nrefine (grp_iso_compose _ (groupiso_pi_functor _ (pequiv_loops_em_em _ _))).
      symmetry; exact (groupiso_pi_loops _ _).
  Defined.

  Definition iscohhspace_em {G : AbGroup} (n : nat)
    : IsCohHSpace K(G, n).
  Proof.
    napply iscohhspace_equiv_cohhspace.
    2: apply pequiv_loops_em_em.
    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).
  Proof.
    napply Build_Is0Functor.
    intros G G' f.
    induction n as [|n IHn].
    - exact f.
    - destruct n as [|m].
      + exact (fmap B f).
      + exact (fmap (pTr m.+2) (fmap psusp IHn)).
  Defined.

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

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).
  Proof.
    destruct n as [|n].
    all: refine (compose_cate_fun (A:=pType) _ _ @* _).
    all: refine (pmap_postwhisker _ (compose_cate_fun (A:=pType) _ _) @* _).
    1: refine (pmap_postwhisker _ (pto_O_natural (Tr _) _) @* _).
    2: refine (pmap_postwhisker _ (ptr_natural _ _) @* _).
    all: refine ((pmap_compose_assoc _ _ _)^* @* _).
    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.
  Proof.
    destruct n as [|n].
    - exact (pbloop_natural G G' f).
    - refine (pmap_postwhisker _ (loops_em_em_ptr_unit G n) @* _).
      refine (_ @* pmap_prewhisker _ (loops_em_em_ptr_unit G' n)^*).
      refine ((pmap_compose_assoc _ _ _)^* @* _).
      refine (pmap_prewhisker _ (fmap_comp loops _ _)^* @* _).
      refine (pmap_prewhisker _ (fmap2 loops (ptr_natural _ _)) @* _).
      refine (pmap_prewhisker _ (fmap_comp loops _ _) @* _).
      refine (pmap_compose_assoc _ _ _ @* _).
      refine (pmap_postwhisker _ (loop_susp_unit_natural _)^* @* _).
      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.
  Proof.
    induction n as [|n IHn]; intro g.
    - exact (ap tr (bloop_natural G G' f g)).
    - lhs napply (ap _ (equiv_g_pi_n_em_succ G n g)).
      rhs napply (equiv_g_pi_n_em_succ G' n (f g)).
      apply moveL_equiv_V.
      lhs tapply (fmap_pi_loops n.+1 (fmap (K' n.+2) f)).
      lhs napply (ap _ (eisretr (groupiso_pi_loops n _) _)).
      lhs_V tapply (fmap_comp (pPi n.+1)).
      lhs tapply (fmap2 (pPi n.+1) (em_fmap_loops_natural f n.+1)).
      lhs tapply (fmap_comp (pPi n.+1)).
      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).

It follows that fmap (Pi n.+1) (fmap (K' n.+1) f) is an embedding when f is.
  #[export] Instance isembedding_pi_em_fmap {G G' : AbGroup}
    (f : GroupHomomorphism G G') `{!IsEmbedding f} (n : nat)
    : IsEmbedding (fmap (Pi n.+1) (fmap (K' n.+1) f)).
  Proof.
    snapply (mapinO_homotopic (Tr (-1))
               (equiv_g_pi_n_em G' n o f o (equiv_g_pi_n_em G n)^-1%equiv)).
    - symmetry; apply pi_em_fmap'.
    - rapply mapinO_compose.
  Defined.

G is also the n.+1-st homotopy group of loops K(G, n.+2), through the loop identification pequiv_loops_em_em. Composing with the inverse of groupiso_pi_loops gives equiv_g_pi_n_em G n.+1.
  Definition equiv_g_pi_n_loops_em (G : AbGroup) (n : nat)
    : GroupIsomorphism G (Pi n.+1 (loops K(G, n.+2)))
    := grp_iso_compose (groupiso_pi_functor n (pequiv_loops_em_em G n.+1))
         (equiv_g_pi_n_em G n).

This identification is natural, since pequiv_loops_em_em and equiv_g_pi_n_em are.
  Definition pi_loops_em_fmap {G G' : AbGroup}
    (f : GroupHomomorphism G G') (n : nat)
    : fmap (Pi n.+1) (fmap loops (fmap (K' n.+2) f)) o equiv_g_pi_n_loops_em G n
      == equiv_g_pi_n_loops_em G' n o f.
  Proof.
    intro g.
    lhs_V tapply (fmap_comp (Pi n.+1)).
    lhs tapply (fmap2 (Pi n.+1) (em_fmap_loops_natural f n.+1)).
    lhs tapply (fmap_comp (Pi n.+1)).
    exact (ap _ (pi_em_fmap f n g)).
  Defined.

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).
  Proof.
    induction n as [|[|n] IHn].
    - exact _.
    - exact _.
    - rapply contr_O_contr.
  Defined.

K(-,n) is a pointed functor.
  #[export] Instance ispointedfunctor_em (n : nat)
    : IsPointedFunctor (K' n).
  Proof.
    rapply Build_IsPointedFunctor'; cbn.
    snapply Build_pEquiv.
    1: exact 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 aps 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).
  Proof.
    induction n as [|n IHn].
    - exact (isconnmap_fmap_pclassifyingspace f).
    - napply (isconnmap_isconnmap_fmap_loops (n:=n)).
      1, 2: exact _.
      nrefine (cancelR_conn_map n (pequiv_loops_em_em G n.+1) _).
      1: exact _.
      rapply (conn_map_homotopic n _ _ (em_fmap_loops_natural f _)^* ).
  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).
  Proof.
    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)) _).
    intro f.
    apply equiv_path_grouphomomorphism; symmetry.
    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).
  Proof.
    symmetry.
    destruct n as [|m].
    - exact grp_iso_g_pi1_bg.
    - exact (equiv_g_pi_n_em (abgroup_pi m 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 maps between Eilenberg-Mac Lane spaces

Pointed maps K(B,n.+1) ->* K(A,m.+1) are equivalent to pointed maps K(B,n) ->* K(A,m) when m.+1 ≤ 2n, via fmap loops conjugated by the loop identifications. This is an instance of the stabilization theorem, Buchholtz-van Doorn-Rijke, Theorem 6.7.
Definition equiv_loops_em_pmap `{Univalence} (B A : AbGroup@{u}) (n m : nat)
  {mlt2n : (m.+1 ≤ n + n)%nat}
  : (K(B, n.+1) ->** K(A, m.+1)) <~>* (K(B, n) ->** K(A, m)).
Proof.
  refine (pequiv_pequiv_postcompose (pequiv_loops_em_em A m)^-1*
             o×E pequiv_pequiv_precompose (pequiv_loops_em_em B n)
               o×E pequiv_fmap_loops_pmap (n:=n.-1) _ _).
  destruct n as [|k].
  1: exact (Empty_rec (not_lt_zero_r m mlt2n)).
  rapply (istrunc_leq (m:=m.+1)).
  change (m.+1 ≤ k +2+ k)%trunc.
  (* The universe annotations avoid two spurious universe variables. *)
  apply (transport@{Set Set} (fun x ⇒ (m.+1 ≤ x)%trunc)
           (trunc_index_add_nat_add))^-1.
  exact (trunc_index_leq_nat mlt2n).
Defined.