Lemma univ_surj_ax : ∏ x, univ_surj (p x) = f x. Proof. intro x. apply pathsinv0. apply path_to_ctr. apply (squash_to_prop (surjectivep (p x))). { apply isapropishinh. } intro r. apply hinhpr. exists r. apply comp_f_epi. apply (pr2 r). Qed.
Require Import UniMath.Foundations.UnivalenceAxiom.