Lemma issurjective_tounit {X : UU} : X -> issurjective (@tounit X). Proof. intro x. apply(issurjective_to_contr x). apply iscontrunit. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.