Dear Vasya, The equivalence is given in Propositions 2.1 and 2.2 and Theorem 2.4. We can introduce the logical connectives as primitives and then define equality; or we can introduce equality as a primitive and define the logical connectives in terms of =. Either way gives the same set of derivable judgements. -- Robin Adams On 19/06/14 09:12, Vasili I. Galchin wrote:

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/ ]