不小心

因為臨時和 Agda 玩了一下，不小心就漏了一天沒寫，不過其實也沒什麼好寫 XD。真的要寫的話也只有發一頓牢騷：allegories 好難！又是方桌的（tabular），又是單元的（unitary），奇怪的模化律（modular law）超複雜，左除和右除（left-division/right-division）也很難懂。難怪 Richard Bird 要回去做 functional derivation 啦 XD。

--
卡在第四章動彈不得 ─ AoP 一共十章，其中一到六章只是 "basic theory" XD。