We work in intuitionistic logic, and let H be the complete Heyting
altebra of truth values.

Given a truth value r, define the "continuation monad"

cont_r : H → H
cont_r(p) := ((p ⇒ r) ⇒ r)

What, if anything, can be said about those r for which it is valid that

∀ p ∈ H . cont_r(cont_r(p) ⇒ p)

or spelled out:

∀ p ∈ H . ((((p ⇒ r) ⇒ r) ⇒ p) ⇒ r) ⇒ r ?

If r is True or False then it holds. But is that all?

By an observation of Todd Wilson from a while ago (on the categories
list), the condition is equivalent to:

∀ p, q ∈ H . (p ⇒ cont_r(q)) ⇒ cont_r (p ⇒ q)

And the reverse implication always holds.

With kind regards,

Andrej

-- 
You received this message because you are subscribed to the Google Groups "constructivenews" group.
To unsubscribe from this group and stop receiving emails from it, send an email to constructivenews+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.