Mi pregunta está relacionada con la presentación formal de la teoría tipo como se indicó en el contexto de Homotopy Tipo de Teoría. Cada formalización se basa en escribir sentencias como $$ a: A $$ donde la mayoría de los que se dice que $a$ es un objeto que puede ser construido debido a que varias de formación o plazo de formación de reglas y $A$ es un Tipo de. Pero son tipos y objetos de diferentes capas o es de todo tipo, en cierto sentido, también un término. Así que en conclusión: hay sólo una clase de base de entidades matemáticas en general?
Soy consciente de que los objetos de arriba son las pruebas. Lo que me confunde es que para el universo de la jerarquía postula que uno tiene $$ U_n : U_m $$ for $n<m$. Statements of the form $$A : B$$ with $Un$ and $B$ tipos me sugieren para creer que no hay ninguna distinción entre las pruebas y Tipos. Es este el correcto punto de vista?
Addendum, 01.01.2015: Creo que el "homotopy perspectiva" es también una pista para que - si se supone que los puntos de un espacio puede ser considerado como espacios de sí mismo en algún sentido.
Actualización, 02.01.2015
He encontrado una muy buena respuesta en CS SE. Aproximadamente hablado la respuesta es: Dependiendo del tipo de teoría que se emplea, no hay ninguna distinción (o no es). Para citar la respuesta:
Hay sistemas que ir más allá y completamente tipos de la mezcla y de la base de los términos, así que no hay ninguna distinción entre los dos. Este tipo de sistemas se dice que son de orden superior.
Así que mi pregunta se reduce a: ¿Es cierto que en el libro de Martin-Löf Tipo de Teoría, que HoTT se basa en, no hay ninguna distinción entre los términos y tipos?
