proposition: 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: Proof. apply pathsinv0. apply (transport_map (λ a, pr1 (P := P a))). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics