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.
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
Thus, ap is a higher dimensional explicit substitution. There are definitional equalities
for constant term .
Identity types for product types
Computation rules are defend for product 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)
Dependent identity types
Given a type , a judgment , terms and , and an identity , there is a formation rule for dependent identity types
TODO: Define introduction, elimination, and computation rules for dependent identity types.
There is a rule
and for constant families a rule
Identity types for dependent pair types
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
Thus, ap is a higher dimensional explicit substitution. There are definitional equalities
for constant term .
Identity types for universes
Let be the type of bijective correspondences between two terms of a universe and , and let be the identity type between two terms of a universe and . Then there are rules
Identity types in universes and singleton contractibility
Given a term of a universe
with terms representing singleton contractibility.
Dependent identity types in universes
Given a term of a universe , a judgment , terms and , and an identity , we have
and
We could define a dependent identity type as
There is a rule
and for constant families
See also
References
- Mike Shulman, Towards a Third-Generation HOTT Part 1 (slides, video)