Church's simple type theory is known to be equiconsistent to a bounded version of Zermelo's set theory (using only bounded quantifiers).
Is there also a type theoretical formulation of mathematical foundations which is equiconsistent to some unbounded set theory based on Zermelo's work?
Yes, there is a type theory equiconsistent with unbounded Zermelo set theory. In the paper λZ: Zermelo's Set Theory as a PTS with 4 Sorts Alexandre Miquel presents a type theory $\mathrm{\lambda Z}$ that is shown equiconsitent to the Zermelo Set Theory $\mathrm{Z}$. This type theory $\mathrm{\lambda Z}$ is a subsystem of System $F\omega$ with universes.
The equiconsistency is shown by embedding $\mathrm{IZ} + \mathrm{AFA} + \mathrm{TC}$ (Intuinonistic Zermelo with Aczel's antifoundation axiom and the existance of transitive closures) into $\mathrm{\lambda Z}$ by representing sets as pointed graphs. This theory $\mathrm{IZ} + \mathrm{AFA} + \mathrm{TC}$ is itself equiconsistent to $\mathrm{Z}$.