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 a dependent type theory with identity types, a subtype of a type is a type with a term , with the inclusion relation defined as the bracket type of the embedding type from to :
indicating the mere existence of an embedding. is a supertype of .
This is different from a subtype with a chosen embedding , in the same way that inhabited sets and pointed sets are different. However, equipping a type with an explicit embedding is usually more useful in mathematics without the axiom of choice.
In a dependent type theory with identity types and a hierarchy of type universes a la Tarski, given a universe a subtype of a type is a function . In a universe these are the same as subtypes equipped with an embedding as structure.
The type of all subtypes of in a universe is defined as
Last revised on January 10, 2023 at 21:41:23. See the history of this page for a list of all contributions to it.