proposition: Lemma pr1_transportf_const {A : UU} {B : UU} {P : ∏ (a : A), B -> UU} {a a' : A} (e : a = a') (xs : ∑ b : B, P a b) : pr1 (transportf (λ x, ∑ b : B, P _ b) e xs) = pr1 xs.
proof: Proof. rewrite pr1_transportf. rewrite transportf_const. reflexivity. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three