`{Univalence} (X : pType) n `{IsConnected n.+1 X} : pTr (n +2+ n) X <~>* pTr (n +2+ n) (loops (psusp X)). Proof. snrapply Build_pEquiv. 1:rapply (fmap (pTr _) (loop_susp_unit _)). rapply O_inverts_conn_map. 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.