試著不精確地講講看 ...
首先是 cateogry 上對照 type theory 是什麼呢？[2]
對 category 上每個 object A 考慮作 type A, 那麼
可以將 morphism f : A -> B 寫成
x : A |- f(x) : B
其中把 x 當作是 free variable of type A
在 category 下不是每個 object 都是 set, morphism 也不一定是 function,
例子是考慮 preorder 本身當作一個 category, a <= b 視作 a -> b。
（這個例子也很重要，因為 category 本身可看作 preorder 的範疇化結構[1][3]，
很多概念例如 colimit 跟 limit 可以看作是 sup 跟 inf，adjoint functor
可以看作 Galois correspondence，另一個是 homotopy category, 以
topological space 作為 object，連續函數的 homotopy classes 作為 morphisms,
被 Peter Freyd 證明不是 concrete category）
但是呢，我們還是可以把 x : A 看作是 A 的廣義元素，或是任何到 A 的 morphism。
這個概念來自於在 Set 底下，A 的元素可以看成跟 1 -> A 的morphism，其中
1 是只有一個元素的集合 {*}。
那麼 x : A |- f(x) : B 的意思，就變成說若有一個廣義元素 y : U -> A
函數的套上去之後，有 f o y : U -> A -> B = f(y) : U - B 。
那麼來到 morphism 的 composition, f : A -> B, g : B -> C 得到 A -> C呢？
寫作
x : A |- f(x) : B y : B |- g(y) : C