From mboxrd@z Thu Jan  1 00:00:00 1970
X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2015
Path: news.gmane.org!not-for-mail
From: Steve Awodey <awodey@cmu.edu>
Newsgroups: gmane.science.mathematics.categories
Subject: preprint: Propositions as [Types]
Date: Thu, 14 Jun 2001 16:22:34 -0500
Message-ID: <3B292B1A.5030706@cmu.edu>
NNTP-Posting-Host: main.gmane.org
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
X-Trace: ger.gmane.org 1241018285 1746 80.91.229.2 (29 Apr 2009 15:18:05 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Wed, 29 Apr 2009 15:18:05 +0000 (UTC)
To: categories@mta.ca
Original-X-From: rrosebru@mta.ca Fri Jun 15 14:39:39 2001 -0300
Return-Path: <cat-dist@mta.ca>
Original-Received: (from Majordom@localhost)
	by mailserv.mta.ca (8.11.1/8.11.1) id f5FH73s17820
	for categories-list; Fri, 15 Jun 2001 14:07:03 -0300 (ADT)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
User-Agent: Mozilla/5.0 (X11; U; Linux 2.2.13 i686; en-US; 0.8.1) Gecko/20010421
X-Accept-Language: en
Original-Sender: cat-dist@mta.ca
Precedence: bulk
X-Keywords: 
X-UID: 26
Original-Lines: 48
Xref: news.gmane.org gmane.science.mathematics.categories:2015
Archived-At: <http://permalink.gmane.org/gmane.science.mathematics.categories/2015>

Dear Colleagues,

This is to announce that the Mittag-Leffler technical report listed 
below is available at the addresses given.

Best regards,

Steve Awodey

http://andrej.com/brackets

or

http://www.ml.kva.se/preprints/meta/AwodeyTue_Jun_12_10_31_49.rdf.html

*******************************************************************************************************

Propositions as [Types]

Steve Awodey , Andrej Bauer


Abstract:
Image factorizations in regular categories are stable under
pullbacks, so they model a natural modal operator in dependent type
theory. This unary type constructor [A] has turned up previously
in a syntactic form as a way of erasing computational content, and
formalizing a notion of proof irrelevance. Indeed, semantically,
the notion of a support is sometimes used as surrogate
proposition asserting inhabitation of an indexed family.

We give rules for bracket types in dependent type theory and provide
complete semantics using regular categories. We show that dependent
type theory with the unit type, strong extensional equality types,
strong dependent sums, and bracket types is the internal type theory
of regular categories, in the same way that the usual dependent type
theory with dependent sums and products is the internal type theory
of locally cartesian closed categories.

We also show how to interpret first-order logic in type theory with
brackets, and we make use of the translation to compare type theory
with logic. Specifically, we show that the propositions-as-types
interpretation is complete with respect to a certain fragment of
intuitionistic first-order logic. As a consequence, a modified
double-negation translation into type theory (without bracket types)
is complete for all of classical first-order logic.