(* -*- mode: coq; mode: visual-line -*- *)

(** * Spectra *)

Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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).

Global Existing Instance is_equiv_glue.

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

Global Existing Instance to_is_spectrum.

(** ** 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 n : nat => pTr (trunc_index_inc k n) (E n)) n ->*
loops
  ((fun n : nat => pTr (trunc_index_inc k n) (E n))
     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 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)
     |} 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))
    srapply isequiv_compose.
Defined.