Simple Fact

Allegories 在 arrows 上面除了 categories 原有的 source、target、composition 三個操作，又定義兩個型別相同的 arrows 之間的 inclusion relation 以及 meet operation。用以定義 meet 的性質（universal property）是

從 "and" connective 的 commutativity、idempotence、…等性質（搭配下面提到的 "indirect proof"）可得到 meet 是 commutative、idempotent、…等等。我想證明的一個簡單事實是

這個事實顯然到 AoP 沒寫出來就直接使用。可是這式子的包含順序剛好和 universal property 相反，看來不是直接從 universal property 弄得到。書的前面一點點有提到如何使用 "indirect proof" 證明兩個 arrows 相同，而不直接用 antisymmetry of inclusion（"ping-pong" argument）：

我現在需要的是一個比較弱的版本：

如果這個性質可以用，我要證明的東西就很簡單了，只是一個單純的 and-elimination。但我們現在是在玩代數，不是基本假設或從基本假設導出的東西是不能用的。看起來我好像卡住了，走投無路只好寄信給 scm 老師求救 XD。晚一點再看看，原來 inclusion 已經說是 partial order！那麼那個比較弱的 equivalence 就好證啦：從左邊到右邊是 transitivity，從右邊到左邊是 reflexivity。要強一點的 R = S 就再加個 antisymmetry。一切問題的肇因都是因為我沒看清楚 inclusion 是 partial order 的關係，一看到 partial order 就全部解掉了。只好趕快再寫一封信給 scm 老師取消提問 XD。

--
寓意：書要看仔細 XD。

---

scm 老師還是寫信來了，因為其實真的很簡單：取 X = R meet S，那麼 meet 的 universal property 左邊根據 reflexivity of inclusion 是對的，右邊就是我要的結果。

--
這種事情好像發生很多次了，例如這次 XD。