试着不精确地讲讲看 ...
首先是 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