Contents
Contents
Idea
In dependent type theory, given a type , a type family , terms , , and an identification , a dependent heterogeneous identity type between two elements and is a type whose elements witness that and are “equal” over or modulo the identification .
There is also a non-dependent heterogeneous identity type where we allow the type family to be a constant type family . Non-dependent heterogeneous identity types are not the same as normal identity types because they still depend on the terms and A and the identification , as evidenced by the introduction rules for non-dependent heterogeneous identity types, which is function application to identifications rather than reflexivity.
Note on terminology
There are many different names used for this particular dependent type, as well as many different names used for the terms of this dependent type. These include the following:
name of type | name of terms |
---|
heterogeneous identity type | heterogeneous identities |
heterogeneous path type | heterogeneous paths |
heterogeneous identification type | heterogeneous identifications |
heterogeneous equality type | heterogeneous equalities |
These four names have different reasons behind the use of the name:
-
The name “heterogeneous identity type” comes from the fact that the dependent identity type is the canonical one-to-one correspondence of the transport equivalence on a type family and an identification , which is the dependent/heterogeneous version of the identity type for the identity equivalence
-
The name “heterogeneous path type” comes from either the fact that every term in the heterogeneous identity type is represented by a dependent function from the interval type, the dependent version of the path type.
Definitions
Heterogeneous identity types, like function types and pair types, come in dependent and non-dependent flavors. This is because the usual natural deduction rules for dependent heterogeneous identity types require a type and a type family ; the non-dependent version is for a constant family , which is just a type ; the dependent function in the rules for the dependent heterogeneous identity type becomes the non-dependent function in the non-dependent heterogeneous identity types.
The introduction rules for dependent and non-dependent heterogeneous identity types result in the dependent function application to identifications and non-dependent function application to identifications respectively, in the same way that the introduction rules for identity types result in reflexivity.
Finally, as with every other type in dependent type theory, the computation rules of both dependent and non-dependent heterogeneous identity types use judgmental equality, propositional equality, or typal equality.
Rules for non-dependent heterogeneous identity types
In the same way that there are rules for non-dependent function types and non-dependent pair types, there are also rules for non-dependent heterogeneous identity types, where the type family is a constant type family.
Formation rule for non-dependent heterogeneous identity types:
Introduction rule for non-dependent heterogeneous identity types:
Elimination rule for non-dependent heterogeneous identity types:
Computation rules for non-dependent heterogeneous identity types:
-
Judgmental computational rules
-
Propositional computational rules
-
Typal computational rules
Rules for dependent heterogeneous identity types
Formation rule for dependent heterogeneous identity types:
Introduction rule for dependent heterogeneous identity types:
Elimination rule for dependent heterogeneous identity types:
Computation rules for dependent heterogeneous identity types:
-
Judgmental computational rules
-
Propositional computational rules
-
Typal computational rules
As weak transport along an identity
Another way to define the dependent heterogeneous identity type is by using weak transport along the identity :
Definition in higher observational type theory
In higher observational type theory, the dependent heterogeneous 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 heterogeneous identity type then depends on an “identification in that telescope”, which is defined by mutual recursion as a telescope of dependent heterogeneous identity types. The formation rule is then
… needs to be finished
Heterogeneous identity types in universes
Given a term of a universe , a judgment , terms and , and an identity , we have
and
We could define a heterogeneous identity type as
There is a rule
and for constant families
Categorical semantics
needs to be written
See also
References