`{Funext} {X : Type} (P : X -> Type) : (forall x, merely (P x)) <~> IsSurjection (pr1 : {x : X & P x} -> X). Proof. exact (equiv_iff_hprop_uncurried (iff_merely_issurjection P)). Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.