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 $A$ the apparent tautology that “given a variable $a \colon A$” (as a hypothesis/antecedent) “then we have that variable $a \colon A$” (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 $a \colon A$ itself!
Accordingly, the categorical semantics as dependent types of the variable rule is given by the diagonal morphism on the object interpreting $A$, regarded as a section of the pullback of the bundle/display map $A \to \Gamma$ 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.