Require Import Basics Types Pointed HSet.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Modalities.Modality.
Require Import Truncations.Core Truncations.SeparatedTrunc.
Require Import Algebra.AbGroups.
Require Import WildCat.

Local Open Scope nat_scope.
Local Open Scope pointed_scope.
Local Open Scope path_scope.

(** The type that the nth homotopy group will have. *)
Definition HomotopyGroup_type (n : nat) : Type
  := match n with
      | 0 => pType
      | n.+1 => Group
     end.

(* Every homotopy group is, in particular, a pointed type. *)
Definition HomotopyGroup_type_ptype (n : nat) : HomotopyGroup_type n -> pType
  := match n return HomotopyGroup_type n -> pType with
     | 0 => fun X => X
     (* This works because [ptype_group] is already a coercion. *)
     | n.+1 => fun G => G
     end.

Coercion HomotopyGroup_type_ptype : HomotopyGroup_type >-> pType.

(** We construct the wildcat structure on HomotopyGroup_type in the obvious way. *)
Global Instance isgraph_homotopygroup_type (n : nat)
  : IsGraph (HomotopyGroup_type n) := ltac:(destruct n; exact _).
Global Instance is2graph_homotopygroup_type (n : nat)
  : Is2Graph (HomotopyGroup_type n) := ltac:(destruct n; exact _).
Global Instance is01cat_homotopygroup_type (n : nat)
  : Is01Cat (HomotopyGroup_type n) := ltac:(destruct n; exact _).
Global Instance is1cat_homotopygroup_type (n : nat)
  : Is1Cat (HomotopyGroup_type n) := ltac:(destruct n; exact _).
Global Instance is0functor_homotopygroup_type_ptype (n : nat)
  : Is0Functor (HomotopyGroup_type_ptype n)
  := ltac:(destruct n; exact _).
Global Instance is1functor_homotopygroup_type_ptype (n : nat)
  : Is1Functor (HomotopyGroup_type_ptype n)
  := ltac:(destruct n; exact _).

(** We first define [Pi 1 X], and use this to define [Pi n X].
  The reason is to make it easier for Coq to see that [Pi (n.+1) X] is
  definitionally equal to [Pi 1 (iterated_loops n X)] *)
Definition Pi1 (X : pType) : Group.
X: pType
Group
Proof.
X: pType
Group
  srapply (Build_Group (Tr 0 (loops X)));
  repeat split.
X: pType
SgOp (Tr 0 (loops X))
X: pType
MonUnit (Tr 0 (loops X))
X: pType
Negate (Tr 0 (loops X))
X: pType
IsHSet (Tr 0 (loops X))
X: pType
Associative sg_op
X: pType
LeftIdentity sg_op mon_unit
X: pType
RightIdentity sg_op mon_unit
X: pType
LeftInverse sg_op negate mon_unit
X: pType
RightInverse sg_op negate mon_unit
  (** Operation *)
  +
X: pType
SgOp (Tr 0 (loops X)) intros x y.
X: pType
x, y: Tr 0 (loops X)
Tr 0 (loops X)
    strip_truncations.
X: pType
y, x: loops X
Tr 0 (loops X)
    exact (tr (x @ y)).
  (** Unit *)
  +
X: pType
MonUnit (Tr 0 (loops X)) exact (tr 1).
  (** Inverse *)
  +
X: pType
Negate (Tr 0 (loops X)) srapply Trunc_rec; intro x.
X: pType
x: loops X
Tr 0 (loops X)
    exact (tr x^).
  (** IsHSet *)
  +
X: pType
IsHSet (Tr 0 (loops X)) exact _.
  (** Associativity *)
  +
X: pType
Associative sg_op intros x y z.
X: pType
x, y, z: Tr 0 (loops X)
sg_op x (sg_op y z) = sg_op (sg_op x y) z
    strip_truncations.
X: pType
z, y, x: loops X
sg_op (tr x) (sg_op (tr y) (tr z)) =
sg_op (sg_op (tr x) (tr y)) (tr z)
    cbn; apply ap.
X: pType
z, y, x: loops X
x @ (y @ z) = (x @ y) @ z
    apply concat_p_pp.
  (** Left identity *)
  +
X: pType
LeftIdentity sg_op mon_unit intro x.
X: pType
x: Tr 0 (loops X)
sg_op mon_unit x = x
    strip_truncations.
X: pType
x: loops X
sg_op mon_unit (tr x) = tr x
    cbn; apply ap.
X: pType
x: loops X
1 @ x = x
    apply concat_1p.
  (** Right identity *)
  +
X: pType
RightIdentity sg_op mon_unit intro x.
X: pType
x: Tr 0 (loops X)
sg_op x mon_unit = x
    strip_truncations.
X: pType
x: loops X
sg_op (tr x) mon_unit = tr x
    cbn; apply ap.
X: pType
x: loops X
x @ 1 = x
    apply concat_p1.
  (** Left inverse *)
  +
X: pType
LeftInverse sg_op negate mon_unit intro x.
X: pType
x: Tr 0 (loops X)
sg_op (negate x) x = mon_unit
    strip_truncations.
X: pType
x: loops X
sg_op (negate (tr x)) (tr x) = mon_unit
    apply (ap tr).
X: pType
x: loops X
x^ @ x = 1
    apply concat_Vp.
  (** Right inverse *)
  +
X: pType
RightInverse sg_op negate mon_unit intro x.
X: pType
x: Tr 0 (loops X)
sg_op x (negate x) = mon_unit
    strip_truncations.
X: pType
x: loops X
sg_op (tr x) (negate (tr x)) = mon_unit
    apply (ap tr).
X: pType
x: loops X
x @ x^ = 1
    apply concat_pV.
Defined.

(** Definition of the nth homotopy group *)
Definition Pi (n : nat) (X : pType) : HomotopyGroup_type n.
n: nat
X: pType
HomotopyGroup_type n
Proof.
n: nat
X: pType
HomotopyGroup_type n
  destruct n.
X: pType
HomotopyGroup_type 0
n: nat
X: pType
HomotopyGroup_type n.+1
  1: exact (pTr 0 X).
n: nat
X: pType
HomotopyGroup_type n.+1
  exact (Pi1 (iterated_loops n X)).
Defined.

(** See [pi_loops] below for an alternate unfolding. *)
Definition pi_succ n X : Pi n.+1 X $<~> Pi 1 (iterated_loops n X)
  := grp_iso_id.

Module PiUtf8.
  Notation "'π'" := Pi.
End PiUtf8.

Global Instance ishset_pi {n : nat} {X : pType}
  : IsHSet (Pi n X)
  := ltac:(destruct n; exact _).

(** When n >= 2 we have that the nth homotopy group is an abelian group. Note that we don't actually define it as an abelian group but merely show that it is one. This would cause lots of complications with the typechecker. *)
Global Instance isabgroup_pi (n : nat) (X : pType)
  : IsAbGroup (Pi n.+2 X).
n: nat
X: pType
IsAbGroup (Pi n.+2 X)
Proof.
n: nat
X: pType
IsAbGroup (Pi n.+2 X)
  nrapply Build_IsAbGroup.
n: nat
X: pType
IsGroup (Pi n.+2 X)
n: nat
X: pType
Commutative sg_op
  1: exact _.
n: nat
X: pType
Commutative sg_op
  intros x y.
n: nat
X: pType
x, y: Pi n.+2 X
sg_op x y = sg_op y x
  strip_truncations.
n: nat
X: pType
y, x: loops (iterated_loops n.+1 X)
sg_op (tr x) (tr y) = sg_op (tr y) (tr x)
  cbn; apply (ap tr).
n: nat
X: pType
y, x: loops (iterated_loops n.+1 X)
x @ y = y @ x
  apply eckmann_hilton.
Defined.

(** For the same reason as above, we make [Pi1] a functor before making [Pi] a functor. *)
Global Instance is0functor_pi1 : Is0Functor Pi1.
Is0Functor Pi1
Proof.
Is0Functor Pi1
  apply Build_Is0Functor.
forall a b : pType, (a $-> b) -> Pi1 a $-> Pi1 b
  intros X Y f.
X, Y: pType
f: X $-> Y
Pi1 X $-> Pi1 Y
  snrapply Build_GroupHomomorphism.
X, Y: pType
f: X $-> Y
Pi1 X -> Pi1 Y
X, Y: pType
f: X $-> Y
IsSemiGroupPreserving ?f
  {
X, Y: pType
f: X $-> Y
Pi1 X -> Pi1 Y rapply (fmap (Tr 0)).
X, Y: pType
f: X $-> Y
loops X $-> loops Y
    rapply (fmap loops).
X, Y: pType
f: X $-> Y
X $-> Y
    assumption. }
X, Y: pType
f: X $-> Y
IsSemiGroupPreserving (fmap (Tr 0) (fmap loops f))
  (** Note: we don't have to be careful about which paths we choose here since we are trying to inhabit a proposition. *)
  intros x y.
X, Y: pType
f: X $-> Y
x, y: Pi1 X
fmap (Tr 0) (fmap loops f) (sg_op x y) =
sg_op (fmap (Tr 0) (fmap loops f) x)
  (fmap (Tr 0) (fmap loops f) y)
  strip_truncations.
X, Y: pType
f: X $-> Y
y, x: loops X
fmap (Tr 0) (fmap loops f) (sg_op (tr x) (tr y)) =
sg_op (fmap (Tr 0) (fmap loops f) (tr x))
  (fmap (Tr 0) (fmap loops f) (tr y))
  apply (ap tr); cbn.
X, Y: pType
f: X $-> Y
y, x: loops X
(point_eq f)^ @ (ap f (x @ y) @ point_eq f) =
((point_eq f)^ @ (ap f x @ point_eq f)) @
((point_eq f)^ @ (ap f y @ point_eq f))
  rewrite 2 concat_pp_p.
X, Y: pType
f: X $-> Y
y, x: loops X
(point_eq f)^ @ (ap f (x @ y) @ point_eq f) =
(point_eq f)^ @
(ap f x @
 (point_eq f @ ((point_eq f)^ @ (ap f y @ point_eq f))))
  apply whiskerL.
X, Y: pType
f: X $-> Y
y, x: loops X
ap f (x @ y) @ point_eq f =
ap f x @
(point_eq f @ ((point_eq f)^ @ (ap f y @ point_eq f)))
  rewrite 2 concat_p_pp.
X, Y: pType
f: X $-> Y
y, x: loops X
ap f (x @ y) @ point_eq f =
((ap f x @ point_eq f) @ (point_eq f)^) @
(ap f y @ point_eq f)
  rewrite (concat_pp_p (ap f x)).
X, Y: pType
f: X $-> Y
y, x: loops X
ap f (x @ y) @ point_eq f =
(ap f x @ (point_eq f @ (point_eq f)^)) @
(ap f y @ point_eq f)
  rewrite concat_pV, concat_p1.
X, Y: pType
f: X $-> Y
y, x: loops X
ap f (x @ y) @ point_eq f =
ap f x @ (ap f y @ point_eq f)
  rewrite concat_p_pp.
X, Y: pType
f: X $-> Y
y, x: loops X
ap f (x @ y) @ point_eq f =
(ap f x @ ap f y) @ point_eq f
  apply whiskerR.
X, Y: pType
f: X $-> Y
y, x: loops X
ap f (x @ y) = ap f x @ ap f y
  apply ap_pp.
Defined.

Global Instance is0functor_pi (n : nat) : Is0Functor (Pi n)
  := ltac:(destruct n; exact _).

Definition fmap_pi_succ {X Y : pType} (f : X $-> Y) (n : nat)
  : fmap (Pi n.+1) f $== fmap (Pi 1) (fmap (iterated_loops n) f).
X, Y: pType
f: X $-> Y
n: nat
fmap (Pi n.+1) f $==
fmap (Pi 1) (fmap (iterated_loops n) f)
Proof.
X, Y: pType
f: X $-> Y
n: nat
fmap (Pi n.+1) f $==
fmap (Pi 1) (fmap (iterated_loops n) f)
  reflexivity.
Defined.

Global Instance is1functor_pi1 : Is1Functor Pi1.
Is1Functor Pi1
Proof.
Is1Functor Pi1
  (** The conditions for [Pi1] to be a 1-functor only involve equalities of maps between groups, which reduce to equalities of maps between types.  Type inference shows that [Tr 0 o loops] is a 1-functor, and so it follows that [Pi1] is a 1-functor. *)
  assert (is1f : Is1Functor (Tr 0 o loops)) by exact _.
is1f: Is1Functor (Tr 0 o (fun A : pType => loops A))
Is1Functor Pi1
  apply Build_Is1Functor; intros;
    [ by rapply (fmap2 _ (is1functor_F := is1f))
    | by rapply (fmap_id _ (is1functor_F := is1f))
    | by rapply (fmap_comp _ (is1functor_F := is1f)) ].
Defined.

Global Instance is1functor_pi (n : nat) : Is1Functor (Pi n)
  := ltac:(destruct n; exact _).

(** Sometimes it is convenient to regard [Pi n] as landing in pointed types.  On objects, this is handled by the coercion [HomotopyGroup_type_ptype], but on morphisms it doesn't seem possible to define a coercion.  So we explicitly name the composite functor. *)
Definition pPi (n : nat) : pType -> pType := HomotopyGroup_type_ptype n o Pi n.
Global Instance is0functor_ppi (n : nat) : Is0Functor (pPi n) := _.
Global Instance is1functor_ppi (n : nat) : Is1Functor (pPi n) := _.

(** [pPi] is equal to a more explicit map.  These are definitional for [n = 0] and [n] a successor; it would be nice to make them definitional for generic [n]. *)
Definition ppi_ptr_iterated_loops (n : nat)
  : pPi n = pTr 0 o iterated_loops n
  := ltac:(destruct n; reflexivity).

(** Here is the associated object-wise equivalence, which is the identity map for [0] and successors. *)
Definition pequiv_ppi_ptr_iterated_loops (n : nat) (X : pType)
  : pPi n X <~>* pTr 0 (iterated_loops n X)
  := ltac:(destruct n; exact pequiv_pmap_idmap).

(** These equivalences are natural. Put another way, we can compute [fmap Pi] in terms of the composite functor, up to the equivalences above. For [n = 0] or [n] a successor, we can omit the equivalences; for [n = 0], the induced maps are definitionally equal as pointed maps; for [n] a successfor the underlying unpointed maps are definitionally equal, but the pointedness proofs are not, and this is handled by [phomotopy_homotopy_hset]. *)
Definition fmap_ppi_ptr_iterated_loops (n : nat) {X Y : pType} (f : X ->* Y)
  : pequiv_ppi_ptr_iterated_loops n Y o* fmap (pPi n) f
     ==* fmap (pTr 0) (fmap (iterated_loops n) f) o* pequiv_ppi_ptr_iterated_loops n X.
n: nat
X, Y: pType
f: X ->* Y
pequiv_ppi_ptr_iterated_loops n Y o* fmap (pPi n) f ==*
fmap (pTr 0) (fmap (iterated_loops n) f)
o* pequiv_ppi_ptr_iterated_loops n X
Proof.
n: nat
X, Y: pType
f: X ->* Y
pequiv_ppi_ptr_iterated_loops n Y o* fmap (pPi n) f ==*
fmap (pTr 0) (fmap (iterated_loops n) f)
o* pequiv_ppi_ptr_iterated_loops n X
  destruct n; unfold pequiv_ppi_ptr_iterated_loops.
X, Y: pType
f: X ->* Y
pequiv_pmap_idmap o* fmap (pPi 0) f ==*
fmap (pTr 0) (fmap (iterated_loops 0) f)
o* pequiv_pmap_idmap
n: nat
X, Y: pType
f: X ->* Y
pequiv_pmap_idmap o* fmap (pPi n.+1) f ==*
fmap (pTr 0) (fmap (iterated_loops n.+1) f)
o* pequiv_pmap_idmap
  1: refine (pmap_postcompose_idmap _ @* (pmap_precompose_idmap _)^*).
n: nat
X, Y: pType
f: X ->* Y
pequiv_pmap_idmap o* fmap (pPi n.+1) f ==*
fmap (pTr 0) (fmap (iterated_loops n.+1) f)
o* pequiv_pmap_idmap
  refine (pmap_postcompose_idmap _ @* _ @* (pmap_precompose_idmap _)^*).
n: nat
X, Y: pType
f: X ->* Y
fmap (pPi n.+1) f ==*
fmap (pTr 0) (fmap (iterated_loops n.+1) f)
  srapply phomotopy_homotopy_hset; reflexivity.
Defined.

(** [Pi n.+1] sends equivalences to group isomorphisms. *)
Definition groupiso_pi_functor (n : nat) {X Y : pType} (e : X <~>* Y)
  : Pi n.+1 X $<~> Pi n.+1 Y
  := emap (Pi n.+1) e.

(** The homotopy groups of a loop space are those of the space shifted.  *)
Definition pi_loops n X : Pi n.+1 X <~>* Pi n (loops X).
n: nat
X: pType
Pi n.+1 X <~>* Pi n (loops X)
Proof.
n: nat
X: pType
Pi n.+1 X <~>* Pi n (loops X)
  destruct n.
X: pType
Pi 1 X <~>* Pi 0 (loops X)
n: nat
X: pType
Pi n.+2 X <~>* Pi n.+1 (loops X)
  1: reflexivity.
n: nat
X: pType
Pi n.+2 X <~>* Pi n.+1 (loops X)
  rapply (emap (pTr 0 o loops)).
n: nat
X: pType
iterated_loops n.+1 X $<~> iterated_loops n (loops X)
  apply unfold_iterated_loops'.
Defined.

(** Except in the lowest case, this can be expressed as an isomorphism of groups. *)
Definition groupiso_pi_loops n X : Pi n.+2 X $<~> Pi n.+1 (loops X).
n: nat
X: pType
Pi n.+2 X $<~> Pi n.+1 (loops X)
Proof.
n: nat
X: pType
Pi n.+2 X $<~> Pi n.+1 (loops X)
  snrapply (groupiso_pi_functor 0).
n: nat
X: pType
[pt = pt, 1] <~>* iterated_loops n (loops X)
  apply unfold_iterated_loops'.
Defined.

(** Naturality of [pi_loops]. *)
Definition fmap_pi_loops (n : nat) {X Y : pType} (f : X ->* Y)
  : (pi_loops n Y) o* (fmap (Pi n.+1) f)
    ==* (fmap (pPi n o loops) f) o* (pi_loops n X).
n: nat
X, Y: pType
f: X ->* Y
pi_loops n Y o* fmap (Pi n.+1) f ==*
fmap (pPi n o loops) f o* pi_loops n X
Proof.
n: nat
X, Y: pType
f: X ->* Y
pi_loops n Y o* fmap (Pi n.+1) f ==*
fmap (pPi n o loops) f o* pi_loops n X
  destruct n; srapply phomotopy_homotopy_hset; intros x.
X, Y: pType
f: X ->* Y
x: Pi 1 X
(pi_loops 0 Y o* fmap (Pi 1) f) x =
(fmap (pPi 0 o loops) f o* pi_loops 0 X) x
n: nat
X, Y: pType
f: X ->* Y
x: Pi n.+2 X
(pi_loops n.+1 Y o* fmap (Pi n.+2) f) x =
(fmap (pPi n.+1 o loops) f o* pi_loops n.+1 X) x
  1: reflexivity.
n: nat
X, Y: pType
f: X ->* Y
x: Pi n.+2 X
(pi_loops n.+1 Y o* fmap (Pi n.+2) f) x =
(fmap (pPi n.+1 o loops) f o* pi_loops n.+1 X) x
  refine ((O_functor_compose 0 _ _ _)^ @ _ @ (O_functor_compose 0 _ _ _)).
n: nat
X, Y: pType
f: X ->* Y
x: Pi n.+2 X
O_functor (Tr 0%nat)
  (fun x : loops (iterated_loops n.+1 X) =>
   fmap loops (unfold_iterated_loops' n Y)
     (fmap loops (fmap (iterated_loops n.+1) f) x)) x =
O_functor (Tr 0%nat)
  (fun x : loops (iterated_loops n.+1 X) =>
   fmap loops (fmap (iterated_loops n) (fmap loops f))
     (fmap loops (unfold_iterated_loops' n X) x)) x
  apply O_functor_homotopy.
n: nat
X, Y: pType
f: X ->* Y
x: Pi n.+2 X
(fun x : loops (iterated_loops n.+1 X) =>
 fmap loops (unfold_iterated_loops' n Y)
   (fmap loops (fmap (iterated_loops n.+1) f) x)) ==
(fun x : loops (iterated_loops n.+1 X) =>
 fmap loops (fmap (iterated_loops n) (fmap loops f))
   (fmap loops (unfold_iterated_loops' n X) x))
  exact (pointed_htpy (unfold_iterated_fmap_loops n.+1 f)).
Defined.

(** Homotopy groups preserve products.  This is a direct proof, but below we give a second proof whose underlying map is the natural one. *)
Definition pi_prod' {n : nat} (X Y : pType)
  : pPi n (X * Y) <~>* (pPi n X) * (pPi n Y).
n: nat
X, Y: pType
pPi n (X * Y) <~>* pPi n X * pPi n Y
Proof.
n: nat
X, Y: pType
pPi n (X * Y) <~>* pPi n X * pPi n Y
  (* First we re-express this in terms of the composite [pTr 0 o iterated_loops n]. *)
  refine (_ o*E pequiv_ppi_ptr_iterated_loops _ _).
n: nat
X, Y: pType
pTr 0 (iterated_loops n (X * Y)) <~>*
pPi n X * pPi n Y
  refine ((equiv_functor_pprod (pequiv_ppi_ptr_iterated_loops _ _)
                               (pequiv_ppi_ptr_iterated_loops _ _))^-1* o*E _).
n: nat
X, Y: pType
pTr 0 (iterated_loops n (X * Y)) <~>*
pTr 0 (iterated_loops n X) *
pTr 0 (iterated_loops n Y)
  (* For this composite, the proof is straightforward. *)
  refine (_ o*E pequiv_ptr_functor 0 _).
n: nat
X, Y: pType
iterated_loops n (X * Y) <~>* ?Goal
n: nat
X, Y: pType
pTr 0 ?Goal <~>*
pTr 0 (iterated_loops n X) *
pTr 0 (iterated_loops n Y)
  1: nrapply iterated_loops_prod.
n: nat
X, Y: pType
pTr 0 (iterated_loops n X * iterated_loops n Y) <~>*
pTr 0 (iterated_loops n X) *
pTr 0 (iterated_loops n Y)
  snrapply Build_pEquiv'; cbn.
n: nat
X, Y: pType
Trunc 0 (iterated_loops n X * iterated_loops n Y) <~>
Trunc 0 (iterated_loops n X) *
Trunc 0 (iterated_loops n Y)
n: nat
X, Y: pType
?Goal (tr ispointed_prod) = ispointed_prod
  -
n: nat
X, Y: pType
Trunc 0 (iterated_loops n X * iterated_loops n Y) <~>
Trunc 0 (iterated_loops n X) *
Trunc 0 (iterated_loops n Y) refine (equiv_O_prod_cmp 0 _ _).
  -
n: nat
X, Y: pType
equiv_O_prod_cmp (Tr 0%nat) (iterated_loops n X)
  (iterated_loops n Y) (tr ispointed_prod) =
ispointed_prod reflexivity.
Defined.

(** The pointed map from left-to-right below, coming from functoriality, is an equivalence. *)
Definition pi_prod {n : nat} (X Y : pType)
  : pPi n (X * Y) <~>* (pPi n X) * (pPi n Y).
n: nat
X, Y: pType
pPi n (X * Y) <~>* pPi n X * pPi n Y
Proof.
n: nat
X, Y: pType
pPi n (X * Y) <~>* pPi n X * pPi n Y
  snrapply Build_pEquiv.
n: nat
X, Y: pType
pPi n (X * Y) ->* pPi n X * pPi n Y
n: nat
X, Y: pType
IsEquiv ?pointed_equiv_fun
  (* This describes the natural map. *)
  -
n: nat
X, Y: pType
pPi n (X * Y) ->* pPi n X * pPi n Y rapply (equiv_pprod_coind (pfam_const _) (pfam_const _)); split.
n: nat
X, Y: pType
pPi n (X * Y) ->* pPi n X
n: nat
X, Y: pType
pPi n (X * Y) ->* pPi n Y
    +
n: nat
X, Y: pType
pPi n (X * Y) ->* pPi n X exact (fmap (pPi n) (@pfst X Y)).
    +
n: nat
X, Y: pType
pPi n (X * Y) ->* pPi n Y exact (fmap (pPi n) (@psnd X Y)).
  (* To see that it is an equivalence, we show that it is homotopic to [pi_prod']. *)
  -
n: nat
X, Y: pType
IsEquiv
  (equiv_pprod_coind (pfam_const (pPi n X))
     (pfam_const (pPi n Y))
     (fmap (pPi n) pfst, fmap (pPi n) psnd)) snrapply (isequiv_homotopic' (pi_prod' X Y)).
n: nat
X, Y: pType
pi_prod' X Y ==
equiv_pprod_coind (pfam_const (pPi n X))
  (pfam_const (pPi n Y))
  (fmap (pPi n) pfst, fmap (pPi n) psnd)
    intro xy.
n: nat
X, Y: pType
xy: pPi n (X * Y)
pi_prod' X Y xy =
equiv_pprod_coind (pfam_const (pPi n X))
  (pfam_const (pPi n Y))
  (fmap (pPi n) pfst, fmap (pPi n) psnd) xy
    destruct n; strip_truncations.
X, Y: pType
xy: X * Y
pi_prod' X Y (tr xy) =
equiv_pprod_coind (pfam_const (pPi 0 X))
  (pfam_const (pPi 0 Y))
  (fmap (pPi 0) pfst, fmap (pPi 0) psnd) (tr xy)
n: nat
X, Y: pType
xy: loops (iterated_loops n (X * Y))
pi_prod' X Y (tr xy) =
equiv_pprod_coind (pfam_const (pPi n.+1 X))
  (pfam_const (pPi n.+1 Y))
  (fmap (pPi n.+1) pfst, fmap (pPi n.+1) psnd) (tr xy)
    +
X, Y: pType
xy: X * Y
pi_prod' X Y (tr xy) =
equiv_pprod_coind (pfam_const (pPi 0 X))
  (pfam_const (pPi 0 Y))
  (fmap (pPi 0) pfst, fmap (pPi 0) psnd) (tr xy) apply path_prod; reflexivity.
    +
n: nat
X, Y: pType
xy: loops (iterated_loops n (X * Y))
pi_prod' X Y (tr xy) =
equiv_pprod_coind (pfam_const (pPi n.+1 X))
  (pfam_const (pPi n.+1 Y))
  (fmap (pPi n.+1) pfst, fmap (pPi n.+1) psnd) (tr xy) apply path_prod.
n: nat
X, Y: pType
xy: loops (iterated_loops n (X * Y))
fst (pi_prod' X Y (tr xy)) =
fst
  (equiv_pprod_coind (pfam_const (pPi n.+1 X))
     (pfam_const (pPi n.+1 Y))
     (fmap (pPi n.+1) pfst, fmap (pPi n.+1) psnd)
     (tr xy))
n: nat
X, Y: pType
xy: loops (iterated_loops n (X * Y))
snd (pi_prod' X Y (tr xy)) =
snd
  (equiv_pprod_coind (pfam_const (pPi n.+1 X))
     (pfam_const (pPi n.+1 Y))
     (fmap (pPi n.+1) pfst, fmap (pPi n.+1) psnd)
     (tr xy))
      1,2: apply (ap tr).  (* Not obvious, but unfolding makes things cluttered. *)
n: nat
X, Y: pType
xy: loops (iterated_loops n (X * Y))
fst (iterated_loops_prod X Y xy) =
fmap loops (fmap (iterated_loops n) pfst) xy
n: nat
X, Y: pType
xy: loops (iterated_loops n (X * Y))
snd (iterated_loops_prod X Y xy) =
fmap loops (fmap (iterated_loops n) psnd) xy
      *
n: nat
X, Y: pType
xy: loops (iterated_loops n (X * Y))
fst (iterated_loops_prod X Y xy) =
fmap loops (fmap (iterated_loops n) pfst) xy exact (pfst_iterated_loops_prod X Y (n:=n.+1) xy).
      *
n: nat
X, Y: pType
xy: loops (iterated_loops n (X * Y))
snd (iterated_loops_prod X Y xy) =
fmap loops (fmap (iterated_loops n) psnd) xy exact (psnd_iterated_loops_prod X Y (n:=n.+1) xy).
Defined.

(** For positive [n], this equivalence is an isomorphism of groups. *)
Lemma grp_iso_pi_prod {n : nat} (X Y : pType)
  : GroupIsomorphism (Pi n.+1 (X * Y)) (grp_prod (Pi n.+1 X) (Pi n.+1 Y)).
n: nat
X, Y: pType
GroupIsomorphism (Pi n.+1 (X * Y))
  (grp_prod (Pi n.+1 X) (Pi n.+1 Y))
Proof.
n: nat
X, Y: pType
GroupIsomorphism (Pi n.+1 (X * Y))
  (grp_prod (Pi n.+1 X) (Pi n.+1 Y))
  snrapply Build_GroupIsomorphism.
n: nat
X, Y: pType
GroupHomomorphism (Pi n.+1 (X * Y))
  (grp_prod (Pi n.+1 X) (Pi n.+1 Y))
n: nat
X, Y: pType
IsEquiv ?grp_iso_homo
  (* The underlying map is the natural one, so it is automatically a group homomorphism. *)
  -
n: nat
X, Y: pType
GroupHomomorphism (Pi n.+1 (X * Y))
  (grp_prod (Pi n.+1 X) (Pi n.+1 Y)) apply grp_prod_corec.
n: nat
X, Y: pType
GroupHomomorphism (Pi n.+1 (X * Y)) (Pi n.+1 X)
n: nat
X, Y: pType
GroupHomomorphism (Pi n.+1 (X * Y)) (Pi n.+1 Y)
    +
n: nat
X, Y: pType
GroupHomomorphism (Pi n.+1 (X * Y)) (Pi n.+1 X) exact (fmap (Pi n.+1) (@pfst X Y)).
    +
n: nat
X, Y: pType
GroupHomomorphism (Pi n.+1 (X * Y)) (Pi n.+1 Y) exact (fmap (Pi n.+1) (@psnd X Y)).
  (* This is also the underlying map of [pi_prod], so we can reuse the proof that it is an equivalence. *)
  -
n: nat
X, Y: pType
IsEquiv
  (grp_prod_corec (fmap (Pi n.+1) pfst)
     (fmap (Pi n.+1) psnd)) exact (equiv_isequiv (pi_prod X Y (n:=n.+1))).
Defined.

(** Homotopy groups of truncations *)

(** An [n]-connected map induces an equivalence on the nth homotopy group.  We first state this for [pTr 0 o iterated_loops n], since the proof works for general [n], and then we deduce the result for [pPi n] afterwards. *)
Definition isequiv_pi_connmap' `{Univalence} (n : nat) {X Y : pType} (f : X ->* Y)
  `{!IsConnMap n f}
  : IsEquiv (fmap (pTr 0) (fmap (iterated_loops n) f)).
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
IsConnMap0: IsConnMap (Tr n) f
IsEquiv (fmap (pTr 0) (fmap (iterated_loops n) f))
Proof.
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
IsConnMap0: IsConnMap (Tr n) f
IsEquiv (fmap (pTr 0) (fmap (iterated_loops n) f))
  rapply O_inverts_conn_map.
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
IsConnMap0: IsConnMap (Tr n) f
IsConnMap (Tr 0) (fmap (iterated_loops n) f)
  rapply isconnected_iterated_fmap_loops.
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
IsConnMap0: IsConnMap (Tr n) f
IsConnMap (Tr (trunc_index_inc' 0 n)) f
  rewrite 2 trunc_index_inc'_succ.
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
IsConnMap0: IsConnMap (Tr n) f
IsConnMap (Tr (trunc_index_inc' (-2) n).+2) f
  rewrite <- trunc_index_inc_agree.
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
IsConnMap0: IsConnMap (Tr n) f
IsConnMap (Tr (trunc_index_inc (-2) n).+2) f
  assumption.
Defined.

(** The same holds for [pPi n]. *)
Global Instance isequiv_pi_connmap `{Univalence} (n : nat) {X Y : pType} (f : X ->* Y)
  `{!IsConnMap n f}
  : IsEquiv (fmap (pPi n) f).
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
IsConnMap0: IsConnMap (Tr n) f
IsEquiv (fmap (pPi n) f)
Proof.
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
IsConnMap0: IsConnMap (Tr n) f
IsEquiv (fmap (pPi n) f)
  (* For [n = 0] and [n] a successor, [fmap (pPi n) f] is definitionally equal to the map in the previous result as a map of types. *)
  destruct n; rapply isequiv_pi_connmap'.
Defined.

Definition pequiv_pi_connmap `{Univalence} (n : nat) {X Y : pType} (f : X ->* Y)
  `{!IsConnMap n f}
  : Pi n X <~>* Pi n Y
  := Build_pEquiv _ _ (fmap (pPi n) f) _.

(** For positive [n], it is a group isomorphism. *)
Definition grp_iso_pi_connmap `{Univalence} (n : nat) {X Y : pType} (f : X ->* Y)
  `{!IsConnMap n.+1 f}
  : GroupIsomorphism (Pi n.+1 X) (Pi n.+1 Y)
  := Build_GroupIsomorphism _ _ (fmap (Pi n.+1) f) (isequiv_pi_connmap n.+1 f).

(** As a consequence, the truncation map [ptr : X -> pTr n X] induces an equivalence on [Pi n].  We don't make this an instance, since it is found by typeclass search. *)
Definition isequiv_pi_Tr `{Univalence} (n : nat) (X : pType)
  : IsEquiv (fmap (pPi n) ptr : Pi n X -> Pi n (pTr n X))
  := _.

Definition pequiv_pi_Tr `{Univalence} (n : nat) (X : pType)
  : Pi n X <~>* Pi n (pTr n X)
  := Build_pEquiv _ _ (fmap (pPi n) ptr) _.

(** For positive [n], it is a group isomorphism. *)
Definition grp_iso_pi_Tr `{Univalence} (n : nat) (X : pType)
  : GroupIsomorphism (Pi n.+1 X) (Pi n.+1 (pTr n.+1 X))
  := grp_iso_pi_connmap n ptr.

(** An [n]-connected map induces a surjection on [n+1]-fold loop spaces and [Pi (n+1)]. *)
Definition issurj_iterated_loops_connmap `{Univalence} (n : nat) {X Y : pType} (f : X ->* Y)
  {C : IsConnMap n f}
  : IsSurjection (fmap (iterated_loops (n.+1)) f).
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
C: IsConnMap (Tr n) f
IsConnMap (Tr (-1)) (fmap (iterated_loops n.+1) f)
Proof.
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
C: IsConnMap (Tr n) f
IsConnMap (Tr (-1)) (fmap (iterated_loops n.+1) f)
  apply isconnected_iterated_fmap_loops.
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
C: IsConnMap (Tr n) f
IsConnMap (Tr (trunc_index_inc' (-1) n.+1)) f cbn.
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
C: IsConnMap (Tr n) f
IsConnMap (Tr (trunc_index_inc' 0 n)) f
  rewrite trunc_index_inc'_0n; assumption.
Defined.

Definition issurj_pi_connmap `{Univalence} (n : nat) {X Y : pType} (f : X ->* Y)
  {C : IsConnMap n f}
  : IsConnMap (Tr (-1)) (fmap (pPi n.+1) f).
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
C: IsConnMap (Tr n) f
IsConnMap (Tr (-1)) (fmap (pPi n.+1) f)
Proof.
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
C: IsConnMap (Tr n) f
IsConnMap (Tr (-1)) (fmap (pPi n.+1) f)
  rapply conn_map_O_functor_strong_leq.
H: Univalence
n: nat
X, Y: pType
f: X ->* Y
C: IsConnMap (Tr n) f
IsConnMap (Tr (-1))
  (fmap loops (fmap (iterated_loops n) f))
  by apply issurj_iterated_loops_connmap.
Defined.

(** Pointed sections induce embeddings on homotopy groups. *)
Proposition isembedding_pi_psect {n : nat} {X Y : pType}
  (s : X ->* Y) (r : Y ->* X) (k : r o* s ==* pmap_idmap)
  : IsEmbedding (fmap (pPi n) s).
n: nat
X, Y: pType
s: X ->* Y
r: Y ->* X
k: r o* s ==* pmap_idmap
IsEmbedding (fmap (pPi n) s)
Proof.
n: nat
X, Y: pType
s: X ->* Y
r: Y ->* X
k: r o* s ==* pmap_idmap
IsEmbedding (fmap (pPi n) s)
  apply isembedding_isinj_hset.
n: nat
X, Y: pType
s: X ->* Y
r: Y ->* X
k: r o* s ==* pmap_idmap
isinj (fmap (pPi n) s)
  rapply (isinj_section (r:=fmap (pPi n) r)).
n: nat
X, Y: pType
s: X ->* Y
r: Y ->* X
k: r o* s ==* pmap_idmap
(fun x : pPi n X => fmap (pPi n) r (fmap (pPi n) s x)) ==
idmap
  intro x.
n: nat
X, Y: pType
s: X ->* Y
r: Y ->* X
k: r o* s ==* pmap_idmap
x: pPi n X
fmap (pPi n) r (fmap (pPi n) s x) = x
  lhs_V rapply (fmap_comp (pPi n) s r x).
n: nat
X, Y: pType
s: X ->* Y
r: Y ->* X
k: r o* s ==* pmap_idmap
x: pPi n X
fmap (pPi n) (r $o s) x = x
  lhs rapply (fmap2 (pPi n) k x).
n: nat
X, Y: pType
s: X ->* Y
r: Y ->* X
k: r o* s ==* pmap_idmap
x: pPi n X
fmap (pPi n) pmap_idmap x = x
  exact (fmap_id (pPi n) X x).
Defined.