proposition: Lemma iff_merely_issurjection {X : Type} (P : X -> Type) : (forall x, merely (P x)) <-> IsSurjection (pr1 : {x : X & P x} -> X).
proof: Proof. refine (iff_compose _ (iff_forall_inO_mapinO_pr1 (Conn _) P)). apply iff_functor_forall; intro a. symmetry; apply (iff_contr_hprop (Tr (-1) (P a))). Defined.
imports: Basics Types WildCat.Core WildCat.Universe Modalities.Modality (coercions) Modalities.Modality