proposition: Theorem equiv_isprojective_ishset_AC `{Univalence} (X : Type) : IsProjective X <~> IsHSet X.
proof: 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.
imports: Basics Types Truncations.Core Truncations.SeparatedTrunc Modalities.Modality Modalities.Identity Limits.Pullback