ホモトピー型理論

[004V] 構造同一原理

[0022]で構造同一原理の例をいくつか見たが、群や環などの数学的に興味深い構造については後回しにしていた。これは、型理論において「\(a_{1}=a_{2}\)」は単なる型なので公理を適切に記述するためには[003Z]の意味での命題の概念が必要だからである。例えば、ある二項演算\(\times \)の結合律を素直に\((a_{1}\times a_{2})\times a_{3}=a_{1}\times (a_{2}\times a_{3})\)と書くと、これは公理というよりも構造の一部になってしまう。結合律を適切に公理として扱うためには、同一視型が命題であることを要請すればよい。

[004W] 例

\(i\)を階数とする。型\(\mathord {\textnormal {\textsf {GroupStr}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を次のレコード型と定義する。

  • -\(\mathord {\textnormal {\textsf {Carrier}}}:\mathcal {U}(i)\)
  • -\(\mathord {\textnormal {\textsf {unit}}}:\mathord {\textnormal {\textsf {Carrier}}}\)
  • -\(\mathord {\textnormal {\textsf {mul}}}:\mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\)
  • -\(\mathord {\textnormal {\textsf {inv}}}:\mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\)
要素\(G:\mathord {\textnormal {\textsf {GroupStr}}}(i)\)に対して、型\(\mathord {\textnormal {\textsf {GroupAxiom}}}(G):\mathcal {U}(i)\)を次のレコード型と定義する。
  • -\(\_:\mathord {\textnormal {\textsf {IsSet}}}(G.\mathord {\textnormal {\textsf {Carrier}}})\)
  • -\(\_:\prod _{x:G.\mathord {\textnormal {\textsf {Carrier}}}}G.(\mathord {\textnormal {\textsf {mul}}}(G.\mathord {\textnormal {\textsf {unit}}},x))=x\)
  • -\(\_:\prod _{x:G.\mathord {\textnormal {\textsf {Carrier}}}}G.\mathord {\textnormal {\textsf {mul}}}(x,G.\mathord {\textnormal {\textsf {unit}}})=x\)
  • -\(\_:\prod _{x_{1},x_{2},x_{3}:G.\mathord {\textnormal {\textsf {Carrier}}}}G.\mathord {\textnormal {\textsf {mul}}}(G.\mathord {\textnormal {\textsf {mul}}}(x_{1},x_{2}),x_{3})=G.\mathord {\textnormal {\textsf {mul}}}(x_{1},G.\mathord {\textnormal {\textsf {mul}}}(x_{3},x_{3}))\)
  • -\(\_:\prod _{x:G.\mathord {\textnormal {\textsf {Carrier}}}}G.\mathord {\textnormal {\textsf {mul}}}(G.\mathord {\textnormal {\textsf {inv}}}(x),x)=G.\mathord {\textnormal {\textsf {unit}}}\)
  • -\(\_:\prod _{x:G.\mathord {\textnormal {\textsf {Carrier}}}}G.\mathord {\textnormal {\textsf {mul}}}(x,G.\mathord {\textnormal {\textsf {inv}}}(x))=G.\mathord {\textnormal {\textsf {unit}}}\)
型\(\mathord {\textnormal {\textsf {Group}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を\(\sum _{X:\mathord {\textnormal {\textsf {GroupStr}}}(i)}\mathord {\textnormal {\textsf {GroupAxiom}}}(X)\)と定義する。\(\mathord {\textnormal {\textsf {Group}}}(i)\)の要素を(階数\(i\)の)群(group)と呼ぶ。群\(A,B:\mathord {\textnormal {\textsf {Group}}}(i)\)に対して、同一視型\(A=B\)を計算しよう。[004X]と[0048]より\(\mathord {\textnormal {\textsf {GroupAxiom}}}(X)\)は命題であることが分かるので、[0049]より同値\((A=B)\simeq (\mathord {\textnormal {\textsf {proj}}}_{1}(A)=\mathord {\textnormal {\textsf {proj}}}_{1}(B))\)を得る。[0028]と同様に、\(\mathord {\textnormal {\textsf {proj}}}_{1}(A)=\mathord {\textnormal {\textsf {proj}}}_{1}(B)\)は次のレコード型と同値であることが分かる。
  • -\(f:(\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {Carrier}}}\simeq (\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {Carrier}}}\)
  • -\(\_:f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {unit}}})=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {unit}}}\)
  • -\(\_:\prod _{x_{1},x_{2}}f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {mul}}}(x_{1},x_{2}))=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {mul}}}(f(x_{1}),f(x_{2}))\)
  • -\(\_:\prod _{x}f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {inv}}}(x))=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {inv}}}(f(x))\)
この型の要素はいわゆる群同型(group isomorphism)である。\(\mathord {\textnormal {\textsf {GroupAxiom}}}(G)\)の定義で\(\mathord {\textnormal {\textsf {IsSet}}}(G.\mathord {\textnormal {\textsf {Carrier}}})\)を落とすと、\(\mathord {\textnormal {\textsf {Group}}}(i)\)の同一視の特徴付けは演算だけでなく残りの構造も保つ同値というものになってしまう。

ちなみに、群の間の乗法を保つ関数は単位元と逆元も保つことを示せるので、群同型の型は次のレコード型とも同値である。

  • -\(f:(\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {Carrier}}}\simeq (\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {Carrier}}}\)
  • -\(\_:\prod _{x_{1},x_{2}}f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {mul}}}(x_{1},x_{2}))=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {mul}}}(f(x_{1}),f(x_{2}))\)

[004Y] 例

\(i\)を階数とする。型\(\mathord {\textnormal {\textsf {RingStr}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を次のレコード型と定義する。

  • -\(\mathord {\textnormal {\textsf {Carrier}}}:\mathcal {U}(i)\)
  • -\(\mathord {\textnormal {\textsf {zero}}}:\mathord {\textnormal {\textsf {Carrier}}}\)
  • -\(\mathord {\textnormal {\textsf {plus}}}:\mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\)
  • -\(\mathord {\textnormal {\textsf {neg}}}:\mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\)
  • -\(\mathord {\textnormal {\textsf {one}}}:\mathord {\textnormal {\textsf {Carrier}}}\)
  • -\(\mathord {\textnormal {\textsf {mul}}}:\mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\)
要素\(R:\mathord {\textnormal {\textsf {RingStr}}}(i)\)に対して、型\(\mathord {\textnormal {\textsf {RingAxiom}}}(R):\mathcal {U}(i)\)を次のレコード型と定義する。
  • -\(\_:\mathord {\textnormal {\textsf {IsSet}}}(R.\mathord {\textnormal {\textsf {Carrier}}})\)
  • -\(\_:\prod _{x:R.\mathord {\textnormal {\textsf {Carrier}}}}R.\mathord {\textnormal {\textsf {plus}}}(R.\mathord {\textnormal {\textsf {zero}}},x)=x\)
  • -\(\_:\prod _{x_{1},x_{2},x_{3}:R.\mathord {\textnormal {\textsf {Carrier}}}}R.\mathord {\textnormal {\textsf {plus}}}(R.\mathord {\textnormal {\textsf {plus}}}(x_{1},x_{2}),x_{3})=R.\mathord {\textnormal {\textsf {plus}}}(x_{1},R.\mathord {\textnormal {\textsf {plus}}}(x_{2},x_{3}))\)
  • -\(\_:\prod _{x_{1},x_{2}:R.\mathord {\textnormal {\textsf {Carrier}}}}R.\mathord {\textnormal {\textsf {plus}}}(x_{1},x_{2})=R.\mathord {\textnormal {\textsf {plus}}}(x_{2},x_{1})\)
  • -\(\_:\prod _{x}R.\mathord {\textnormal {\textsf {plus}}}(x,R.\mathord {\textnormal {\textsf {neg}}}(x))=R.\mathord {\textnormal {\textsf {zero}}}\)
  • -\(\_:\prod _{x}R.\mathord {\textnormal {\textsf {mul}}}(R.\mathord {\textnormal {\textsf {one}}},x)=x\)
  • -\(\_:\prod _{x}R.\mathord {\textnormal {\textsf {mul}}}(x,R.\mathord {\textnormal {\textsf {one}}})=x\)
  • -\(\_:\prod _{x_{1},x_{2},x_{3}:R.\mathord {\textnormal {\textsf {Carrier}}}}R.\mathord {\textnormal {\textsf {mul}}}(R.\mathord {\textnormal {\textsf {mul}}}(x_{1},x_{2}),x_{3})=R.\mathord {\textnormal {\textsf {mul}}}(x_{1},R.\mathord {\textnormal {\textsf {mul}}}(x_{2},x_{3}))\)
  • -\(\_:\prod _{x,y_{1},y_{2}:R.\mathord {\textnormal {\textsf {Carrier}}}}R.\mathord {\textnormal {\textsf {mul}}}(x,R.\mathord {\textnormal {\textsf {plus}}}(y_{1},y_{2}))=R.\mathord {\textnormal {\textsf {plus}}}(R.\mathord {\textnormal {\textsf {mul}}}(x,y_{1}),R.\mathord {\textnormal {\textsf {mul}}}(x,y_{2}))\)
  • -\(\_:\prod _{x_{1},x_{2},y:R.\mathord {\textnormal {\textsf {Carrier}}}}R.\mathord {\textnormal {\textsf {mul}}}(R.\mathord {\textnormal {\textsf {plus}}}(x_{1},x_{2}),y)=R.\mathord {\textnormal {\textsf {plus}}}(R.\mathord {\textnormal {\textsf {mul}}}(x_{1},y),R.\mathord {\textnormal {\textsf {mul}}}(x_{2},y))\)
型\(\mathord {\textnormal {\textsf {Ring}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を\(\sum _{X:\mathord {\textnormal {\textsf {RingStr}}}(i)}\mathord {\textnormal {\textsf {RingAxiom}}}(X)\)と定義する。\(\mathord {\textnormal {\textsf {Ring}}}(i)\)の要素を(階数\(i\)の)環(ring)と呼ぶ。環\(A,B:\mathord {\textnormal {\textsf {Ring}}}(i)\)に対して、同一視型\(A=B\)は次のレコード型と同値であることが分かる。
  • -\(f:(\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {Carrier}}}\simeq (\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {Carrier}}}\)
  • -\(\_:f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {zero}}})=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {zero}}}\)
  • -\(\_:\prod _{x_{1},x_{2}}f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {plus}}}(x_{1},x_{2}))=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {plus}}}(f(x_{1}),f(x_{2}))\)
  • -\(\_:\prod _{x}f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {neg}}}(x))=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {neg}}}(f(x))\)
  • -\(\_:f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {one}}})=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {one}}}\)
  • -\(\_:\prod _{x_{1},x_{2}}f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {mul}}}(x_{1},x_{2}))=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {mul}}}(f(x_{1}),f(x_{2}))\)
この型の要素はいわゆる環同型(ring isomorphism)である。