一価性(と関数外延性)の帰結として、構造同一原理(structure identity principle)をいくつか例示する。構造とは厳密に定義はしないが、なんらかの数学的構造を表すレコード型のこととする。構造同一原理は、構造の同一視型は構造を保つ同値の型と同値であることを主張する。
ある構造\(A\)と要素\(a:A\)に対し、同一視型\(\lambda x.(a=x)\)を特徴付けるには、候補\(E:A\to \mathcal {U}(i)\)を見つけて\(\sum _{x:A}E(x)\)が可縮であることを示す。要素\(e:E(a)\)を自然に見つけられる場合がほとんどで、[001S]から\((a=x)\simeq E(x)\)を得る。基本的な戦略は目的の型から始めて、既に可縮と分かっている型になるまでレトラクトの列を作ることである(実際には同値の列を作れる場合が多い)。すると[001K]により目的の型が可縮であることが従う。レトラクトの列を作る際には[0025]が便利で、大きなレコード型の一部に同一視型の特徴付けを知っている部分があれば、そのレコード型はより単純な型のレトラクトであることを示せる。また、レコード型の要素を並び換える関数はレトラクションであることも便利である。
\(i\)を階数とする。\(\mathcal {U}_{\bullet }(i)\) ([008A])の同一視型を特徴付ける。\(A:\mathcal {U}_{\bullet }(i)\)に対し、\(E:\mathcal {U}_{\bullet }(i)\to \mathcal {U}(i)\)を\(\lambda Z.(\sum _{e:A.\mathord {\textnormal {\textsf {Carrier}}}\simeq Z.\mathord {\textnormal {\textsf {Carrier}}}}e(A.\mathord {\textnormal {\textsf {point}}})=Z.\mathord {\textnormal {\textsf {point}}})\)と定義する。要素\(\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {id}}},\mathord {\textnormal {\textsf {refl}}}):E(A)\)を得る。レトラクトの列
\(\sum _{Z:\mathcal {U}_{\bullet }(i)}E(Z)\)\(\triangleleft \) {並び換え}\(\sum _{X:\mathcal {U}(i)}\sum _{e:A.\mathord {\textnormal {\textsf {Carrier}}}\simeq X}\sum _{x:X}e(A.\mathord {\textnormal {\textsf {point}}})=x\)\(\triangleleft \) {一価性}\(\sum _{x:A.\mathord {\textnormal {\textsf {Carrier}}}}A.\mathord {\textnormal {\textsf {point}}}=x\)
を得て、最後の型は
[001N]より可縮なので、
\(\sum _{Z:\mathcal {U}_{\bullet }(i)}E(Z)\)は可縮である。
\(i\)を階数とする。\(\mathord {\textnormal {\textsf {Magma}}}(i)\) ([008B])の同一視型を特徴付ける。\(A:\mathord {\textnormal {\textsf {Magma}}}(i)\)に対し、\(E:\mathord {\textnormal {\textsf {Magma}}}(i)\to \mathcal {U}(i)\)を
\(\lambda Z.(\sum _{e:A.\mathord {\textnormal {\textsf {Carrier}}}\simeq Z.\mathord {\textnormal {\textsf {Carrier}}}}\prod _{x_{1},x_{2}:A.\mathord {\textnormal {\textsf {Carrier}}}}e(A.\mathord {\textnormal {\textsf {op}}}(x_{1},x_{2}))=Z.\mathord {\textnormal {\textsf {op}}}(e(x_{1}),e(x_{2})))\)
と定義する。要素
\(\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {id}}},\lambda (x_{1},x_{2}).\mathord {\textnormal {\textsf {refl}}}):E(A)\)を得る。レトラクトの列
\(\sum _{Z:\mathord {\textnormal {\textsf {Magma}}}(i)}E(Z)\)\(\triangleleft \) {並び換え}\(\sum _{X:\mathcal {U}(i)}\sum _{e:A.\mathord {\textnormal {\textsf {Carrier}}}\simeq X}\sum _{f:X\to X\to X}\prod _{x_{1},x_{2}:A.\mathord {\textnormal {\textsf {Carrier}}}}e(A.\mathord {\textnormal {\textsf {op}}}(x_{1},x_{2}))=f(e(x_{1}),e(x_{2}))\)\(\triangleleft \) {一価性}\(\sum _{f:A.\mathord {\textnormal {\textsf {Carrier}}}\to A.\mathord {\textnormal {\textsf {Carrier}}}\to A.\mathord {\textnormal {\textsf {Carrier}}}}\prod _{x_{1},x_{2}:A.\mathord {\textnormal {\textsf {Carrier}}}}A.\mathord {\textnormal {\textsf {op}}}(x_{1},x_{2})=f(x_{1},x_{2})\)
を得て、最後の型は関数外延性により可縮なので、
\(\sum _{Z:\mathord {\textnormal {\textsf {Magma}}}(i)}E(Z)\)は可縮である。
\(i\)を階数とする。\(\mathord {\textnormal {\textsf {ReflGraph}}}(i)\) ([008C])の同一視型を特徴付ける。\(A:\mathord {\textnormal {\textsf {ReflGraph}}}(i)\)と\(Z:\mathord {\textnormal {\textsf {ReflGraph}}}(i)\)に対し、\(E(Z):\mathcal {U}(i)\)を次のレコード型と定義する。
- -\(v:A.\mathord {\textnormal {\textsf {Vertex}}}\simeq Z.\mathord {\textnormal {\textsf {Vertex}}}\)
- -\(e:\prod _{\lbrace x_{1},x_{2}:A.\mathord {\textnormal {\textsf {Vertex}}}\rbrace }A.\mathord {\textnormal {\textsf {Edge}}}(x_{1},x_{2})\simeq Z.\mathord {\textnormal {\textsf {Edge}}}(v(x_{1}),v(x_{2}))\)
- -\(r:\prod _{x:A.\mathord {\textnormal {\textsf {Vertex}}}}e(A.\mathord {\textnormal {\textsf {refl}}}(x))=Z.\mathord {\textnormal {\textsf {refl}}}(v(x))\)
要素
\(\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}v\equiv \mathord {\textnormal {\textsf {id}}},e\equiv \lambda (x_{1},x_{2}).\mathord {\textnormal {\textsf {id}}},r\equiv \lambda x.\mathord {\textnormal {\textsf {refl}}}\mathclose {|\negmedspace \} }:E(A)\)を得る。レトラクトの列
\(\sum _{Z:\mathord {\textnormal {\textsf {ReflGraph}}}(i)}E(Z)\)\(\triangleleft \) {並び換え}\(\sum _{X:\mathcal {U}(i)}\sum _{v:A.\mathord {\textnormal {\textsf {Vertex}}}\simeq X}\sum _{Y}\sum _{e}\sum _{z}\prod _{x}\_\)\(\triangleleft \) {一価性}\(\sum _{Y:A.\mathord {\textnormal {\textsf {Vertex}}}\to A.\mathord {\textnormal {\textsf {Vertex}}}\to \mathcal {U}(i)}\sum _{e:\prod _{x_{1},x_{2}:A.\mathord {\textnormal {\textsf {Vertex}}}}A.\mathord {\textnormal {\textsf {Edge}}}(x_{1},x_{2})\simeq Y(x_{1},x_{2})}\sum _{z}\prod _{x}\_\)\(\triangleleft \) {関数外延性と一価性}\(\sum _{z:\prod _{x:A.\mathord {\textnormal {\textsf {Vertex}}}}A.\mathord {\textnormal {\textsf {Edge}}}(x,x)}\prod _{x:A.\mathord {\textnormal {\textsf {Vertex}}}}A.\mathord {\textnormal {\textsf {refl}}}(x)=z(x)\)
を得て、最後の型は関数外延性により可縮なので、
\(\sum _{Z:\mathord {\textnormal {\textsf {ReflGraph}}}(i)}E(Z)\)は可縮である。
数学でよく登場する構造といえば群や環などであるが、これらについての構造同一原理を正しく述べるには[003W]で導入する\(n\)型の概念を用いる。[004V]でさらなる構造同一原理を見る。