* Intro to higher order categorical logic question
@ 2014-06-19 7:12 Vasili I. Galchin
2014-06-27 9:37 ` Robin Adams
0 siblings, 1 reply; 2+ messages in thread
From: Vasili I. Galchin @ 2014-06-19 7:12 UTC (permalink / raw)
To: Categories mailing list
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/ ]
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: Intro to higher order categorical logic question
2014-06-19 7:12 Intro to higher order categorical logic question Vasili I. Galchin
@ 2014-06-27 9:37 ` Robin Adams
0 siblings, 0 replies; 2+ messages in thread
From: Robin Adams @ 2014-06-27 9:37 UTC (permalink / raw)
To: categories
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/ ]
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2014-06-27 9:37 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-06-19 7:12 Intro to higher order categorical logic question Vasili I. Galchin
2014-06-27 9:37 ` Robin Adams
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).