`{Univalence} (A B : pType@{u}) : A <~>* B <~> A = B. Proof. refine (equiv_path_from_contr A (fun C => A <~>* C) pequiv_pmap_idmap _ B). nrapply (contr_equiv' { X : Type@{u} & { f : A <~> X & {x : X & f pt = x} }}). 1: make_equiv. rapply (contr_equiv' { X : Type@{u} & A <~> X }). nrapply equiv_functor_sigma_id; intro X; symmetry. rapply equiv_sigma_contr. Defined.
Require Import Basics Types. Require Import Homotopy.IdentitySystems. Require Import WildCat. Require Import Truncations.Core. Require Import ReflectiveSubuniverse. Require Import Extensions.