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 type theory, the notion of subtypes is the analog of subsets in set theory.
In the presence of a type universe of propositions (alternatively denoted “”), the subtypes of a given may be simply be identified with the function type from to :
In topos-semantics, is interpreted as the subobject classifier and subtypes as subobjects.
Notice that with itself being a subtype of a type universe , the subtypes of are thus a special case of the -dependent types
namely those whose fiber type over is the proposition asserting that “ is contained in the subtype”.
This is equivalent to other definitions of subtypes, which one can make sense of also in the absence of a Prop-universe.
Notice here that in set theory, there are in fact two notions of subsets:
In material set theory, a subset of a set is a set with the property that for all , if , then , which by the definition of power set in material set theory, is the same thing as an element .
In structural set theory, a subset of a set is a set with an injection .
In dependent type theory, a similar distinction can be made between the two notions of subtypes, resulting in material subtypes and structural subtypes.
We work with a Russell type of all propositions .
The power set of a type is defined as the function type from to the Russell type of all propositions , .
The power set of a type is always a set because its codomain, the Russell type of all propositions , is a set due to the univalence axiom or propositional extensionality.
A material subtype on is an element of the power set .
The local membership relation between elements and material subtypes is defined as
A structural subtype of is a type with an embedding . is a supertype of .
material subtype | predicate | structural subtype |
---|---|---|
Given a type , the improper material subtype on is the material subtype such that for all elements , is contractible.
Given a type , there is a binary operation on the power set of called the intersection, such that for all material subtypes and , is defined as
for all , where is the disjunction of two types and is the propositional truncation of .
Given a type and a type , there is an function called the -indexed intersection, such that for all families of material subtypes , is defined as
for all , where
is the universal quantification of a type family and is the propositional truncation of .
Given a type , the empty material subtype on is the material subtype such that for all elements , is equivalent to the empty type.
Given a type , there is a binary operation on the power set of called the union, such that for all material subtypes and , is defined as
for all , where is the disjunction of two types and is the propositional truncation of .
Given a type and a type , there is an function called the -indexed union, such that for all families of material subtypes , is defined as
for all , where
is the existential quantification of a type family and is the propositional truncation of .
Given a type , there is a binary relation on the power set of called the subtype inclusion relation, such that for all material subtypes and , is defined as
Given a type , there is a binary relation on the power set of called observational equality, such that for all material subtypes and , is defined as
Axiom of extensionality: Given a type , for all subtypes and , there is an equivalence of types between and .
For all and , since is propositions, by the introduction rules of the Russell type of all propositions, . The univalence axiom for states that is equivalent to . Thus, is equivalent to . But by function extensionality, there is an equivalence of types between and ; hence there is an equivalence of types between and .
Given a type , a singleton subtype on is a material subtype such that there exists a unique such that :
Given a type , there is a binary function called the cartesian product of subtypes, defined by
for all elements , and subtypes and .
Given a type , is the improper structural subtype, with embedding given by the identity function on .
Given a type and structural subtypes and with embeddings and , the intersection of and is the dependent sum type
Given a type , the empty type is the empty structural subtype, with embedding given by any function from the empty type to .
Given a type and structural subtypes and with embeddings and , the union of and is the pushout type
where and are the first and second projection functions for the first dependent sum type and is the first projection function for the second dependent sum type for the intersection as defined above ()
Given a type and structural subtypes and with embeddings and , the cartesian product of and is simply the product . The associated embedding is defined by
for all , where and are the first and second product projection functions defined in the inference rules of the negative product type .
decidable subtype?
Martin Hofmann, Benjamin Pierce, Positive Subtyping, Information and Computation 126 1 (1996) 11-33 [doi:10.1006/inco.1996.0031]
(including early discussion of lenses in computer science)
Univalent Foundations Project, p. 111 of: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]
Egbert Rijke, §12.2 in: Introduction to Homotopy Type Theory (2019) [web, pdf, GitHub]
Martín Escardó, The subtype classifier and other classifiers, in: Introduction to Univalent Foundations of Mathematics with Agda [arXiv:1911.00580, webpage]
Felix Cherubini, Thierry Coquand, Matthias Hutzler, A Foundation for Synthetic Algebraic Geometry (2023) [arXiv:2307.00073]
(in the context of synthetic algebraic geometry)
In Agda:
Ettore Aldrovandi, Subtypes, §4 in: Propositions, Sets and Logic–Ⅱ [web]
In Lean:
Last revised on November 24, 2023 at 05:01:05. See the history of this page for a list of all contributions to it.