# Heyting algebra in simply typed lambda calculus

The Emil Jeřábek's comment in Can boolean algebra be expressed in simply typed lambda caclulus? give rise to the following question:

Can some non-trivial Heyting algebra be expressed in simply typed lambda calculus?

Consider, for example, the simplest Heyting algebra that is not already a Boolean algebra, that's the totally ordered set $\{0, \frac 12, 1\}$ described here.

More generally, I ask if is possible to build a type $H$ togheter with two terms $\mathrm{true},\mathrm{false}:H$ and functions $\wedge, \vee, \Rightarrow, \neg:H\to H$ satisfying the inference usual rules for intuitionistic logic, exception for the excluded middle.

• The previous question was about representation of the specific 2-element Boolean algebra, not the variety of Boolean algebras. So: which Heyting algebra? And what are the conditions that you want the expression to satisfy? – Emil Jeřábek supports Monica Apr 27 '16 at 10:48
• After the edit: yes, the 2-element Boplean algebra, which is also a Heyting algebra. – Emil Jeřábek supports Monica Apr 27 '16 at 13:35