Theorem injective_pairing_uip : injective_pairing_statement → uip_statement. Proof. intros injpair A x y p q. assert (eqpair : @paths (∑ x, x = y) (x ,, p) (x ,, q)). { induction p. induction q. use total2_paths_f; apply idpath. } unfold injective_pairing_statement in injpair. exact (injpair _ (λ x, x = y) x p q eqpair). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.