Showing changes from revision #15 to #16:
Added | Removed | Changed
Contents
< higher observational type theory
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.
Telescopes
Telescopes represent lists of terms in the context.
Rules for the empty telescope
Rules for telescopes given a telescope and a type
Rules for the empty context in a telescope
Rules for …
…
Identity telescopes
…
…
Dependent identity types
The identity types in higher observational type theory is defined as
Computation rules are defend for pair types:
Computation rules are defined for function types:
Computation rules are defend for dependent pair types:
Computation rules are defend for dependent pair types:
Dependent Ap
…
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