Isomorphisms in a Category of Propositions and Proofs

from blog Home on consequently.org, | ↗ original
Abstract: In this talk, I show how a category of propositions and classical proofs can give rise to three different hyperintensional notions of sameness of content. One of these notions is very fine-grained, going so far as to distinguish \(p\) and \(p\land p\), while identifying other distinct pairs of formulas, such as \(p\land q\) and \(q\land...