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, in the sense that a formula from the fragment is derivable in intuitionistic first-order logic if, and only if, its interpretation in dependent type theory is inhabited. As a consequence, a modified double-negation translation into type theory (without bracket types) is complete, in the same sense, for all of classical first-order logic
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
A Note on Russell's Paradox in Locally Cartesian Closed Categories.Andrew M. Pitts & Paul Taylor - 1989 - Studia Logica 48 (3):377 - 387.
Syntactic Calculus with Dependent Types.Aarne Ranta - 1998 - Journal of Logic, Language and Information 7 (4):413-431.
The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
The Logic of First Order Intuitionistic Type Theory with Weak Sigma- Elimination.M. D. G. Swaen - 1991 - Journal of Symbolic Logic 56 (2):467-483.
An Intensional Type Theory: Motivation and Cut-Elimination.Paul C. Gilmore - 2001 - Journal of Symbolic Logic 66 (1):383-400.
An Interpretation of Martin-Löf's Type Theory in a Type-Free Theory of Propositions.Jan Smith - 1984 - Journal of Symbolic Logic 49 (3):730-753.
Lascar Types and Lascar Automorphisms in Abstract Elementary Classes.Tapani Hyttinen & Meeri Kesälä - 2010 - Notre Dame Journal of Formal Logic 52 (1):39-54.
A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems.Fairouz Kamareddine & Twan Laan - 2001 - Journal of Logic, Language and Information 10 (3):375-402.
The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory.Bart Jacobs - 1989 - Journal of Philosophical Logic 18 (4):399 - 422.
Added to index2010-09-14
Total downloads13 ( #351,847 of 2,164,583 )
Recent downloads (6 months)3 ( #128,912 of 2,164,583 )
How can I increase my downloads?