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