Subspaces of an arithmetic universe via type theory
Logic
2010-11-17 v1
Abstract
We define the notion of subspace of an arithmetic universe by using its internal dependent type theory.
Keywords
Cite
@article{arxiv.1011.3607,
title = {Subspaces of an arithmetic universe via type theory},
author = {Maria Emilia Maietti},
journal= {arXiv preprint arXiv:1011.3607},
year = {2010}
}