preprint: Propositions as [Types]

[Steve Awodey <awodey@cmu.edu>]

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.