高次モノイド指標と論理

高次モノイド指標を定義したい。そのためには、モノイド箙とモノイダッド（monoidad）を一緒に定義する。monoidadはcomputadに似せた僕の造語。

次元	モノイド箙	モノイダッド	モノイダッド結合
-1	-	単元集合{*}	-
0	{*}上の0-アロー集合	モノイド
1	モノイド上の1-アロー集合	厳密モノイド圏	, ;
2	厳密モノイド圏上の2-アロー集合	厳密モノイド厳密2-圏	, ;, |

• (k-1)-モノイダッドと、そこに両端を持つようなk-アローの集合がk-モノイド箙を定義する。
• k-モノイド箙から、k-モノイダッドが自由生成される。
• k-モノイダッドは、(k+1)個の結合演算を持つ。k個はベースとなる(k-1)-モノイダッドから受け継ぐ。

モノイド指標はモノイド箙の特殊なものである。Σ = (|Σ|₀, |Σ|₁, |Σ|₂) が2-モノイド指標であるとは：

1. Σ^(-1*) = {*} と置く。
2. |Σ|₀は、(-1)-モノイダッドΣ^(-1*)上の0-アロー集合である。実質的には単なる集合で、その要素が0-アロー。
3. 0-モノイド箙(Σ^(-1*), |Σ|₀)で生成された0-モノイダッドをΣ^(0*)とする。
4. |Σ|₁は、0-モノイダッドΣ^(0*)上の1-アロー集合である。
5. 1-モノイド箙(Σ^(0*), |Σ|₁)で生成された1-モノイダッドをΣ^(1*)とする。
6. |Σ|₂は、1-モノイダッドΣ^(1*)上の2-アロー集合である。
7. 2-モノイド箙(Σ^(1*), |Σ|₂)で生成された2-モノイダッドをΣ^(2*)とする。

以上のようなモノイド箙／モノイダッドのタワー構成が可能なアロー集合列(|Σ|₀, |Σ|₁, |Σ|₂) が2-モノイド指標である。

n-指標を定義するには、n-モノイド箙とn-モノイダッドの定義が必要である。特に、n-モノイダッドが重要で、n-モノイダッドが定義できればn-モノイド箙は定義できる。

次元	アローの論理的な意味	構成子
0	型	タプル型
1	項	平行タプル, 項の代入（置き換え）
2	等式	平行タプルの等式, 両辺の置き換え, 推移性

まだまだこれは一部。高次圏と論理はもっと色々な形で関係しているはず。