natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In dependent type theory, given a type , a type family , terms , , and an identification , a dependent identity type or a heterogeneous identity type between two elements and is a type whose elements witness that and are “equal” over or modulo the identification . There are different ways to define this precisely, depending partly on the particular type theory used.
One way to define the dependent identity type in Martin-Lof type theory is using transport along the identification :
There are also other possibilities…
In higher observational type theory, the dependent identity type is a primitive type former (although depending on the presentation, it can also be obtained using into the universe). In its general form, the type family can depend not just on a single type but on a type telescope . The resulting dependent identity type then depends on an “identification in that telescope”, which is defined by mutual recursion as a telescope of dependent identity types. The formation rule is then
… needs to be finished
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
needs to be written
Mike Shulman, Towards a Third-Generation HOTT Part 1 (slides, video)
Mike Shulman, Towards a Third-Generation HOTT Part 2 (slides, video)
Last revised on June 6, 2022 at 11:45:49. See the history of this page for a list of all contributions to it.