Homotopy Type Theory higher observational type theory > history (Rev #8, changes)

Showing changes from revision #7 to #8: Added | Removed | Changed

Contents

Idea

Higher observational type theory involves a different definition of identity types where the identity types are defined recursively for each type former rather than uniformly across all types. types inintensional Martin-Loef type theory.

ap is a primitive in higher observational type theory, rather than being derived from path induction? of path types as in intensional Martin-Loef type theory.

Definitions

We are working in a dependent type theory.

The identity types 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$.

Identity types for pair types

Computation rules are defend for pair types:

with computation rules for ap

and computation rules for reflexivity

Identity types for function types

Computation rules are defined for function types:

with computation rules for ap

Computation rules are also defined for abstractions: TBD (involves currying)

Transport

Given a type $A$, a judgment $z:A \vdash B(z)\ \mathrm{type}$, terms $x:A$ and $y:A$, and an identity $p:(x =_A y)$, there is a function $\overrightarrow{\mathrm{tr}}_{B}^{p}:B(x) \to B(y)$ called transport.

and a dependent function indicating that transport is an equivalence:

Identity types for dependent pair types

Computation rules are defend for dependent pair types:

with computation rules for ap

…

Identity types for dependent function types

With universes

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$.

Identity types for universes

Let $A \cong_\mathcal{U} B$ be the type of bijective 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

Identity types in universes and singleton contractibility

Given a term of a universe $A:\mathcal{U}$

with terms representing singleton contractibility.

Dependent identity types in universes

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}$

See also

• homotopy type theory

References

• Mike Shulman, Towards a Third-Generation HOTT Part 1 (slides, video)