Supongo que debido a su presencia en varios blogs de matemáticas e incluso de física, recientemente he empezado a aprender algo de teoría de tipos, a menudo de gente que sabe de ella y de libros que la utilizan. Quiero escribir algunos apuntes personales, concretamente sobre cómo se hacen las matemáticas en ella, pero tengo una especie de problema en que parece que hay decenas de formas de implementar la lógica en ella y no veo cuál es más canon que la otra. "Mi trabajo" hasta ahora consiste en recopilar las ideas que he encontrado.
Una norma como
$$\frac{\Gamma\vdash a:P\hspace{1cm}\Gamma\vdash f:P\to Q}{\Gamma\vdash f(a):Q}$$
es esencialmente utilizar la idea "si-entonces" tres veces a la vez. El eje vertical $\frac{foo}{bar}$ se utiliza como para la deducción natural, el $\vdash$ siendo sustituido por implicaciones $\implies$ . Otras veces parece que hacemos la teoría de la prueba con el lenguaje del objeto escrito horizontalmente. El contexto $\Gamma$ es a veces una serie de juicios tipográficos separados por comas $\Gamma=(a:A,b:B,c:C)$ pero en un sistema reforzado podemos hacer que sean un tipo en sí mismo, $\Gamma=(a,b,c):A\times B\times C$ . El torniquete denota derivabilidad y $foo\vdash bar$ son secuencias clásicas. Aquí me pregunto si realmente necesitamos dibujar en dos dimensiones y, si no es así, ¿el eje vertical es la meta-lógica de la construcción? Cuando escribimos $\frac{A\ \ \ B}{C}$ el espacio vacío entre $A$ y $B$ debe ser un "y" formalizado. Es curioso, pues, que la gente esté tan motivada para resolver la aparentemente difícil tarea de dar semántica a los sistemas formales que carecen de producto-tipo. Entonces la gente hace cálculos no tipificados en la teoría de tipos, que es lo mismo que colapsar un tipo. Las proposiciones lógicas se convierten en los términos. O usamos la correspondencia Curry Howard. Los términos son pruebas entonces, los tipos son proposiciones. Por lo tanto, la función tipo $\to$ son implicaciones $\implies$ . Cuando se trata de su semántica categórica, las cosas se salen de madre. Lo primero que leí, en un contexto de tipos dependientes, fue que las categorías son los tipos básicos y los funtores son implicaciones en la interpretación lógica. Pero entonces los objetos son los tipos y me imaginé que estos son objetos con elementos (como set) como los tipos tienen términos. Pero los términos (o las pruebas, en la interpretación lógica) sólo están contenidos en los objetos de forma solapada, porque los objetos son en su mayoría el contexto. Los morfismos son los torniquetes. Pero a veces son programas informáticos, es decir, pruebas, es decir, las implicaciones de una proposición (=tipo (=objeto)) a otra. De hecho, son clases de equivalencia de los cálculos con respecto a $\beta\eta$ -conversión. Pero si tienes 2 categorías, entonces los 2-morfismos son la conversión. La última parte me parece razonable.
En cualquier caso, ¿cuál es la forma más natural de utilizar la teoría de tipos para capturar la lógica proposicional, de modo que no tenga que reescribir mis notas por completo una vez que pase a la lógica de predicados? (=tipos dependientes (=categorías fibrosas?)). Mis motivaciones son una presentación clara de las matemáticas, no realmente teoría de la prueba y no un gran énfasis en la computación.
