`{Univalence} (A : Type) : merely (exists X:HSet, exists p : X -> A, IsSurjection p). Proof. pose (X := Build_HSet (Tr 0 A)). pose proof ((equiv_isoprojective_hasochoice _ X)^-1 (AC X)) as P. pose proof (P A _ X _ idmap tr _) as F; clear P. strip_truncations. destruct F as [f p]. refine (tr (X; (f; BuildIsSurjection f _))). intro a; unfold hfiber. apply equiv_O_sigma_O. refine (tr (tr a; _)). rapply (equiv_path_Tr _ _)^-1%equiv. apply p. Defined.
Require Import Basics Types. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Modalities.Modality Modalities.Identity. Require Import Limits.Pullback.