パラメータ

宣言にパラメータを付けることで、構造を抽象化できます。

基本

パラメータは名前の直後に [...] で書きます。

cat[C: *] = {
    x: C → C
    m: x x → x
    assoc: m x; m → x m; m
}

インスタンス化

パラメータを渡してインスタンスを作ります。

u: *
c = cat[u]

// c.x, c.m, c.assoc が使える

異なるパラメータで作ったインスタンスは異なるセルを持ちます: cat[u].x と cat[v].x は別のセルです。

複数パラメータ

Hom[X: *, Y: *] = X → Y

高次のパラメータ

0-cell だけでなく、1-cell や 2-cell もパラメータにできます。

rep2[C: *, x: C → C, f: x → x] = f; f

rep2 は 0-cell C、1-cell x、2-cell f: x → x を受け取り、f を2回合成した f; f を返します。