`{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.
Require Import HoTT.Basics HoTT.Types. Require Import Pointed.