Subspaces of an arithmetic universe via type theory

TL;DR

This paper introduces a new way to understand subspaces within arithmetic universes by leveraging their internal dependent type theory, providing a novel theoretical framework.

Contribution

It presents a novel definition of subspaces in arithmetic universes using internal dependent type theory, bridging category theory and type theory.

Findings

Defines subspaces via internal dependent type theory

Establishes a theoretical framework connecting arithmetic universes and type theory

Provides foundational insights for further research in categorical logic

Abstract

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