**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

In a dependent type theory with identity types, a **subtype** of a type $A$ is a type $B$ with a term $i: B \subseteq A$, with the inclusion relation defined as

$B \subseteq A \coloneqq \left[\sum_{f:B \to A} is1Monic(f)\right]$

indicating the mere existence of a 1-monic function or embedding, where $[T]$ is the propositional truncation of $T$. $A$ is a **supertype** of $B$.

This is different from a subtype with a chosen 1-monic function, a type $B$ with a term $i:B \hookrightarrow A$, with the type of 1-monic functions defined as

$B \hookrightarrow A \coloneqq \sum_{f:B \to A} is1Monic(f)$

in the same way that inhabited sets and pointed sets are different. However, equipping a type with an explicit 1-monic function is usually more useful in mathematics without the axiom of choice.

In a dependent type theory with identity types and a hierarchy of type universes a la Tarski, given a universe $(\mathcal{U},\mathcal{T}_{\mathcal{U}})$ a subtype of a type $A:\mathcal{U}$ is a function $B:\mathcal{T}_{\mathcal{U}}(A) \to \mathrm{Prop}_\mathcal{U}$. In a universe these are the same as subtypes equipped with a 1-monic function as structure.

The type of all subtypes of $B$ in a universe is defined as

$Sub_\mathcal{U}(B) \coloneqq \sum_{A:\mathcal{U}} \mathcal{T}_\mathcal{U}(A) \subseteq B$

Last revised on June 17, 2022 at 17:42:33. See the history of this page for a list of all contributions to it.