With Alex Simpson.

Abstract: We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space (CSM) without isolated points, `X`, in such a way that every sequentially continuous function from Cantor space to `ZZ` extends to a sequentially continuous function from `X` to `RR`. The second asserts an analogous property for Baire space relative to any inhabited locally non-compact CSM. Both results rely on having careful constructive formulations of the concepts involved.

As a first application, we derive new relationships between “continuity principles” asserting that all functions between specified metric spaces are pointwise continuous. In particular, we give conditions that imply the failure of the continuity principle “all functions from `X` to `RR` are continuous”, when `X` is an inhabited CSM without isolated points, and when `X` is an inhabited locally non-compact CSM. One situation in which the latter case applies is in models based on “domain realizability”, in which the failure of the continuity principle for any inhabited locally non-compact CSM, `X`, generalizes a result previously obtained by Escardo and Streicher in the special case `X = C[0,1]`.

As a second application, we show that, when the notion of inhabited complete separable metric space without isolated points is interpreted in a recursion-theoretic setting, then, for any such space `X`, there exists a Banach-Mazur computable function from `X` to the computable real numbers that is not Markov computable. This generalizes a result obtained by Hertling in the special case that `X` is the space of computable real numbers.

Published in: Mathematical Logic Quarterly, 50(4,5):351-369, 2004.

Download: continuity.pdf, continuity.ps.gz

→ continue reading

With Steve Awodey.

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.

Published in: Journal of Logic and Computation. Volume 14, Issue 4, August 2004, pp. 447-471.

Download: bracket_types.pdf, bracket_types.ps.gz

→ continue reading (2 comments)