{X Y : pType} (f : X ->* Y) : f o* loop_susp_counit X ==* loop_susp_counit Y o* fmap psusp (fmap loops f). Proof. pointed_reduce. simple refine (Build_pHomotopy _ _); simpl. - simple refine (Susp_ind _ _ _ _); cbn; try reflexivity; intros p. rewrite transport_paths_FlFr, ap_compose, concat_p1. apply moveR_Vp. refine (ap_compose (Susp_rec North South (fun x0 => merid (1 @ (ap f x0 @ 1)))) (Susp_rec (point Y) (point Y) idmap) (merid p) @ _). do 2 rewrite Susp_rec_beta_merid. refine (concat_1p _ @ _). f_ap. f_ap. symmetry. refine (Susp_rec_beta_merid _). - reflexivity. Qed.
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.