Lemma univ_surj_unique : ∏ (g : B -> C) (H : ∏ a : A, g (p a) = f a) (b : B), g b = univ_surj b. Proof. intros g H b. apply (surjectionisepitosets p); [assumption|assumption|]. intro x. rewrite H,univ_surj_ax. apply idpath. Qed.
Require Import UniMath.Foundations.UnivalenceAxiom.