(X : pType) : loop_susp_counit (psusp X) o* fmap psusp (loop_susp_unit X) ==* pmap_idmap. Proof. simple refine (Build_pHomotopy _ _); [ simple refine (Susp_ind _ _ _ _) | ]; try reflexivity; cbn. - exact (merid (point X)). - intros x. rewrite transport_paths_FlFr, ap_idmap, ap_compose. rewrite Susp_rec_beta_merid. apply moveR_pM; rewrite concat_p1. refine (inverse2 (Susp_rec_beta_merid _) @ _). rewrite inv_pp, inv_V; 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.