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 theory, a dependent function is like a function but where we allow the codomain of the to depend on elements of the domain.
In dependent type theory, a type $A$ is a contractible type if it comes with an element $a:A$ and a family of identities $x:A \vdash c(x):a =_A x$ indicating that $a$ is a center of contraction. A dependent function from type $A$ to the type family $x:A \vdash B(x)$ could be defined as
The first three definitions are interdefinable with each other in dependent type theories with identity types and dependent sum types, and the fourth definition is interdefinable with the other three via the rules for dependent function types
dependent tuple, dependent sequence, dependent function
Last revised on January 12, 2023 at 06:32:51. See the history of this page for a list of all contributions to it.