Theorem uip_injective_pairing : uip_statement → injective_pairing_statement. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.