Componentwise

當我們有兩個 groups G 和 G'，我們可以取它們的 direct product G × G'，其上的操作是對每個分量個別運算。可以很直覺地想像，這樣的定義確實造就一個 group。

另一方面，任意的函數集 G^A = (A → G)（其中 G 是一個 group）也可以擴充成一個 group ─ 只要定義 (f · g) x = f(x) · g(x) 即可。Martin-Löf 這時會跳出來說：A → G 其實是一堆 G 的 cartesian product，以 A 的元素當作 index。例如 ℕ → G 就相當於 G × G × G × ⋯，一個函數 f : ℕ → G 就相當於一個 countably infinite tuple (f(0), f(1), f(2), ...)。如此詮釋下，(f · g) x = f(x) · g(x) 的意義就很明顯：「f · g 的 x 分量」是「f 的 x 分量」乘上「g 的 x 分量」，其實就是推廣的 direct product。

--
和 accessibility 一樣，這裡丟掉 higher-order 的想法會更直覺簡單 XD。