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
The interval type is an axiomatization of the cellular interval object in the context of homotopy type theory.
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
An interval type is provably contractible. Conversely, any contractible type satisfies the rules of an interval type up to propositional equality.
On the other hand, postulating an interval type with definitional computation rules for left
and right
implies function extensionality. (Shulman).
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? $\Box^1$.