`{Funext} (X Y : Type) : (Susp X -> Y) <~> { NS : Y * Y & X -> fst NS = snd NS }. Proof. snrapply equiv_adjointify. - intros f. exists (f North, f South). intros x; exact (ap f (merid x)). - intros [[N S] m]. exact (Susp_rec N S m). - intros [[N S] m]. apply ap, path_arrow. intros x; apply Susp_rec_beta_merid. - intros f. symmetry; apply Susp_rec_eta. Defined.
Require Import Basics. Require Import Types. Require Import Cubical.DPath Cubical.DPathSquare. Require Import WildCat. Require Import Colimits.Pushout. Require Import NullHomotopy. Require Import Truncations.Core. Require Import Modalities.Modality. Require Import Extensions.