From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8163 Path: news.gmane.org!not-for-mail From: "Vasili I. Galchin" Newsgroups: gmane.science.mathematics.categories Subject: Intro to higher order categorical logic question Date: Thu, 19 Jun 2014 02:12:00 -0500 Message-ID: Reply-To: "Vasili I. Galchin" NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 X-Trace: ger.gmane.org 1403216104 30939 80.91.229.3 (19 Jun 2014 22:15:04 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Thu, 19 Jun 2014 22:15:04 +0000 (UTC) To: Categories mailing list Original-X-From: majordomo@mlist.mta.ca Fri Jun 20 00:14:57 2014 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.186]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1Wxkbg-0004RY-CW for gsmc-categories@m.gmane.org; Fri, 20 Jun 2014 00:14:56 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:37027) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1Wxkap-0000pf-Iu; Thu, 19 Jun 2014 19:14:03 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1Wxkap-0005GA-4Q for categories-list@mlist.mta.ca; Thu, 19 Jun 2014 19:14:03 -0300 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8163 Archived-At: 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/ ]