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 set theory, there are 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.
Let denote the type of all propositions and its type reflector type family. Let be a type.
The power set of a type is defined as the function type from to the type of all propositions , .
The power set of a type is always a set because its codomain, the 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 .
In the inference rules for the type of all propositions, one has an operation which takes a proposition and turns it into an element of the type of all propositions .
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 .
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 .
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 , 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 ()
Last revised on May 25, 2023 at 14:55:25. See the history of this page for a list of all contributions to it.