OTT

今天和 Weijin 到花蓮拜訪高中同學。因為三人只有一輛機車，所以長距離移動時必須分兩趟，我在等的時候就拿預先準備好的 HOAS paper 和 OTT paper 出來看。HOAS paper 看來並不特別難，只超出我目前的 category theory 知識一點點，最關鍵的 machinery 似乎就是 Yoneda lemma，所以先搞懂 Yoneda lemma 再繼續嘍。至於 OTT paper 還真如 scm 老師所說，是看得懂的耶！而且前幾天用 W-types 模映 lists，試圖把 W-elimination 特化成完整的 dependent foldr 時遇到了問題 ─ 沒辦法證明 [] 只可能有一種實作（intensionally）。讀了 OTT paper 才發現這正是其中一個懸疑點，paper 裡面也沒辦法從 W-elimination 特化出 induction on natural numbers，正是同一個問題，而稍後 OTT 將提供解答！這下我對 OTT 更有興趣了 XD。

--
我會試著在我的系統裡面為（我認知的）慈濟大學的精神找個位置的…