\(i\)を階数、\(A,B,C:\mathcal {U}(i)\)を型、\(f:A\to B\)と\(g:B\to C\)を関数とする。合成関数(composed function)\(g\circ f:A\to C\)を\((g\circ f)(x)\equiv g(f(x))\)と定義する。