`{Funext} (A : pType) : NatEquiv (opyon (psusp A)) (opyon A o loops). Proof. rapply Build_NatEquiv. 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.