Contents
Contents
Idea
What is called higher observational type theory (HOTT) is a flavor of intensional type theory that is a higher homotopy version of observational type theory (OTT).
It may be regarded as a homotopy type theory (HoTT): the propositions of OTT correspond to the h-propositions of HoTT, the sets in OTT correspond to h-sets in HoTT, and so forth. The notion of equality on HOTT in a type universe is based on one-to-one correspondences, but is usually defined as a primitive identity type for types outside a universe. Since equality is defined type-by-type, HOTT enjoys function extensionality.
There are a few technical differences (e.g. proofs of types in a universe are definitionally equal in HOTT, whereas proofs of types in a universe are only propositionally equal in HoTT) but on the whole HoTT looks a lot like HOTT.
Overview
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 one-to-one 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
Higher observational type theory was introduced in