Lemma issurjective_idfun (X : UU) : issurjective (idfun X). Proof. exact(λ (x : X), hinhpr (x ,, idpath x)). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.