Una propiedad de monotonicidad de la teoría de tipos de Martin-Löf

Question

Creo (y por favor corríjanme si me equivoco) que la mayoría de las presentaciones de la Teoría de Tipos de Martin-Löf satisfacen la siguiente propiedad, o algo muy cercano a ella.

Dado un árbol de derivación con conclusión $\Gamma \vdash a : A$ a árbol de derivación con conclusión $\Delta, x : A \vdash t : T$ , encontrar un árbol de derivación con conclusión $\Delta, \Gamma \vdash t[x \leftarrow a] : T[x \leftarrow a]$ .

Además, supongo que se puede demostrar con un humilde argumento de inducción. Desgraciadamente, eso parece una prueba larguísima que preferiría no hacer yo mismo, lo que me lleva a mis preguntas.

1. ¿Tiene esta propiedad un nombre oficial?
2. ¿Se cumple tal como he dicho (o tal vez con algunas condiciones adicionales)?
3. ¿Cuál es una buena referencia que afirme y demuestre esta propiedad?

Answer 1

1. Sí, esta propiedad suele denominarse "lema de sustitución" (también en sistemas de tipos distintos de la teoría de tipos de Martin-Löf).

2. Sí, excepto que la conclusión debe ser de la forma $\Gamma, \Delta [x \leftarrow a] \vdash t[x \leftarrow a] : T[x \leftarrow a]$ (la sustitución se filtra también al contexto). En realidad, la afirmación exacta depende de la definición precisa de la teoría de tipos de Martin-Löf.

3. Una buena referencia es el doctorado de Gardner tesis en particular el lema de sustitución de la página 16 (lema 2.1.10). En realidad, este lema no se enuncia para la teoría de tipos de Matin-Löf, sino para un sistema de tipos puros más sencillo en la misma línea (no hay ninguna diferencia significativa, al menos para el enunciado y la demostración de dicho lema).