Subspaces of an arithmetic universe via type theory
Logic
2012-02-08 v2
Abstract
We define the notion of subspace of an arithmetic universe by using its internal dependent type theory.
Keywords
Cite
@article{arxiv.1011.1226,
title = {Subspaces of an arithmetic universe via type theory},
author = {Maria Emilia Maietti},
journal= {arXiv preprint arXiv:1011.1226},
year = {2012}
}
Comments
This paper has been withdrawn by the author due to a further submission of a more correct copy