Heyting代数
summary.icon
definition.icon
$ \left\lang\mathrm{ Heyting\ algebra }\colon L; ∧, ∨, 0, 1, ▷ \right\rang
$ \wedge
$ ▷
$ ⊃,→ でもいいけど
list.icon
余単位
$ ^a\mathrm{eval} \colon (a▷) * (a\wedge) ⇒ C^\wedge
$ b.^a\mathrm{eval} \colon a\wedge (a▷b) ≦ b
out-of.icon
into.icon
reference.icon