(X : pType) : fmap loops (loop_susp_counit X) o* loop_susp_unit (loops X) ==* pmap_idmap. Proof. simple refine (Build_pHomotopy _ _). - intros p; cbn. refine (concat_1p _ @ (concat_p1 _ @ _)). refine (ap_pp (Susp_rec (point X) (point X) idmap) (merid p) (merid (point (point X = point X)))^ @ _). refine ((1 @@ ap_V _ _) @ _). refine ((Susp_rec_beta_merid p @@ inverse2 (Susp_rec_beta_merid (point (loops X)))) @ _). exact (concat_p1 _). - apply moveL_pV. destruct X as [X x]; cbn; unfold point. apply whiskerR. rewrite (concat_pV_inverse2 (ap (Susp_rec x x idmap) (merid 1)) 1 (Susp_rec_beta_merid 1)). rewrite (ap_pp_concat_pV (Susp_rec x x idmap) (merid 1)). rewrite ap_compose, (ap_compose _ (fun p => p @ 1)). rewrite concat_1p_1; apply ap. apply concat_p1_1. 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.