From HoTT Require Import Basics Types Pointed HSet.From HoTT Require Import Basics Types Pointed HSet.
Require Import Modalities.Modality Modalities.Identity.
Require Import Truncations.Core Truncations.SeparatedTrunc
  Truncations.Connectedness.
Require Import Algebra.AbGroups.AbelianGroup.
Require Import Spaces.Finite.Tactics.
Require Import Homotopy.SuccessorStructure Homotopy.ExactSequence.
From HoTT.WildCat Require Import Core Universe Equiv.

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. *)
Instance isgraph_homotopygroup_type (n : nat)
  : IsGraph (HomotopyGroup_type n) := ltac:(destruct n; exact _).
Instance is2graph_homotopygroup_type (n : nat)
  : Is2Graph (HomotopyGroup_type n) := ltac:(destruct n; exact _).
Instance is01cat_homotopygroup_type (n : nat)
  : Is01Cat (HomotopyGroup_type n) := ltac:(destruct n; exact _).
Instance is1cat_homotopygroup_type (n : nat)
  : Is1Cat (HomotopyGroup_type n) := ltac:(destruct n; exact _).
Instance hasequivs_homotopygroup_type (n : nat)
  : HasEquivs (HomotopyGroup_type n) := ltac:(destruct n; exact _).
Instance is0functor_homotopygroup_type_ptype (n : nat)
  : Is0Functor (HomotopyGroup_type_ptype n)
  := ltac:(destruct n; exact _).
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))).
X: pType
SgOp (Tr 0 (loops X))
X: pType
MonUnit (Tr 0 (loops X))
X: pType
Inverse (Tr 0 (loops X))
X: pType
IsGroup (Tr 0 (loops X))
  (** 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
Inverse (Tr 0 (loops X)) srapply Trunc_rec; intro x.
X: pType
x: loops X
Tr 0 (loops X)
    exact (tr x^).
  -
X: pType
IsGroup (Tr 0 (loops X)) split.
X: pType
IsMonoid (Tr 0 (loops X))
X: pType
LeftInverse sg_op inv mon_unit
X: pType
RightInverse sg_op inv mon_unit
    +
X: pType
IsMonoid (Tr 0 (loops X)) repeat split.
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
      (** [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 inv mon_unit intro x.
X: pType
x: Tr 0 (loops X)
sg_op (inv x) x = mon_unit
      strip_truncations.
X: pType
x: loops X
sg_op (inv (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 inv mon_unit intro x.
X: pType
x: Tr 0 (loops X)
sg_op x (inv x) = mon_unit
      strip_truncations.
X: pType
x: loops X
sg_op (tr x) (inv (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.

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. *)
Instance commutative_pi (n : nat) (X : pType)
  : Commutative (A:=Pi n.+2 X) sg_op.
n: nat
X: pType
Commutative sg_op
Proof.
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. *)
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
  snapply Build_GroupHomomorphism.
X, Y: pType
f: X $-> Y
Pi1 X -> Pi1 Y
X, Y: pType
f: X $-> Y
IsSemiGroupPreserving ?grp_homo_map
  {
X, Y: pType
f: X $-> Y
Pi1 X -> Pi1 Y tapply (fmap (Tr 0)).
X, Y: pType
f: X $-> Y
loops X $-> loops Y
    tapply (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.

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.

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.

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.
Instance is0functor_ppi (n : nat) : Is0Functor (pPi n) := _.
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: exact (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.

(** For a successor, the equivalences above are the identity, so the previous result simplifies to a pointed homotopy between the two induced maps. *)
Definition fmap_ppi_ptr_iterated_loops_succ (n : nat) {X Y : pType} (f : X ->* Y)
  : fmap (pPi n.+1) f ==* fmap (pTr 0) (fmap (iterated_loops n.+1) f).
n: nat
X, Y: pType
f: X ->* Y
fmap (pPi n.+1) f ==* fmap (pTr 0) (fmap (iterated_loops n.+1) f)
Proof.
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)
  tapply (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)
  snapply (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 x0 : loops (iterated_loops n.+1 X) =>
   fmap loops (unfold_iterated_loops' n Y)
     (fmap loops (fmap (iterated_loops n.+1) f) x0))
  x =
O_functor (Tr 0%nat)
  (fun x0 : loops (iterated_loops n.+1 X) =>
   fmap loops (fmap (iterated_loops n) (fmap loops f))
     (fmap loops (unfold_iterated_loops' n X) x0))
  x
  apply O_functor_homotopy.
n: nat
X, Y: pType
f: X ->* Y
x: Pi n.+2 X
(fun x0 : loops (iterated_loops n.+1 X) =>
 fmap loops (unfold_iterated_loops' n Y)
   (fmap loops (fmap (iterated_loops n.+1) f) x0)) ==
(fun x0 : loops (iterated_loops n.+1 X) =>
 fmap loops (fmap (iterated_loops n) (fmap loops f))
   (fmap loops (unfold_iterated_loops' n X) x0))
  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: napply 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)
  snapply 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) exact (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
  snapply 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)) snapply (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, ispointed_prod]
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, ispointed_prod]
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))
  snapply 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
Pi n.+1 (X * Y) $-> Pi n.+1 X
n: nat
X, Y: pType
Pi n.+1 (X * Y) $-> Pi n.+1 Y
    +
n: nat
X, Y: pType
Pi n.+1 (X * Y) $-> Pi n.+1 X exact (fmap (Pi n.+1) (@pfst X Y)).
    +
n: nat
X, Y: pType
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 conn_map_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]. *)
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; tapply 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 conn_map_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.

(** The [n.+2]-nd homotopy group of an [n.+1]-truncated type vanishes. *)
Definition contr_pi_succ_istrunc `{Univalence} (n : nat) (X : pType)
  `{IsTrunc n.+1 X}
  : Contr (Pi n.+2 X).
H: Univalence
n: nat
X: pType
IsTrunc0: IsTrunc n.+1 X
Contr (Pi n.+2 X)
Proof.
H: Univalence
n: nat
X: pType
IsTrunc0: IsTrunc n.+1 X
Contr (Pi n.+2 X)
  rapply contr_O_contr.
H: Univalence
n: nat
X: pType
IsTrunc0: IsTrunc n.+1 X
Contr (loops (iterated_loops n.+1 X))
  rapply (equiv_istrunc_contr_iterated_loops n.+2).
Defined.

(** An [n.+1]-truncated pointed [0]-connected type whose [n.+1]-st homotopy group vanishes is [n]-truncated. *)
Definition istrunc_contr_pi `{Univalence} (n : nat) (X : pType)
  `{IsConnected 0 X} `{IsTrunc n.+1 X} (c : Contr (Pi n.+1 X))
  : IsTrunc n X.
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr 0%nat) X
IsTrunc0: IsTrunc n.+1 X
c: Contr (Pi n.+1 X)
IsTrunc n X
Proof.
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr 0%nat) X
IsTrunc0: IsTrunc n.+1 X
c: Contr (Pi n.+1 X)
IsTrunc n X
  apply (equiv_istrunc_contr_iterated_loops n.+1 X)^-1.
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr 0%nat) X
IsTrunc0: IsTrunc n.+1 X
c: Contr (Pi n.+1 X)
forall a : X, Contr (iterated_loops n.+1 [X, a])
  rapply (conn_point_elim (-1)%trunc).
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr 0%nat) X
IsTrunc0: IsTrunc n.+1 X
c: Contr (Pi n.+1 X)
Contr (iterated_loops n.+1 [X, pt])
  pose proof (istrunc_iterated_loops n.+1 X).
H: Univalence
n: nat
X: pType
H0: IsConnected (Tr 0%nat) X
IsTrunc0: IsTrunc n.+1 X
c: Contr (Pi n.+1 X)
X0: IsHSet (iterated_loops n.+1 X)
Contr (iterated_loops n.+1 [X, pt])
  exact (contr_equiv' (Pi n.+1 X) (equiv_tr 0 _)^-1%equiv).
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
IsInjective (fmap (pPi n) s)
  tapply (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 exact (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 exact (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.

(** ** The long exact sequence of homotopy groups *)

(** A fiber sequence [F -> X -> Y] gives rise to a long exact sequence of homotopy groups.  [Pi_les_pset] already provides one, but its maps are expressed using the composite [pTr 0 o iterated_loops n] instead of [pPi n].  We build the equivalent sequence whose maps are [fmap (pPi n)] and the connecting maps, giving each ingredient a name so that the terms of the sequence are transparent.  When [n] is destructed, the objects of the two sequences are definitionally equal, and the only difference between the morphisms is in their pointedness proofs.  The new sequence also definitionally lands in groups for successor indices. *)

Section PiLES.
  Local Open Scope succ_scope.

  Context `{Univalence} {F X Y : pType} (i : F ->* X) (f : X ->* Y)
    `{IsExact purely F X Y i f}.

  (** The types appearing in the sequence. *)
  Definition pi_carrier (n : N3) : pType :=
    match n with
    | (n, inl (inl (inl x))) => Empty_ind _ x
    | (n, inl (inl (inr tt))) => pPi n Y
    | (n, inl (inr tt)) => pPi n X
    | (n, inr tt) => pPi n F
    end.

  (** They are pointed equivalent to the types appearing in [Pi_les_pset], by the identity map in each case. *)
  Definition pequiv_pi_carrier (n : N3)
    : pi_carrier n <~>* pTr 0 (loops_carrier F X Y n).
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: N3
pi_carrier n <~>* pTr 0 (loops_carrier F X Y n)
  Proof.
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: N3
pi_carrier n <~>* pTr 0 (loops_carrier F X Y n)
    destruct n as [n x]; FinIndOn x; exact (pequiv_ppi_ptr_iterated_loops _ _).
  Defined.

  (** The connecting map [Pi n.+1 Y -> Pi n F] of the fiber sequence. *)
  Definition pi_connecting_map (n : nat)
    : pPi n.+1 Y ->* pPi n F
    := (pequiv_ppi_ptr_iterated_loops n F)^-1*
         o* fmap (pTr 0) (connecting_map (fmap (iterated_loops n) i)
                                         (fmap (iterated_loops n) f)).

  (** The maps appearing in the sequence. *)
  Definition pi_les_fn (n : N3)
    : pi_carrier (ss_succ n) ->* pi_carrier n.
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: N3
pi_carrier n.+1 ->* pi_carrier n
  Proof.
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: N3
pi_carrier n.+1 ->* pi_carrier n
    destruct n as [n x]; FinIndOn x.
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
pi_carrier (n, inl (inl (inr tt))).+1 ->* pi_carrier (n, inl (inl (inr tt)))
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
pi_carrier (n, inl (inr tt)).+1 ->* pi_carrier (n, inl (inr tt))
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
pi_carrier (n, inr tt).+1 ->* pi_carrier (n, inr tt)
    -
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
pi_carrier (n, inl (inl (inr tt))).+1 ->* pi_carrier (n, inl (inl (inr tt))) exact (fmap (pPi n) f).
    -
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
pi_carrier (n, inl (inr tt)).+1 ->* pi_carrier (n, inl (inr tt)) exact (fmap (pPi n) i).
    -
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
pi_carrier (n, inr tt).+1 ->* pi_carrier (n, inr tt) exact (pi_connecting_map n).
  Defined.

  (** They agree with the maps of [Pi_les_pset] under the equivalences above.  For the first two this is [fmap_ppi_ptr_iterated_loops]; for the connecting map it is the cancellation of an equivalence with its inverse. *)
  Definition pi_les_square (n : N3)
    : pequiv_pi_carrier n o* pi_les_fn n
      ==* les_fn (Pi_les_pset i f) n o* pequiv_pi_carrier (ss_succ n).
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: N3
pequiv_pi_carrier n o* pi_les_fn n ==*
les_fn (Pi_les_pset i f) n o* pequiv_pi_carrier n.+1
  Proof.
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: N3
pequiv_pi_carrier n o* pi_les_fn n ==*
les_fn (Pi_les_pset i f) n o* pequiv_pi_carrier n.+1
    destruct n as [n x]; FinIndOn x.
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
pequiv_pi_carrier (n, inl (inl (inr tt)))
o* pi_les_fn (n, inl (inl (inr tt))) ==*
les_fn (Pi_les_pset i f) (n, inl (inl (inr tt)))
o* pequiv_pi_carrier (n, inl (inl (inr tt))).+1
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
pequiv_pi_carrier (n, inl (inr tt)) o* pi_les_fn (n, inl (inr tt)) ==*
les_fn (Pi_les_pset i f) (n, inl (inr tt))
o* pequiv_pi_carrier (n, inl (inr tt)).+1
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
pequiv_pi_carrier (n, inr tt) o* pi_les_fn (n, inr tt) ==*
les_fn (Pi_les_pset i f) (n, inr tt) o* pequiv_pi_carrier (n, inr tt).+1
    -
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
pequiv_pi_carrier (n, inl (inl (inr tt)))
o* pi_les_fn (n, inl (inl (inr tt))) ==*
les_fn (Pi_les_pset i f) (n, inl (inl (inr tt)))
o* pequiv_pi_carrier (n, inl (inl (inr tt))).+1 exact (fmap_ppi_ptr_iterated_loops n f).
    -
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
pequiv_pi_carrier (n, inl (inr tt)) o* pi_les_fn (n, inl (inr tt)) ==*
les_fn (Pi_les_pset i f) (n, inl (inr tt))
o* pequiv_pi_carrier (n, inl (inr tt)).+1 exact (fmap_ppi_ptr_iterated_loops n i).
    -
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
pequiv_pi_carrier (n, inr tt) o* pi_les_fn (n, inr tt) ==*
les_fn (Pi_les_pset i f) (n, inr tt) o* pequiv_pi_carrier (n, inr tt).+1 tapply phomotopy_homotopy_hset.
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
pequiv_pi_carrier (n, inr tt) o* pi_les_fn (n, inr tt) ==
les_fn (Pi_les_pset i f) (n, inr tt) o* pequiv_pi_carrier (n, inr tt).+1
      intro x; cbn.
H: Univalence
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
n: +N
x: pi_carrier (n, inr tt).+1
pequiv_ppi_ptr_iterated_loops n F
  ((pequiv_ppi_ptr_iterated_loops n F)^-1
     (Trunc_rec
        (fun x0 : pt = pt =>
         tr
           (O_rec idmap
              (center
                 (hfiber
                    (fun
                       x1 : (fix F0 (m : nat) : pType :=
                               match m with
                               | 0 => F
                               | m'.+1%nat => loops (F0 m')
                               end)
                              n =>
                     (fmap (iterated_loops n) i x1; cx_isexact x1))
                    ((pfiber2_loops (fmap (iterated_loops n) f))^-1 x0).1))).1)
        x)) =
Trunc_rec
  (fun x0 : pt = pt =>
   tr
     (O_rec idmap
        (center
           (hfiber
              (fun
                 x1 : (fix F0 (m : nat) : pType :=
                         match m with
                         | 0 => F
                         | m'.+1%nat => loops (F0 m')
                         end)
                        n =>
               (fmap (iterated_loops n) i x1; cx_isexact x1))
              ((pfiber2_loops (fmap (iterated_loops n) f))^-1 x0).1))).1)
  x
      apply eisretr.
  Defined.

  (** The long exact sequence of homotopy groups of a fiber sequence. *)
  Definition Pi_les : LongExactSequence (Tr (-1)) N3
    := les_pequiv (Pi_les_pset i f) pi_carrier
         pequiv_pi_carrier pi_les_fn pi_les_square.

  (** Each level of [Pi_les] contributes three exactness statements, which we record separately to save the reader from the indexing of [N3].  They are named after the space whose homotopy group sits in the middle of the sequence, and are listed in the order in which they occur. *)

  (** [Pi_les] is exact at [Pi n F], the homotopy group of the fiber.  The map into it is the connecting map. *)
  Definition isexact_pi_fiber (n : nat)
    : IsExact (Tr (-1)) (pi_connecting_map n) (fmap (pPi n) i)
    := les_isexact _ _ Pi_les (n, inl (inr tt)).

  (** [Pi_les] is exact at [Pi n X], the homotopy group of the total space. *)
  Definition isexact_pi_total (n : nat)
    : IsExact (Tr (-1)) (fmap (pPi n) i) (fmap (pPi n) f)
    := les_isexact _ _ Pi_les (n, inl (inl (inr tt))).

  (** [Pi_les] is exact at [Pi n.+1 Y], the homotopy group of the base.  The map out of it is the connecting map. *)
  Definition isexact_pi_base (n : nat)
    : IsExact (Tr (-1)) (fmap (pPi n.+1) f) (pi_connecting_map n)
    := les_isexact _ _ Pi_les (n, inr tt).

End PiLES.

(** [F], [X] and [Y] cannot be inferred from the index, so we make them explicit, as they are in [loops_carrier]. *)
Arguments pi_carrier F X Y n : clear implicits.
Arguments pequiv_pi_carrier F X Y n : clear implicits.