Subspaces of an arithmetic universe via type theory

TL;DR

This paper introduces a novel approach to defining subspaces within arithmetic universes by leveraging their internal dependent type theory, offering a new perspective on their structural properties.

Contribution

It presents the first formal definition of subspaces of arithmetic universes using internal dependent type theory, bridging category theory and type theory.

Findings

Provides a formal framework for subspaces in arithmetic universes

Establishes connections between type theory and categorical structures

Lays groundwork for further exploration of internal structures

Abstract

We define the notion of subspace of an arithmetic universe by using its internal dependent type theory.