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 theories with more than one layer of type, function extension types are types which behave like function types except the domain is the outer layer (or equivalent) of type rather than the normal layer of type.
In dependent type theory with a second layer of propositions , the inference rules for extension types are given as follows:
Formation rules for extension types:
Introduction rules for extension types:
Elimination rules for extension types:
Computation rules:
Uniqueness rules:
The introduction and elimination operators and implicitly carries around the underlying proposition , and these matter in the equations.
For instance, in type theories with coercive subtyping?, one may expect to coerce stronger extension types into weaker ones using the composition of and , where we use to say that the proposition implies in the second layer:
But this coercion does not simplify directly to because the underlying proposition carried by the operators are not the same.
In type theory with shapes, there are three different layers - there are the cube layer and the tope layer, which is logic over type theory where the cubes are the types and the topes are the propositions in the logic over type theory, and finally there is the type layer, which is a dependent type theory. Note that this type layer is distinct from the cube layer regarded as a type theory.
Shapes are formed in the usual set-builder notation in set theory: given a cube and a predicate tope , one could construct the shape . A cofibration in two-level type theory is an inclusion of shapes, which means shapes and with a predicate .
Formation rules for dependent extension types
Emily Riehl, Michael Shulman, A type theory for synthetic -categories arXiv:1705.07442
Jonathan Sterling, Robert Harper, Logical Relations as Types: Proof-Relevant Parametricity for Program Modules, Journal of the ACM, Volume 68, Issue 6, December 2021, Article No.: 41, pp 1-47. (doi:10.1145/3474834, arXiv:2010.08599)
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal, Controlling unfolding in type theory (arXiv:2210.05420)
Tesla Zhang?, Three non-cubical applications of extension types (arXiv:2311.05658)
For extension types in cubical type theory, see section 3.5 of:
Last revised on January 24, 2024 at 03:32:02. See the history of this page for a list of all contributions to it.