We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Lof type theory The original interpretation treated logic in Martin-Lof type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Lof 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.
展开▼
