In type theory, the notation $(x : A) \to B (x)$ instead of $\Pi_{x : A} B (x)$ for the dependent product and $(x : A) \times B (x)$ instead of $\Sigma _{x : A} B (x)$ for the dependent sum. For non-type-theorists, a dependent product is a set-indexed product of a collection of sets, and a dependent sum is a set-indexed disjoint union of a collection of sets[1]. The former notation is used in the [Agda](http://wiki.portal.chalmers.se/agda/pmwiki.php), the latter is less widely spread but both are used for example in [cubicaltt](https://github.com/mortberg/cubicaltt). Some advantages of this notation are:

* It is consistent with notation for non-dependent sums and products $A \times B$ and $A \to B$ (the latter is in fact an instance of the third example of good notation given in the original question, and is already widespread among type-theorists as a notation for the set of functions from $A$ to $B$)

* The fact that $A$ does not appear as a subscript certain complex types easier to follow, as in the equation

$$ (x : A) \times ((y : B (x)) \times C (x, y)) \cong (u : (x : A) \times B (x)) \times C (\pi_1 u, \pi_2 u) $$

* The fact that $A$ does not appear as a subscript makes it easier to represent this notation in plaintext, as is frequently done when programming with dependent types.

[1] Here and in the rest of my answer, I am ignoring the distinction between a set and a type.