Boolean algebra v.s. Heyting algebra

【2021/10/12 ラジオ】Coqとか証明駆動開発とかに関するファクトチェックをした時のノートをlatexで書き起こしたものです. 興味がある方は参考にどうぞ.

※ブログメンテナンスの影響で, 記事番号が変わりました.