Harper 1 2015 (40:00)
Heiting Algebra, preorder
--> soundness
<-- completeness