{X Y : Type} {r : X -> Y} (s : Y -> X) (h : forall y:Y, r (s y) = y) : IsSurjection r. Proof. intro y. rapply contr_inhabited_hprop. exact (tr (s y; h y)). Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.