Intro to higher order categorical logic question

Hello, In the "Introduction to Part II" paragraph one , two type theories are mentioned. The last sentence of this paragraph states "These two versions are shown to be equivalent, although the second(equality .. my words) is useful for describing the internal language of a topos". Question: In what sense are these two type theory equivalent? In some technical sense? Kind regards, Vasya [For admin and other information see: http://www.mta.ca/~cat-dist/ ]