Lemma total2_section_path {X:UU} {Y:X->UU} (a:X) (b:Y a) (e:∏ x, Y x) : (a,,e a) = (a,,b) -> e a = b. Proof. intros p. simple refine (_ @ fiber_paths p). unfold base_paths. simpl. apply pathsinv0, transport_section. Defined.