Lemma totalfst_display {A: Type} (Bf: ∑ B, B -> A) : totalfst (display Bf) = Bf. Proof. use total2_paths_f. - apply weqtopaths. apply sum_of_fibers. - rewrite transportf_fun. rewrite <- eqweqmap_transportb. rewrite eqweqmap_pathsinv0. rewrite eqweqmap_weqtopaths. reflexivity. Defined.