**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**

Type theory with shapes is a layered type theory consisting of a dependent type theory over a typed predicate logic with finite product types. The type layer of the typed predicate logic is called the **cube layer**, whose types are called **cubes**, the propositional logic layer of the typed predicate logic is called the **tope layer**, whose types are called **topes**, and the type layer of the dependent type theory is called the **type layer**, whose types are called **types**. Shapes are then built out of cubes and topes.

Type theory with shapes is used in some formalizations of simplicial type theory and cubical type theory as an alternative to two-level type theory.

The cube layer is a type theory which consists of finite product types.

$\frac{}{() \; \mathrm{cubectx}} \qquad \frac{\Xi \; \mathrm{cubectx} \quad \Xi \vdash I \; \mathrm{cube}}{\Xi, t:I \; \mathrm{cubectx}} \quad \frac{\Xi, t:I, \Xi' \; \mathrm{cubectx}}{\Xi, t:I, \Xi' \vdash t:I}$

$\frac{\Xi \; \mathrm{cubectx}}{\Xi \vdash \mathbb{1} \; \mathrm{cube}} \qquad \frac{\Xi \vdash I \; \mathrm{cube} \quad \Xi \vdash J \; \mathrm{cube}}{\Xi \vdash I \times J \; \mathrm{cube}}$

The tope layer is an intuitionistic logic over the cube layer, and the types in the tope layer are called topes because they can be interpreted as polytopes embedded in a cube. There is a tope representing equality of terms of cubes, called the *equality tope* and given the symbol $\equiv_I$ for cube $I$. The equality tope is used to define the eta and beta conversion rules for finite product cubes.

$\frac{\Xi \; \mathrm{cubectx}}{\Xi \vert () \; \mathrm{topectx}} \qquad \frac{\Xi \vert \Phi \; \mathrm{topectx} \quad \Xi \vert \Phi \vdash \phi \; \mathrm{tope}}{\Xi \vert \Phi, \phi \; \mathrm{topectx}} \quad \frac{\Xi \vert \Phi, \phi, \Phi' \; \mathrm{topectx}}{\Xi \vert \Phi, \phi, \Phi' \vdash \phi}$

Shapes are a cube with a tope in the context of a term of the cube

$\frac{\Xi \vdash I \: \mathrm{cube} \quad \Xi, t:I \vdash \phi \; \mathrm{tope}}{\Xi \vdash \{t:I \vert \phi \} \; \mathrm{shape}}$

This type layer is a dependent type theory with some notion of identity type, dependent product type, dependent sum type, and higher inductive types, as well as judgmental equality to reflect the equality tope of the tope layer, and cube contexts and tope contexts in addition to the usual type contexts. The beta conversion and eta conversion rules for the types may either be typal or judgmental. In addition, there is no equality reflection rule, which makes the dependent type theory an intensional type theory.

It is also possible to combine the cube layer and the tope layer together into one layer of shapes, just as in traditional mathematics it is possible to combine the set layer and the logic layer into one layer of types. However, the resulting theory is just a two-level type theory where the non-fibrant types are called “shapes”.

- simplicial type theory
- cubical type theory
- two-level type theory
- extension type, dependent extension type

- Emily Riehl, Michael Shulman,
*A type theory for synthetic $\infty$-categories*$[$arXiv:1705.07442$]$

Last revised on May 20, 2023 at 01:09:48. See the history of this page for a list of all contributions to it.