Subspaces of an arithmetic universe via type theory
arXiv:1011.1226
Abstract
We define the notion of subspace of an arithmetic universe by using its internal dependent type theory.
arXiv commentThis paper has been withdrawn by the author due to a further submission of a more correct copy