proposition: Lemma transportf_total2_const (A B : UU) (P : B -> A -> UU) (b : B) (a1 a2 : A) (e : a1 = a2) (p : P b a1) : transportf (λ x, ∑ y, P y x) e (b,, p) = b,, transportf (P b) e p.
proof: Proof. induction e. apply idpath. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics