Church Encoding!

Max 講了新內容 second-order intuitionistic propositional logic。雖然沒講很多，可是最後一張投影片馬上吸引我的目光：

稍微多看一眼，algebra 的 type 就浮出來了 ─ 又是 Church encoding！再跟 Agda 的經驗對照一下就更清楚了 :D。

--
不過我還是先不要貼到 Lambdawan 上吧，Curry-Howard correspondence 要留給 Max XD。