generated at
Heyting代数
Heyting algebra
pseudo-Boolean algebra
ハイティング代数
擬Boole代数

summary
交わり⊣含意を備えた、つまりデカルト閉な有界束
definition
\left\lang\mathrm{ Heyting\ algebra }\colon L; ∧, ∨, 0, 1, ▷ \right\rang
二項直積として交わり
meet
\wedge
左内部hom函手として含意
implication
▷
⊃,→でもいいけど
list
余単位
^a\mathrm{eval} \colon (a▷) * (a\wedge) ⇒ C^\wedge
b.^a\mathrm{eval} \colon a\wedge (a▷b) ≦ b
modus ponensです
out-of
Heyting代数はデカルト閉圏
Ref 述語論理とインデックス付き圏と限量随伴性 - 檜山正幸のキマイラ飼育記 (はてなBlog)
into
Boole代数はHeyting代数
Ref
Heyting algebra - Wikipedia
Arend Heytingにちなむ