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
indicating the mere existence of a 1-monic function or embedding, where is the propositional truncation of . is a supertype of .
This is different from a subtype with a chosen 1-monic function, a type with a term , with the type of 1-monic functions defined as
in the same way that inhabited sets and pointed sets are different. However, equipping a type with an explicit 1-monic function 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 a 1-monic function as structure.
The type of all subtypes of in a universe is defined as
Last revised on June 17, 2022 at 17:42:33. See the history of this page for a list of all contributions to it.