The generalised type-theoretic interpretation of constructive set theory
Keyword(s):
New Type
◽
AbstractWe present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation.
Keyword(s):
2010 ◽
Vol 75
(4)
◽
pp. 1137-1146
◽
2019 ◽
Vol 169
(1)
◽
pp. 1-18
◽
1998 ◽
Vol 94
(1-3)
◽
pp. 181-200
◽
Keyword(s):
2014 ◽
Vol 14
(01)
◽
pp. 1450005
◽
Keyword(s):
2006 ◽
Vol 141
(1-2)
◽
pp. 257-265
◽