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, what is known as the variable rule (or projection rule) is the structural inference rule which, informally speaking, asserts for any dependent type the apparent tautology that “given a variable ” (as a hypothesis/antecedent) “then we have that variable ” (as a succedent).
As usual in dependent type theory, the meaning of this rule is a little less trivial than it may superficially seem by the generic type dependency involved: In the antecedent the variable may be picked out of a context telescope, and in the succedent it is implicitly weakened to depend on that full context, – which includes itself!
Accordingly, the categorical semantics as dependent types of the variable rule is given by the diagonal morphism on the object interpreting , regarded as a section of the pullback of the bundle/display map to its own total space:
Bart Jacobs, p. 121 in: Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, Elsevier (1998) [ISBN:978-0-444-50170-7, pdf]
Univalent Foundations Project, p. 422 in: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]
(in the context of homotopy type theory)
Egbert Rijke, p. 4 of: Dependent type theory [pdf], Lecture 1 in: Introduction to Homotopy Type Theory, lecture notes, CMU (2018) [pdf, pdf, webpage]
(in the context of homotopy type theory)
Last revised on August 15, 2023 at 19:39:15. See the history of this page for a list of all contributions to it.