(X : pType) : X ->* loops (psusp X) := Build_pMap X (loops (psusp X)) (fun x => merid x @ (merid (point X))^) (concat_pV _). Global Instance conn_map_loop_susp_unit `{Univalence} (n : trunc_index) (X : pType) `{IsConnected n.+1 X} : IsConnMap (n +2+ n) ( X). Proof. refine (conn_map_compose _ merid (equiv_concat_r (merid pt)^ _)). 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.