Lemma pr2_transportf {A} {B1 B2 : A → UU} {a a' : A} (e : a = a') (xs : B1 a × B2 a) : pr2 (transportf (λ a, B1 a × B2 a) e xs) = transportf _ e (pr2 xs). Proof. apply pathsinv0. apply (transport_map (λ a, pr2 (P := λ _, B2 a))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.