Homotopy Type Theory higher observational type theory > history (Rev #2)

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.

Definitions

We are working in a dependent type theory with universes.

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 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 for product types

Computation rules are defend for product types:

with computation rules for ap

and computation rules for reflexivity

Identity types and singleton contractibility

Singleton contractibility:

Dependent identity types

Given $x:A \vdash B:\mathcal{U}$ we could define a dependent identity type as

There are also rules

and for constant families

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)

Identity types for dependent function types

Identity types for dependent pair types

Presets

Just as in set theory a preset is a set without an equality relation, a preset in higher observational type theory is a type without a recursively defined identity type.

See also

• homotopy type theory

References

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