Redirected from "interval types".
Contents
Contents
Idea
The interval type is an axiomatization of the cellular interval object in the context of homotopy type theory.
Definition
As a higher inductive type, the interval is given by
Inductive Interval : Type
| left : Interval
| right : Interval
| segment : Id Interval left right
This says that the type is inductive constructed from two terms in the interval, whose interpretation is as the endpoints of the interval, together with a term in the identity type of paths between these two terms, which interprets as the 1-cell of the interval
Induction principle
The induction principle for the interval says that for any equipped with point and and a dependent identification , there is such that:
and for every such that
there is an identification .
As a special case, its recursion principle says that given any type with points and and an identification , there is with
Syntax
The interval type is defined by the following rules:
Formation rules for the interval type:
Introduction rules for the interval type:
Elimination rules for the interval type:
Computation rules for the interval type:
- judgmental computational rules
- propositional computation rules
Uniqueness rules for the interval type:
The elimination rules and the propositional computation and uniqueness rules for the interval type state that the interval type satisfy the dependent universal property of the interval type. If the dependent type theory also has dependent sum types and product types, allowing one to define the uniqueness quantifier, the dependent universal property of the interval type could be simplified to the following rule:
In type theories with a separate type judgment where not all types are elements of universes, one has to additionally add the following elimination and computation rules:
Elimination rules:
Computation rules:
- judgmental computation rules
- typal computation rules
Using a function from the boolean domain
The interval type is defined by the following rules:
Formation rules for the interval type:
Introduction rules for the interval type:
Elimination rules for the interval type:
Computation rules for the interval type:
Uniqueness rules for the interval type:
…
Properties
-
An interval type is provably contractible. Conversely, any contractible type satisfies the rules of an interval type up to typal equality.
-
An interval type is a suspension type of the unit type, and the suspension of an interval type is a 2-globe type.
-
An interval type is a cone type of the unit type.
-
An interval type is a cubical type? .
Induction principle without heterogeneous identifications
There is a version of the induction principle which uses a type and a function instead of a type family indexed by . It has the benefit of not requiring that one has first defined heterogeneous identification types, whether as an inductive family of types or by using transport.
The induction principle of the interval type says that given a type and a function , as well as
-
elements and
-
identifications , and such that , , , and form a square
- an identification saying that the square commutes
one can construct
- a homotopy witnessing that is a section of :
such that
The last condition needs some explanation. Since is a section of , the composite is the identity function on the interval type, up to identification. Now, given any identity function on the interval type with homotopy
we have the following square for all , , and :
This square commutes via the J rule: it suffices to construct an element of
But reduces down to via
and similarly reduces down to , so just take reflexivity of .
So the naturality square is inductively defined by
When , , , , and , this results in the identification
which is of the same type as due to the judgmental equalities in the other computation rules.
One gets back the usual induction principle of the interval type when and the first projection function of the dependent sum type, and one gets back the recursion principle of the interval type when and the first projection function of the product type.
Path types and identity types
In general, functions from to a type can be thought of as the paths in in Martin-Löf type theory, and the function type can be thought of as the path types of , similar to how in topology paths in a (topological) space are (continuous) functions from the unit interval, and how in cubical type theory the cubical paths are a kind of function type out of the pre-defined interval pre-type.
The recursion principle of the interval type allows for paths to be defined from a given identification, and function application to identifications allows for identifications to be defined from a given path:
Theorem
Every identification between two terms and of a type has an associated path , recursively defined by
where
is the function application to identities,
is concatenation of identities (i.e. transitivity), and
is the inverse of identities (i.e. symmetry).
Theorem
Given a path and terms and with identities and , there is an identity
The path version of reflexivity of an element is represented by the constant function . By definition of function application to identifications, one has
for all and .
This allows us to posit versions of path induction using functions from the interval type, which states that:
Theorem
Given a type , a type family indexed by , and a family of elements , one could construct a dependent function such that .
The alternate induction principle of the path type, which uses functions into the path type rather than families indexed by the path type, is given by:
Theorem
Given any type and function into the path type in , and given a function and a homotopy
which states that the composite of and is the canonical function which takes elements of to constant paths into , one can construct a function and a homotopy witnessing that is a section of :
such that for all , and .
elimination rules for path induction:
computation rules for path induction:
Theorem
Suppose that path induction for function types out of the interval type is true.
Then the J-rule is true: given a type and given a type family indexed by , , and , and a dependent function , one can construct a dependent function
such that for all ,
Proof
By path induction on the type family indexed by , we can construct a dependent function
such that for all ,
since by definition of constant function and reflexivity, one has
We define
since by interval recursion one has a path such that
Relation to dependent identity types
Given a type , a dependent type , terms and , identity , terms and , and dependent identity , let us inductively define the family of elements by
where is transport, is the function application to identities, is concatenation of identities (i.e. transitivity), and is the inverse of identities (i.e. symmetry).
Let and be types, and let be an equivalence between and . Then there is a type family defined by , , and .
Relation to function extensionality
Postulating an interval type with judgmental computation rules for the point constructors of the interval type implies function extensionality. (Shulman).
The proof assumes a typal uniqueness rule for function types. First it constructs a function from a dependent function , inductively defined by
Then it uses the properties of function types, product types, currying, uncurrying, and the symmetry of products , to construct a function , inductively defined by
If the interval type has judgmental computation rules for the point constructors, then and for all , which implies that and for all , and subsequently that and . This means that there are identities and , and an identity
thus proving function extensionality.
An interval type with only typal computation rules for the point constructors does not imply function extensionality. This is because the proof with the judgmental computation rules uses the fact that and for all implies that and . However, if the computation rules are typal, then the equivalent statement is that having identities and for all implies that there are identities and , which is precisely function extensionality, and so cannot be used to prove function extensionality.
Relation to propositional truncations
An interval type is the propositional truncation of the boolean domain . We use the definition of an interval type using a function from . Since the interval type has identities
- ,
- ,
- ,
- ,
there is a dependent function
inductively defined by the identities
If dependent product types have judgmental computation rules, then the above becomes
Both show that the interval type is the propositional truncation of the boolean domain.
The converse is true as well: the propositional truncation of the boolean domain is the interval type. Recall that is inductively generated by a function and a dependent function
which makes into an h-proposition. By definition of an h-proposition, for each element and , the identity type is a contractible type. In particular, by induction on , this means that there are identities
and for every identity , there are identities
Thus, one could simply take and as the term constructors and as the identity constructor of the interval type.
If both propositional truncations and the boolean domain have judgmental computation rules, the the interval type also has judgmental computation rules. See (this file)
References
Proofs of function extensionality using an interval type with judgmental computation rules for point constructors could be found here
- Carlo Angiuli, Univalence implies function extensionality (blog, pdf)