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 in intensional 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
Thus, ap is a higher dimensional explicit substitution. There are definitional equalities
for constant term .
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 judgment , terms and , and an identity , there is a function 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
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)