proposition: Theorem uip_injective_pairing : uip_statement → injective_pairing_statement.
proof: Proof. intros uip A B a b b' eqpair. set (eqa := base_paths _ _ eqpair). assert (eqb : transportf _ eqa b = b'). { apply (fiber_paths eqpair). } assert (eqa_idpath : eqa = idpath _). { apply uip. } symmetry. etrans. { exact (! eqb). } exact (maponpaths (λ p, transportf B p b) eqa_idpath). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Univalence