We present a generalisation of the type-theoretic interpretation of
constructive set theory into Martin-Löf type theory. The
generalisation involves replacing Martin-Löf type theory with a
new type theory in which logic is treated as primitive instead of
being formulated via the propositions-as-types representation. 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.