CatGloss

T $. It is worth pausing here to reflect on what has been accomplished. We now know that the truth arrows in$ mathbf{Set}^{p} $are precisely those natural transformations whose components interpret the corresponding connectives on the Heyting algebras in$ mathbf{P} $. But remember that the truth arrows were defined long before intuitionistic logic and HA’s were mentioned. They arose from a categorial description of the classical truth functions in$ mathbf{Set} $ . Subsequently

This site is open source. Improve this page.