La categoría que faltaba en la lógica (constructiva)

Question

Es bien sabido que los tipos en un lenguaje de programación dado forman una categoría, basada en Set, con sus funciones como morfismos.

También es bien sabido que cualquier programa es básicamente una prueba en lógica constructiva: el resultado se denomina correspondencia Curry-Howard y se utiliza en programas de comprobación de teoremas como Coq y Agda.

¿No constituye entonces la lógica constructiva una categoría por derecho propio? ¿Los objetos son aserciones lógicas, los morfismos son implicaciones y Verdadero y Falso son, como en Coq, el objeto inicial y el objeto terminal? Y si es así, ¿por qué no está definida esa categoría en ninguna parte?

Lo pregunto porque me parece raro que mucha gente hable de la conexión entre la lógica y la teoría de categorías, pero que yo sepa nadie la formaliza.

Answer 1

Parece que estás buscando el "modelo a plazo" o categoría sintáctica de una teoría de tipos. Se define en Bocetos de un elefante: Compendio de teoría de topos D1.4.

En general, esto distinguirá entre las pruebas; de lo contrario, sólo se obtiene un poset llamado álgebra de Lindenbaum-Tarski. Se trata de un álgebra de Heyting si su teoría obedece a los axiomas de la lógica intuicionista.