{A B} (f : A -> B) : (forall b, merely (hfiber f b)) -> IsSurjection f. Proof. intros H b; refine (contr_inhabited_hprop _ _). apply H. Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.