An equational way to prove associativity of least upper bounds

Traditionally, to prove the associativity of the least upper bounds, i.e. we need few lines to prove the inequality from the left hand side and conversely. However, by turning the definition of finit join to the adjunction form, we have a more compact and algebraic-like way to do it.

Well-definedness

脫稿好久，而且還不是本來預定要寫的東西，只是最近即便是這簡單的例子，也發現把事情講清楚的重要性。

給定一個等價類 ，事實上這個 relation 的性質跟等式一樣，因此作 quotient set 的意義實際上是替代原本的等式，換成這個 relation，所以就有 若且唯若 這件事情。實際上構造也很簡單，就是定義 .

接下來的問題是，我們要怎麼在 quotient set 上定義函數呢？事實上就跟一般函數的定義方式一樣，取 指定對應的對象就好了。但是既然 quotient set 可以寫成 ，我們是不是能根據 來定義呢？可以的，但是數學教科書都會寫，必須是良好定義的，也就是若 ，那麼 ，白話來講，原本被看作一樣的東西，對應過去也是要一樣的。

那為甚麼在一般的集合上定義不需要呢？若是根據 的 表示來定義，事實上我們定義的是一個從原本集合 為定義域的函數，而不是 這個新的集合，而為了要說這個函數可以沿用到 上，我們自然必須檢查是否還是個集合。

若是用範疇論的語言來解釋的話，考慮 其中箭頭代表兩個投影函數 分別對應成 和 的投影而已，那麼 quotient set 事實上是該 diagram 的 coequalizer ，那麼定義   用表示來定義的函數，若是對所有 都滿足 的話，那麼自然從 coequalizer 會有一個唯一的映射到 ，而那就是 quotient set 上的函數。

用箭頭語言講的好處是，我們清楚知道是哪些物件在作用，每個步驟都是 diagram 裡的一部分，但是我們又不限定多餘的東西：誰說 quotient set 一定要是 呢？因為與 quotient set 相等的集合有很多，只要有一對一且映成的函數連結起來就夠了。

A technical difficulity of modelling transition systems

To be precise, the title should be read as “a technical … using well-founded set theory such as ZFC axioms”. One of the major achievement  in mathematics is to find a standard or canonical form of a formula, a system or any mathematical entity.

Yoneda argument – Application

A simple application of Yoneda argument is to prove that in Cartesian closed category.

Lemma. In Cartesian closed category, where is terminal.

Proof. for all objects . Hene .

It’s also quite easy to see that since .  Hence . It’s just like that we prvoe the equality in the Heyting algebra!

Yoneda argument

I don’t want to repeat the Yoneda lemma, but one of the important corollary should be emphasized. Roughly speaking, given any object in the category , is determined by its morphisms up to isomorphism. That is, the natural isomorphism between hom-sets corresponds to the isomorphism between objects, i.e. . How do we prove it? Well, let’s see a simpler analogy in partial orders.

Lemma. if and only if .
Proof. If , then and which imply and . Hence . The converse is quite trivial.

First, we can prove it by brute force method.

Lemma. if and only if .
Proof. Consider the following diagrams,

by replacing with , we will see that and we will have the other isomorphism by replacing with and reversing the arrows.

However, the diagram above is exactly used in Yoneda lemma, and of course we can use Yoneda lemma to prove it.

First recall that Yoneda lemma states that where is a Set-valued functor and is an object in a locally small category . Let be the hom-set functor . It gives the isomorphism between . Hence, it indeed tells you that is fully faithful. Therefore, we have the second proof.

Proof2. Given that is fully faithful, thus the natural isomorphisms actually correspond to the isomorphism and vice verse. That’s it!

為甚麼是 Functional Programming？– call by need

call-by-need 是另外一點值得強調的部份。程式基本上只能作有限的計算，而回傳資料也總是有限的，所以不大可能在程式語言中，有個值完整代表無理數，或者是無窮的資料，只是有限的估計而已。是這樣嗎？

為甚麼是 Functional Programming？

正在 Midlands Graduate School 2010 上課，想到一些東西寫點輕鬆的。

我第一個學的語言，嚴格講起來應該是小學二年級的 GW-Basic，姊姊正在念高職時，借她的課本來看，稍微玩一下。不過並沒有認真學，到最後電腦只是拿來玩電動而已。在那之後過很久，高中電子辭典有些內建 gw-basic，那時候還稍微記得上課會寫些東西打發時間，但就只是玩玩而已。

恭喜 Josh ~

恭喜 Josh 獲得 Clarendon Scholarship – University College MPLS Scholarship！（當然同時也獲得入學許可了），原文在此。

這代表我以後去 Oxford 可以住 University College 了嗎？XD

a^1 \cong a

I’d like to show that . First, I tried to prove it by algebraic way, i.e. writing down the diagram and looking for the suitable equality. However, it goes wildly messy eventually, but I finally proved it by its universal properties as follows.

Let be a isomorphism between and , and be any morphism from to . Since we have , it doesn’t matter whether we write or . According to the product diagram, we have the unique making the diagram commute (why we don’t care about ?). However, it also means has the same universal property as .

Another example is .

It tells me that to prove categorical idea we had better to prove it by its universal properties. It’s quite different what we do in set theory. We usually prove things are the same if they have the same elements. It seldom works very well in category theory, and I think it is the wrong way to think about it.

a x 1 \cong a

A quick note: where is the terminal object.

Consider the following diagram,

we have already, and we attempt to find whether is equal to . However, where

.

Since is a terminal object, the morphism is unique. So, and therefore which is the identity of .

To see that is the identity, we just draw the following diagram,

where also makes the diagram commute. Since is unique, it must be as same as .

Also, to see we just draw the following diagram,

where by the similar argument.