(** * Spectra *)

Require Import HoTT.Basics HoTT.Types.
Require Import Pointed.

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

(** ** Basic Definitions of Spectra *)

Record Prespectrum :=
  { deloop :> nat -> pType
    ; glue : forall n, deloop n ->* loops (deloop (n .+1)) }.

Class IsSpectrum (E : Prespectrum) :=
  is_equiv_glue :: forall n, IsEquiv (glue E n).

Definition equiv_glue (E : Prespectrum) `{IsSpectrum E}
: forall n, E n <~>* loops (E n.+1)
  := fun n => Build_pEquiv (glue E n) _.

Record Spectrum :=
  { to_prespectrum :> Prespectrum
    ; to_is_spectrum :: IsSpectrum to_prespectrum }.

(** ** Truncations of spectra *)

Definition strunc `{Univalence} (k : trunc_index) (E : Spectrum) : Spectrum.
H: Univalence
k: trunc_index
E: Spectrum
Spectrum
Proof.
H: Univalence
k: trunc_index
E: Spectrum
Spectrum
  simple refine (Build_Spectrum (Build_Prespectrum (fun n => pTr (trunc_index_inc k n) (E n)) _) _).
H: Univalence
k: trunc_index
E: Spectrum
forall n : nat,
(fun n0 : nat => pTr (trunc_index_inc k n0) (E n0)) n ->*
loops ((fun n0 : nat => pTr (trunc_index_inc k n0) (E n0)) n.+1)
H: Univalence
k: trunc_index
E: Spectrum
IsSpectrum
  {|
    deloop := fun n : nat => pTr (trunc_index_inc k n) (E n); glue := ?glue
  |}
  -
H: Univalence
k: trunc_index
E: Spectrum
forall n : nat,
(fun n0 : nat => pTr (trunc_index_inc k n0) (E n0)) n ->*
loops ((fun n0 : nat => pTr (trunc_index_inc k n0) (E n0)) n.+1) intros n.
H: Univalence
k: trunc_index
E: Spectrum
n: nat
(fun n0 : nat => pTr (trunc_index_inc k n0) (E n0)) n ->*
loops ((fun n0 : nat => pTr (trunc_index_inc k n0) (E n0)) n.+1)
    exact ((ptr_loops _ (E n.+1)) o*E (pequiv_ptr_functor _ (equiv_glue E n))).
  -
H: Univalence
k: trunc_index
E: Spectrum
IsSpectrum
  {|
    deloop := fun n : nat => pTr (trunc_index_inc k n) (E n);
    glue :=
      fun n : nat =>
      ptr_loops (trunc_index_inc k n) (E n.+1)
      o*E pequiv_ptr_functor (trunc_index_inc k n) (equiv_glue E n)
  |} intros n.
H: Univalence
k: trunc_index
E: Spectrum
n: nat
IsEquiv
  (glue
     {|
       deloop := fun n0 : nat => pTr (trunc_index_inc k n0) (E n0);
       glue :=
         fun n0 : nat =>
         ptr_loops (trunc_index_inc k n0) (E n0.+1)
         o*E pequiv_ptr_functor (trunc_index_inc k n0) (equiv_glue E n0)
     |} n) unfold glue.
H: Univalence
k: trunc_index
E: Spectrum
n: nat
IsEquiv
  (ptr_loops (trunc_index_inc k n) (E n.+1)
   o*E pequiv_ptr_functor (trunc_index_inc k n) (equiv_glue E n))
    rapply isequiv_compose.
Defined.