proposition: Lemma equiv_merely_issurjection `{Funext} {X : Type} (P : X -> Type) : (forall x, merely (P x)) <~> IsSurjection (pr1 : {x : X & P x} -> X).
proof: Proof. exact (equiv_iff_hprop_uncurried (iff_merely_issurjection P)). Defined.
imports: Basics Types WildCat.Core WildCat.Universe Modalities.Modality (coercions) Modalities.Modality