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:
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)
Created on March 26, 2023 at 13:10:01. See the history of this page for a list of all contributions to it.