<p>I disagree with the premise that not having a full proof of the admissibility of substitution spelt out anywhere is a &quot;major roadblock&quot; to entering the field of type theory, at least as a user; but anyway, the reason it is not usually spelt out is that it is incredibly tedious and devoid of any mathematical content. Whether substitution is built-in or admissible is nothing more than an implementation detail.</p>
<p>As an example, assume we have <span class="math-container">$\Gamma \vdash t : X$</span>, and let us try to prove that <em>type</em> substitution is admissible, i.e.</p>
<p><span class="math-container">$$\frac{\Gamma, x : X, \Delta \vdash T\text{ type}}{\Gamma, \Delta[t/x] \vdash T[t/x]\text{ type}}$$</span></p>
<p>We proceed by structural induction on the premise. Let us only look at one case: the formation rule for dependent pair types, which has the following form here.</p>
<p><span class="math-container">$$\frac{\Gamma, x : X, \Delta \vdash A\text{ type} \quad \Gamma, x : X, \Delta, a : A \vdash B\text{ type}}{\Gamma, x : X, \Delta \vdash \sum\limits_{a : A} B\text{ type}}$$</span></p>
<p>The induction hypothesis gives us the substituted judgements</p>
<p><span class="math-container">$$\Gamma, \Delta[t/x] \vdash A[t/x]\text{ type} \qquad \Gamma, \Delta[t/x], a : A[t/x] \vdash B[t/x]\text{ type}$$</span></p>
<p>whence we conclude by the formation rule for dependent pair types</p>
<p><span class="math-container">$$\Gamma, \Delta[t/x] \vdash \sum_{a : A[t/x]} B[t/x]\text{ type}$$</span></p>
<p>and that's it. It might seem like we haven't done anything at all, but it's useful to have in mind that (and <em>how</em>) alternative presentations of type theory can fail to have admissible substitution.</p>
<p>For instance, the nLab page on <a href="https://ncatlab.org/nlab/show/dependent+sum+type#in_natural_deduction" rel="nofollow noreferrer">dependent sum types</a> gives the following introduction rule:</p>
<p><span class="math-container">$$\frac{\Gamma \vdash A\text{ type} \quad \Gamma, a : A \vdash B\text{ type}}{\Gamma, a : A, b : B \vdash (a, b) : \sum\limits_{a : A} B}$$</span></p>
<p>instead of the more conventional</p>
<p><span class="math-container">$$\frac{\Gamma \vdash A\text{ type} \quad \Gamma, a : A \vdash B\text{ type} \quad \Gamma \vdash u : A \quad \Gamma \vdash v : B[u/a]}{\Gamma \vdash (u, v) : \sum\limits_{a : A} B}$$</span></p>
<p>effectively restricting the pair constructor to variables. In this presentation, term substitution is not admissible, so we would have to add a built-in substitution rule.</p>
<p>Indeed, if we tried the same proof by induction as above, we would need to unify <span class="math-container">$\Gamma, x : X, \Delta$</span> with <span class="math-container">$\Gamma, a : A, b : B$</span>; this is fine as long as <span class="math-container">$a$</span> and <span class="math-container">$b$</span> end up in <span class="math-container">$\Delta$</span>, but if <span class="math-container">$x = a$</span> or <span class="math-container">$x = b$</span> then the proof can't go through. Intuitively, substituting <span class="math-container">$t$</span> for <span class="math-container">$a$</span> or <span class="math-container">$b$</span> in <span class="math-container">$(a, b)$</span> would now result in an ill-typed term unless <span class="math-container">$t$</span> is a variable.</p>

CC BY-SA 4.0
2024-08-27T18:03:54.490Z
This is actually fantastically helpful already, thank you for now. It has been a while, so I will have to think about this, to figure out the base cases even. I hope for a lot more trust-building tedium
Michael
CC BY-SA 4.0
2024-08-27T18:17:22.903Z
If someone wants to add more in the meantime, please go ahead. Chances are that for quite some readers these things will be seen spelt out in full for the first time (unless they have hit upon the right sources outside my knowledge.  (Please share:) ))
Michael
CC BY-SA 4.0
2024-08-27T16:49:17.760Z
2024-08-27T16:49:17.760Z
Naïm Favier
<p>The proofs you are asking for are rarely found in published papers, at least not detailed versions, because an experienced reader is able to reconstruct them easily enough. They always proceed by some sort of structural induction, usually on the derivation of the judgement. The trickiest bit, always, is how to strengthen the induction hypothesis. That is, the statement we usually want to prove cannot be proven directly by induction, instead one looks for a sligthly stronger statement that does. (For instance in Naïm's answer he strengthened the substitution rule so that also part of the context undergoes a substitution, which is necessary as soon as one considers a rule that introduces a new variable into the context in one of its premises.)</p>
<p>The place to look are PhD theses, these more commonly contain detailed proofs. My student Philipp Haselwarter produced detailed proofs for a wide class of type theories, see <a href="https://haselwarter.org/assets/pdfs/effective-metatheory-for-type-theory.pdf" rel="noreferrer">Effective Metatheory for Type Theory</a>:</p>
<ul>
<li>Admissibility of weakening is Proposition 2.2.2. Note that when Philipp says that &quot;most cases are straightforward&quot; this actually means that by the time you write them down you also see that they hold because nothing is going on, one literally just applies the induction hypothesis.</li>
<li>Admissibility of substitution is in Section 2.1.1.1. This is more complicated, it's a whole section.</li>
<li>There are other admissibility results, for example, if you can derive that <span class="math-container">$e$</span> has type <span class="math-container">$A$</span>, then you should be able to derive that <span class="math-container">$A$</span> is a type, yes? That's Theorem 2.2.18.</li>
</ul>
<p>This is not the only thesis containing such results (although I would be hard pressed to point to another one that achieves this level of generality), it's just one that I know well, as an advisor. We can go one step further and ask for <em>formalized</em> proofs of admissibility etc. I am not sure a comprehensive library is available, if someone knows of one, I'd like to know too.</p>
<p>But most importantly, Naïm has a point. <a href="https://www.gutenberg.org/files/5740/5740-pdf.pdf" rel="noreferrer">Wittgensteing wrote</a>:</p>
<blockquote>
<p><em>6.54 My propositions are elucidatory in this way: he who understands me finally recognizes them as senseless, when he has climbed out through them, on them, over them. (He must so to speak throw away the ladder, after he has climbed up on it.) He must surmount these propositions; then he sees the world rightly.</em></p>
</blockquote>
<p>To bring this down to earth and closer to the present case: yes, it is elucidatory to work out the details of the syntax of type theory and belabor the syntactic meta-theorems involving renamings and substitution – but these are just a &quot;ladder&quot; one climbs to arrive at a better, mathematically more meaningful, understanding of what type theory is and how it works. So, after reading Philipp's thesis, you should read Ambrus Kaposi's thesis, and Jon Sterling's thesis, too :-)</p>

CC BY-SA 4.0
2024-08-28T09:28:12.397Z
Philipp Haselwarter's thesis is definitely on my (unfortunately quite long) to do list- I already bounced from it once with the new commitment of learning about de Bruijn-Indices. Also, to start climbing and use type theory oneself I feel there is no substitute for seeing it at work, replicating the experience in math where you observe the newly defined entities behave and relate in the arena provided by the proofs that follow. The dearth is in reasonably selfcontained instances of this being done in type theory; admissibility seemed the first nontrivial thing to do in such a buildup
Michael
CC BY-SA 4.0
2024-08-28T09:31:23.603Z
One issue here is that there are several conceptions of what "type theory" is, and that the very syntactic presentations of it that you are asking about are sometimes seen as "suboptimal". It's like matrices vs. abstract linear algebra. Each has its own uses, but if one is going to learn linear algebra, it's a bad idea to obsess about matrices.
Andrej Bauer
CC BY-SA 4.0
2024-08-28T07:56:53.907Z
2024-08-28T08:10:24.443Z
2024-08-28T08:10:24.443Z
Andrej Bauer
<p>From the nlab article on Martin-Löf dependent type theory:</p>
<blockquote>
<p>The weakening and substitution rules are admissible rules: they do not need to be explicitly included in the type theory as they could be proven by induction on the structure of all possible derivations.</p>
</blockquote>
<p>Similarly, exercise E2.7 from the classic article &quot;Syntax and Semantics of Dependent Types&quot; by Martin Hofmann:</p>
<blockquote>
<p>Show that for any type theory containing some or all of the type formers described above the rules Weak and Subst are admissible.</p>
</blockquote>
<p>This was actually where, coming from the mathematical side, I prematurely ended my last incursion into type theory.</p>
<p>Now, in the hope to establish an entry point for anyone in a similar position: There must be a clear write-up of this somewhere, as it seems pointless to continue into type theory without having solved a point as fundamental as that. Is it just me or is this really nowhere to be found on the net?</p>
<p>I would appreciate answers demonstrating the admissibility of the aforementioned rules, or pointers to relevant sources. This is less about the results for their own sake than about seeing type theory at work supporting itself before serving as a foundation for other things.
The scarcity (?) of hands-on demonstrations in this vein seems a major roadblock to entering the field, at least trustwise. It could be removed easily by material just plainly showing how these fundamental aspects are handled at a basic level (one that should really be routine for a seasoned type theorist?). Thanks!</p>

CC BY-SA 4.0
2024-08-27T11:43:45.130Z
What are you actually asking for? A detailed proof that weakening and substitution are admissible or an explanation of what admissible means?
Max New
CC BY-SA 4.0
2024-08-27T12:18:44.190Z
Thanks for answering! The former. I suspect the reason this seems so hard to come by is that a detailed writeup would probably quite long...but also quite instructive for a beginner.
Michael
CC BY-SA 4.0
2024-08-27T12:21:59.780Z
"it seems pointless to continue into type theory without having solved a point as fundamental as that" It depends on what your goal is. For *using* type theory, you certainly do not need to worry about such details of presentation and should just assume that weakening and substitution are available.
Naïm Favier
CC BY-SA 4.0
2024-08-27T12:23:37.630Z
Quoting Jon Sterling: "Category theorists like to think of things in terms of maps, that can then be composed (which is the primitive operation). Type theorists think about things differently — in terms of generalised elements. These two viewpoints lead to different presentations of syntax — in the former you have a built in substitution construct, and in the latter, substitution is admissible. But in the end, the “complete” versions of either presentation are equivalent."
Naïm Favier
CC BY-SA 4.0
2024-08-27T12:35:58.960Z
For one to be able to think about "things" in different ways may be enlightening for the initiated, but given that type theory is advertised as a foundational system it may even be disconcerting - until you are capable of making the equivalence between different views precise. As a beginner, I think it would help if you saw type theory support itself a bit before basing other things on it.
Michael
CC BY-SA 4.0
2024-08-28T07:24:15.560Z
@NaïmFavier: Your comment read as "these are not the proofs you're looking for", i.e., it looks like you are arguing that a proof should not be shown to a person who is asking for it explicitly. What possible benefit could there be? Don't you think that at least such proofs should be available?
Andrej Bauer
CC BY-SA 4.0
2024-08-28T10:14:11.713Z
@AndrejBauer I am only [unasking](https://en.wikipedia.org/wiki/Mu_(negative)) the part of the question that assumes that one needs to see the technical details of the metatheory under discussion before one can trust type theory as a foundation. I don't think it has much to do with "type theory supporting itself", either.
Naïm Favier
CC BY-SA 4.0
2024-08-28T10:20:28.010Z
I am quite thankful for your answer. For the sake of type theory and its popularization, this should be a concrete question way below PhD level.  Not all of my formulations may have hit the mark as I reason about something I do not fully understand. But of course one has to acquire trust in type theory before using it as a foundation. Coming from math, its metatheory does not seem to be the worst bet.
Michael
CC BY-SA 4.0
2024-08-28T15:06:52.397Z
@Michael this is not directly an answer to your question (whence, a comment) but there is some flexibility in how one sets up type theory/what admissibilities one strives for. After all, at the end of the day all that matters is the terms/types which are available up to definitional equality. For an exposition of type theory which heavily de-emphasizes admissibility in favor of a more 'invariant' approach, you might find the lecture notes by Carlo Angiuli and myself interesting (https://www.danielgratzer.com/courses/type-theory-s-2024/lecture-notes.pdf).
daniel gratzer
CC BY-SA 4.0
2024-08-28T15:10:08.410Z
This does not supplant eg, Philipp's thesis that Andrej links to below. It is just an attempt to give a path to type theory which avoids these details on first encounter without compromising rigor. Details about admissible substitution and similar must be picked up if one wishes to formally justify the informal notation one uses in examples, but I thin kit is helpful to approach this in two steps rather than all at once :) (Indeed, another of Andrej's students (Anja Petković Komel) has studied such things in greater generality)
daniel gratzer
<type-theory><dependent-type>
Admissible rules in dependent type theory
Michael
# Admissible rules in dependent type theory

(Asked by: username_0 on 2024-08-27)

From the nlab article on Martin-Löf dependent type theory:

> The weakening and substitution rules are admissible rules: they do not need to be explicitly included in the type theory as they could be proven by induction on the structure of all possible derivations.

Similarly, exercise E2.7 from the classic article "Syntax and Semantics of Dependent Types" by Martin Hofmann:

> Show that for any type theory containing some or all of the type formers described above the rules Weak and Subst are admissible.

This was actually where, coming from the mathematical side, I prematurely ended my last incursion into type theory.

Now, in the hope to establish an entry point for anyone in a similar position: There must be a clear write-up of this somewhere, as it seems pointless to continue into type theory without having solved a point as fundamental as that. Is it just me or is this really nowhere to be found on the net?

I would appreciate answers demonstrating the admissibility of the aforementioned rules, or pointers to relevant sources. This is less about the results for their own sake than about seeing type theory at work supporting itself before serving as a foundation for other things.
The scarcity (?) of hands-on demonstrations in this vein seems a major roadblock to entering the field, at least trustwise. It could be removed easily by material just plainly showing how these fundamental aspects are handled at a basic level (one that should really be routine for a seasoned type theorist?). Thanks!

**Tags:** type-theory, dependent-type

> **Comments:**
> **username_1**: What are you actually asking for? A detailed proof that weakening and substitution are admissible or an explanation of what admissible means?  
> **username_0**: Thanks for answering! The former. I suspect the reason this seems so hard to come by is that a detailed writeup would probably quite long...but also quite instructive for a beginner.  
> **username_2**: "it seems pointless to continue into type theory without having solved a point as fundamental as that" It depends on what your goal is. For *using* type theory, you certainly do not need to worry about such details of presentation and should just assume that weakening and substitution are available.  
> **username_2**: Quoting Jon Sterling: "Category theorists like to think of things in terms of maps, that can then be composed (which is the primitive operation). Type theorists think about things differently — in terms of generalised elements. These two viewpoints lead to different presentations of syntax — in the former you have a built in substitution construct, and in the latter, substitution is admissible. But in the end, the “complete” versions of either presentation are equivalent."  
> **username_0**: For one to be able to think about "things" in different ways may be enlightening for the initiated, but given that type theory is advertised as a foundational system it may even be disconcerting - until you are capable of making the equivalence between different views precise. As a beginner, I think it would help if you saw type theory support itself a bit before basing other things on it.  
> **username_3**: @NaïmFavier: Your comment read as "these are not the proofs you're looking for", i.e., it looks like you are arguing that a proof should not be shown to a person who is asking for it explicitly. What possible benefit could there be? Don't you think that at least such proofs should be available?  
> **username_2**: @AndrejBauer I am only [unasking](https://en.wikipedia.org/wiki/Mu_(negative)) the part of the question that assumes that one needs to see the technical details of the metatheory under discussion before one can trust type theory as a foundation. I don't think it has much to do with "type theory supporting itself", either.  
> **username_0**: I am quite thankful for your answer. For the sake of type theory and its popularization, this should be a concrete question way below PhD level.  Not all of my formulations may have hit the mark as I reason about something I do not fully understand. But of course one has to acquire trust in type theory before using it as a foundation. Coming from math, its metatheory does not seem to be the worst bet.  
> **username_4**: @username_0 this is not directly an answer to your question (whence, a comment) but there is some flexibility in how one sets up type theory/what admissibilities one strives for. After all, at the end of the day all that matters is the terms/types which are available up to definitional equality. For an exposition of type theory which heavily de-emphasizes admissibility in favor of a more 'invariant' approach, you might find the lecture notes by Carlo Angiuli and myself interesting (https://www.danielgratzer.com/courses/type-theory-s-2024/lecture-notes.pdf).  
> **username_4**: This does not supplant eg, Philipp's thesis that Andrej links to below. It is just an attempt to give a path to type theory which avoids these details on first encounter without compromising rigor. Details about admissible substitution and similar must be picked up if one wishes to formally justify the informal notation one uses in examples, but I thin kit is helpful to approach this in two steps rather than all at once :) (Indeed, another of Andrej's students (Anja Petković Komel) has studied such things in greater generality)  

---

## 2 answers

### Answer by username_2 on 2024-08-27. Score: 2 | Accepted answer

I disagree with the premise that not having a full proof of the admissibility of substitution spelt out anywhere is a "major roadblock" to entering the field of type theory, at least as a user; but anyway, the reason it is not usually spelt out is that it is incredibly tedious and devoid of any mathematical content. Whether substitution is built-in or admissible is nothing more than an implementation detail.

As an example, assume we have $\Gamma \vdash t : X$, and let us try to prove that *type* substitution is admissible, i.e.

$$\frac{\Gamma, x : X, \Delta \vdash T\text{ type}}{\Gamma, \Delta[t/x] \vdash T[t/x]\text{ type}}$$

We proceed by structural induction on the premise. Let us only look at one case: the formation rule for dependent pair types, which has the following form here.

$$\frac{\Gamma, x : X, \Delta \vdash A\text{ type} \quad \Gamma, x : X, \Delta, a : A \vdash B\text{ type}}{\Gamma, x : X, \Delta \vdash \sum\limits\_{a : A} B\text{ type}}$$

The induction hypothesis gives us the substituted judgements

$$\Gamma, \Delta[t/x] \vdash A[t/x]\text{ type} \qquad \Gamma, \Delta[t/x], a : A[t/x] \vdash B[t/x]\text{ type}$$

whence we conclude by the formation rule for dependent pair types

$$\Gamma, \Delta[t/x] \vdash \sum\_{a : A[t/x]} B[t/x]\text{ type}$$

and that's it. It might seem like we haven't done anything at all, but it's useful to have in mind that (and *how*) alternative presentations of type theory can fail to have admissible substitution.

For instance, the nLab page on [dependent sum types](https://ncatlab.org/nlab/show/dependent+sum+type#in_natural_deduction) gives the following introduction rule:

$$\frac{\Gamma \vdash A\text{ type} \quad \Gamma, a : A \vdash B\text{ type}}{\Gamma, a : A, b : B \vdash (a, b) : \sum\limits\_{a : A} B}$$

instead of the more conventional

$$\frac{\Gamma \vdash A\text{ type} \quad \Gamma, a : A \vdash B\text{ type} \quad \Gamma \vdash u : A \quad \Gamma \vdash v : B[u/a]}{\Gamma \vdash (u, v) : \sum\limits\_{a : A} B}$$

effectively restricting the pair constructor to variables. In this presentation, term substitution is not admissible, so we would have to add a built-in substitution rule.

Indeed, if we tried the same proof by induction as above, we would need to unify $\Gamma, x : X, \Delta$ with $\Gamma, a : A, b : B$; this is fine as long as $a$ and $b$ end up in $\Delta$, but if $x = a$ or $x = b$ then the proof can't go through. Intuitively, substituting $t$ for $a$ or $b$ in $(a, b)$ would now result in an ill-typed term unless $t$ is a variable.

> **Comments:**
> **username_0**: This is actually fantastically helpful already, thank you for now. It has been a while, so I will have to think about this, to figure out the base cases even. I hope for a lot more trust-building tedium  
> **username_0**: If someone wants to add more in the meantime, please go ahead. Chances are that for quite some readers these things will be seen spelt out in full for the first time (unless they have hit upon the right sources outside my knowledge.  (Please share:) ))  

---

### Answer by username_3 on 2024-08-28. Score: 5

The proofs you are asking for are rarely found in published papers, at least not detailed versions, because an experienced reader is able to reconstruct them easily enough. They always proceed by some sort of structural induction, usually on the derivation of the judgement. The trickiest bit, always, is how to strengthen the induction hypothesis. That is, the statement we usually want to prove cannot be proven directly by induction, instead one looks for a sligthly stronger statement that does. (For instance in Naïm's answer he strengthened the substitution rule so that also part of the context undergoes a substitution, which is necessary as soon as one considers a rule that introduces a new variable into the context in one of its premises.)

The place to look are PhD theses, these more commonly contain detailed proofs. My student Philipp Haselwarter produced detailed proofs for a wide class of type theories, see [Effective Metatheory for Type Theory](https://haselwarter.org/assets/pdfs/effective-metatheory-for-type-theory.pdf):

* Admissibility of weakening is Proposition 2.2.2. Note that when Philipp says that "most cases are straightforward" this actually means that by the time you write them down you also see that they hold because nothing is going on, one literally just applies the induction hypothesis.
* Admissibility of substitution is in Section 2.1.1.1. This is more complicated, it's a whole section.
* There are other admissibility results, for example, if you can derive that $e$ has type $A$, then you should be able to derive that $A$ is a type, yes? That's Theorem 2.2.18.

This is not the only thesis containing such results (although I would be hard pressed to point to another one that achieves this level of generality), it's just one that I know well, as an advisor. We can go one step further and ask for *formalized* proofs of admissibility etc. I am not sure a comprehensive library is available, if someone knows of one, I'd like to know too.

But most importantly, Naïm has a point. [Wittgensteing wrote](https://www.gutenberg.org/files/5740/5740-pdf.pdf):

> *6.54 My propositions are elucidatory in this way: he who understands me finally recognizes them as senseless, when he has climbed out through them, on them, over them. (He must so to speak throw away the ladder, after he has climbed up on it.) He must surmount these propositions; then he sees the world rightly.*

To bring this down to earth and closer to the present case: yes, it is elucidatory to work out the details of the syntax of type theory and belabor the syntactic meta-theorems involving renamings and substitution – but these are just a "ladder" one climbs to arrive at a better, mathematically more meaningful, understanding of what type theory is and how it works. So, after reading Philipp's thesis, you should read Ambrus Kaposi's thesis, and Jon Sterling's thesis, too :-)

> **Comments:**
> **username_0**: Philipp Haselwarter's thesis is definitely on my (unfortunately quite long) to do list- I already bounced from it once with the new commitment of learning about de Bruijn-Indices. Also, to start climbing and use type theory oneself I feel there is no substitute for seeing it at work, replicating the experience in math where you observe the newly defined entities behave and relate in the arena provided by the proofs that follow. The dearth is in reasonably selfcontained instances of this being done in type theory; admissibility seemed the first nontrivial thing to do in such a buildup  
> **username_3**: One issue here is that there are several conceptions of what "type theory" is, and that the very syntactic presentations of it that you are asking about are sometimes seen as "suboptimal". It's like matrices vs. abstract linear algebra. Each has its own uses, but if one is going to learn linear algebra, it's a bad idea to obsess about matrices.  

---

