You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Jencel Panic (Aug 15 2024 at 07:10):Are there any significant differences between the idea of Propositions as types and of computational trilogy AKA trinitarianism, except for the fact that the latter also includes categories and spaces?
Judging from the table on the nlab page of computational trilogy, the answer is no, the first header goes:
Also, there are other related terms such as Curry-Howard correspondence (there is also Curry-Howard-Lambek) and the BHK interpretation.
Jencel Panic (Aug 15 2024 at 07:13):Ah, now I see that the above nlab has an aswer to my question:
computational trinitarianism = propositions as types + programs as proofs + relation type theory/category theory
Jencel Panic (Aug 15 2024 at 07:14):Still, it's interesting to see people's perspective.
David Corfield (Aug 15 2024 at 08:51):Check out the variant Propositions as some types. This is still part of the trinitarian picture.