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
Where the idea of (non-higher) observational type theory is to equip all type formation rules (notably dependent functions, dependent pairs and inductive constructions) with their dedicated notion of structure preserving definitional equality — namely: component-wise, ie. homo-morphic, hence: “observational” —; the idea of higher observational type theory is to do the same for propositional equality hence for identification types used in homotopy type theory (where types behave like *higher* homomotopy types, whence the qualifier “higher”).
Concretely:
the “observational” principle for identification of dependent functions is to say that these are dependent functions of identifications of arguments and values (a statement otherwise known as function extensionality),
the “observational” principle for identifications of dependent pairs is to say that these are dependent pairs of identifications of factors,
and in ordinary univalent homotopy type theory this form of the “structure identity principle” follows as a type equivalence between identification types:
The idea of higher observational type theory is to make these and analogous structural characterizations of identification types be part of their definitional inference rules, thus building the structure identity principle right into the rewrite rules of the type theory.
In such a higher observational theory, in particular also the univalence axiom would be a definitional equality and hence would “compute”.
This most desirable property of any homotopy type theory has previously been accomplished only by cubical type theories. However, cubical type theories achieve this only by adding syntax for auxiliary/spurious interval types with rewrite rules which encode technical detail that has no abstract motivation other than making the univalence axiom compute and which one would rather keep out of the syntactic logic and instead relegate to the construction of categorical semantics.
The hope is therefore that higher observational type theory would provide a type system which achieves both:
its syntax is as logically clean as that of Martin-Löf dependent type theory equipped with the univalence axiom;
its inference rules for identification types make the univalence axiom be a computable function as it is in cubical type theories.
To which extent this hope is being realized would ideally be elucidated by the references below.
This section does not quite get to the key points across and may need to be largely rewritten from scratch.
We are working in a dependent type theory with judgmental equality.
telescope types contain lists of iteratively dependent terms
Rules for the empty telescope
Rules for telescopes given a telescope and a type
Rules for the empty context in a telescope
Rules for …
…
…
…
The identity types in higher observational type theory is defined as
Computation rules are defined for pair types:
Computation rules are defined for function types:
Computation rules are defined for dependent function types:
Computation rules are defined for dependent pair types:
…
We are working in a dependent type theory with Tarski-style universes.
The identity types in a universe in higher observational type theory have the following formation rule:
We define a general congruence term called ap
and the reflexivity terms:
and computation rules for identity functions
and for constant functions $y$
Thus, ap is a higher dimensional explicit substitution. There are definitional equalities
for constant term $t$.
Let $A \cong_\mathcal{U} B$ be the type of one-to-one correspondences between two terms of a universe $A:\mathcal{U}$ and $B:\mathcal{U}$, and let $\mathrm{id}_\mathcal{U}(A, B)$ be the identity type between two terms of a universe $A:\mathcal{U}$ and $B:\mathcal{U}$. Then there are rules
Given a term of a universe $A:\mathcal{U}$
with terms representing singleton contractibility.
Given a term of a universe $A:\mathcal{U}$, a judgment $z:\mathcal{T}_\mathcal{U}(A) \vdash B:\mathcal{U}$, terms $x:\mathcal{T}_\mathcal{U}(A)$ and $y:\mathcal{T}_\mathcal{U}(A)$, and an identity $p:\mathrm{id}_{\mathcal{T}_\mathcal{U}(A)}(x,y)$, we have
and
We could define a dependent identity type as
There is a rule
and for constant families $B:\mathcal{U}$
Higher observational type theory was introduced as joint work of Thorsten Altenkirch, Ambrus Kaposi and Michael Shulman, first presented in:
Michael Shulman, Towards a Third-Generation HOTT:, talk at Homotopy Type Theory at CMU (2022) [part 1: slides, video; part 2: slides, video; part 3: slides, video]
Agda code: github.com/mikeshulman/ohtt
Last revised on August 29, 2023 at 06:30:28. See the history of this page for a list of all contributions to it.