Lemma pr1_transportf {A : UU} {B : A -> UU} {P : ∏ a, B a -> UU} {a a' : A} (e : a = a') (xs : ∑ b : B a, P _ b): pr1 (transportf (λ x, ∑ b : B x, P _ b) e xs) = transportf (λ x, B x) e (pr1 xs). Proof. apply pathsinv0. apply (transport_map (λ a, pr1 (P := P a))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.