(X : Type) : pType := [Susp X, _]. Global Instance is0functor_psusp : Is0Functor := Build_Is0Functor _ _ _ _ (fun X Y f => Build_pMap ( X) ( Y) (functor_susp f) 1). Global Instance is1functor_psusp : Is1Functor . Proof. snrapply Build_Is1Functor. - intros X Y f g p. pointed_reduce. srapply Build_pHomotopy. { simpl. srapply Susp_ind. 1,2: reflexivity. intro x; cbn. rewrite transport_paths_FlFr. rewrite concat_p1. rewrite 2 Susp_rec_beta_merid. destruct (p x). apply concat_Vp. } reflexivity. - intros X. srapply Build_pHomotopy. { srapply Susp_ind; try reflexivity. intro x. refine (transport_paths_FFlr _ _ @ _). by rewrite ap_idmap, Susp_rec_beta_merid, concat_p1, concat_Vp. } reflexivity. - pointed_reduce_rewrite; srefine (Build_pHomotopy _ _); cbn. { srapply Susp_ind; try reflexivity; cbn. intros x. refine (transport_paths_FlFr _ _ @ _). rewrite concat_p1; apply moveR_Vp. by rewrite concat_p1, ap_compose, !Susp_rec_beta_merid. } reflexivity. Defined.
Require Import Basics. Require Import Types. Require Import Pointed.Core. Require Import Pointed.Loops. Require Import Pointed.pTrunc. Require Import Pointed.pEquiv. Require Import Homotopy.Suspension. Require Import Homotopy.Freudenthal. Require Import Truncations. Require Import WildCat.