`{Univalence} (X : pType) `{IsHSpace X} `{forall a, IsEquiv (a *.)} : pFam (psusp X). Proof. srapply Build_pFam. - apply (Susp_rec (Y:=Type) X X). exact (fun x => path_universe (x *.)). - simpl. exact pt. Defined.
Require Import Types Basics Pointed Truncations. Require Import HSpace Suspension ExactSequence HomotopyGroup. Require Import WildCat.Core WildCat.Universe WildCat.Equiv Modalities.ReflectiveSubuniverse Modalities.Descent. Require Import HSet Spaces.Nat.Core. Require Import Homotopy.Join Colimits.Pushout.