Cartesian Closed Categories 與簡單型別論 (二)

型別理論

簡單型別（simple type theory）由一部份的 lambda term 以及函數型別構成，我們先從基本的名稱開始講起。

Cartesian Closed Categories 與簡單型別論 (一)

介紹

範疇論對理論電腦科學影響重大，其中一個應用提供各種型別理論（複數以上 type theories）的模型語意。為了解釋這兩者之間的關係，我們以 simply-typed lambda calculus $\lambda_\to$（或簡稱 simple type theory、STT）為例，討論其範疇上的詮釋。在 STT 中只討論最基本的函數型別（function type）以及變數型別，具體來看是非常簡單的函數式語言，型別系統只負責處理 function application 是否合適。

這題材預計分做兩篇，首先解釋 Cartesian closed category （簡稱 CCC）跟 simply typed lambda calculus 的定義跟基本性質，接著談論如何聯繫 CCC 與 simply typed lambda calculus 兩者。

函子範疇與 Yoneda Lemma（二）

前面一口氣介紹了函子，自然轉換，函子範疇跟 Yoneda 引理。接下來，我們要談談有關 Yoneda 引理代表了什麼意義。

物件其實就像是集合，只不過⋯⋯

首先，從 Yoneda 引理我們可以推得，考慮的函子 $latex K : C^{\mathrm{op}} \rightarrow \mathbf{Set}$ 換成 $latex hom(-, d)$ 得到：
\[
\hom(c, d)\cong[C^{\mathrm{op}}, \mathbf{Set}](hom(-, c), hom(-, d))
\]其中用 $latex [C^\mathrm{op}, \mathbf{Set}]$ 代表從 $latex C^\mathrm{op}$ 到 $latex \mathbf{Set}$ 的函子範疇，而 $latex [C^\mathrm{op}, \mathbf{Set}](hom(-, c), hom(-, d))$  代表這個函子範疇所有從 $latex hom(-, c)$ 到 $latex hom(-, d)$ 的自然轉換。

函子範疇與 Yoneda Lemma（一）

談完範疇的基礎後，可以理解到數學基礎亂七八糟放心地討論範疇論實用的部分：函子（functor）、自然轉換（natural transformation），函子範疇（functor category）以及 Yoneda 引理。