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

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.

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

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

Global Existing Instance is_equiv_glue.

Definition equiv_glue (E : Prespectrum) `{IsSpectrum E}
: ∀ 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.

Definition strunc `{Univalence} (k : trunc_index) (E : Spectrum) : Spectrum.
Proof.
  simple refine (Build_Spectrum (Build_Prespectrum (fun n ⇒ pTr (trunc_index_inc k n) (E n)) _) _).
  - intros n.
    exact ((ptr_loops _ (E n.+1)) o×E (pequiv_ptr_functor _ (equiv_glue E n))).
  - intros n. unfold glue.
    srapply isequiv_compose.
Defined.