`{Univalence} (X : Type) : IsProjective X <~> IsHSet X. Proof. apply equiv_iff_hprop. - intro isprojX. unfold IsOProjective in isprojX. pose proof (projective_cover_AC X) as P; strip_truncations. destruct P as [P [p issurj_p]]. pose proof (isprojX P _ X _ idmap p issurj_p) as S; strip_truncations. exact (inO_retract_inO (Tr 0) X P S.1 p S.2). - intro ishsetX. apply (equiv_isoprojective_hasochoice purely X)^-1. rapply AC. Defined.
Require Import Basics Types. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Modalities.Modality Modalities.Identity. Require Import Limits.Pullback.