Via the formulas-as-types embedding certain extensions of Heyting Arithmetic can be represented in intuitionistic type theories. In this paper we discuss the embedding of $\omega$-sorted Heyting Arithmetic $\mathbf{HA}^\omega$ into a type theory $\mathbf{WL}$, that can be described as Troelstra's system $\mathbf{ML}^1_0$ with so-called weak $\Sigma$-elimination rules. By syntactical means it is proved that a formula is derivable in $\mathbf{HA}^\omega$ if and only if its corresponding type in $\mathbf{WL}$ is inhabited. Analogous results are proved for Diller's so-called restricted system and for a type theory based on predicate logic instead of arithmetic.