proposition: Lemma total2_paths_equiv'_compute {A : UU} (B : A -> UU) (x y : ∑ x, B x) : pr1weq (total2_paths_equiv' B x y) = (λ (r : x = y), base_paths _ _ r ,, fiber_paths r).
proof: Proof. reflexivity. Defined.
imports: UniMath.MoreFoundations.Notations