proposition: Theorem injective_pairing_uip : injective_pairing_statement → uip_statement.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Univalence