[000B] レコード型

• -単位型(unit type)$\mathbf {1}:\mathcal {U}(0)$を構成できる。
• -要素$\mathord {\star }:\mathbf {1}$を構成できる。
• -要素$a:\mathbf {1}$に対し、$a\equiv \mathord {\star }$と定義される。

$i$を階数、$A:\mathcal {U}(i)$を型、$B:A\to \mathcal {U}(i)$を型の族とする。

• -対型(pair type)$\sum _{x:A}B(x):\mathcal {U}(i)$を構成できる。
• -要素$a:A$と$b:B(a)$に対し、対(pair)$\mathord {\textnormal {\textsf {pair}}}(a,b):\sum _{x:A}B(x)$を構成できる。
• -要素$c:\sum _{x:A}B(x)$に対し、射影(projection)$\mathord {\textnormal {\textsf {proj}}}_{1}(c):A$と$\mathord {\textnormal {\textsf {proj}}}_{2}(c):B(\mathord {\textnormal {\textsf {proj}}}_{1}(c))$を構成できる。
• -要素$a:A$と$b:B(a)$に対し、$\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {pair}}}(a,b))\equiv a$, $\mathord {\textnormal {\textsf {proj}}}_{2}(\mathord {\textnormal {\textsf {pair}}}(a,b))\equiv b$と定義される。
• -要素$c:\sum _{x:A}B(x)$に対し、$c\equiv \mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(c),\mathord {\textnormal {\textsf {proj}}}_{2}(c))$と定義される。

$i$を階数、$A,B:\mathcal {U}(i)$を型とする。型$A\times B:\mathcal {U}(i)$を$\sum _{x:A}B$と定義する。

• -$\times$は右結合の演算子である。例えば、$A\times B\times C$は$A\times (B\times C)$と読む。
• -$\sum _{x:A}$の結合は弱い。例えば、$\sum _{x:A}\sum _{y:B}C\times D$は$\sum _{x:A}(\sum _{y:B}(C\times D))$と読む。

記法$\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}x_{1}:A_{1},\dots ,x_{n}:A_{n}\mathclose {|\negmedspace \} }$を次のように定める。

• -$\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathclose {|\negmedspace \} }$は$\mathbf {1}$のこととする。
• -$\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}x_{1}:A_{1},\dots ,x_{n+1}:A_{n+1}\mathclose {|\negmedspace \} }$は$\sum _{x_{1}:A_{1}}\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}x_{2}:A_{2},\dots ,x_{n+1}:A_{n+1}\mathclose {|\negmedspace \} }$のこととする。

• -$\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathclose {|\negmedspace \} }$は$\mathord {\star }$のこととする。
• -$\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}x_{1}\equiv a_{1},\dots ,x_{n+1}\equiv a_{n+1}\mathclose {|\negmedspace \} }$は$\mathord {\textnormal {\textsf {pair}}}(a_{1},\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}x_{2}\equiv a_{2},\dots ,x_{n+1}\equiv a_{n+1}\mathclose {|\negmedspace \} })$のこととする。

• -$y$が$x_{1}$の時、$a.x_{1}$は$\mathord {\textnormal {\textsf {proj}}}_{1}(a)$のこととする。
• -$y$が$x_{2}$から$x_{n}$のいずれかの時、$a.y$は$(\mathord {\textnormal {\textsf {proj}}}_{2}(a)).y$のこととする。

大きなレコード型を定義する際には、文章内で$\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}x_{1}:A_{1},\dots ,x_{n}:A_{n}\mathclose {|\negmedspace \} }$と書く代わりに縦に並べて

• -$x_{1}:A_{1}$
• -$\vdots$
• -$x_{n}:A_{n}$

$i$を階数、$A,B:\mathcal {U}(i)$を型とする。型$A\leftrightarrow B:\mathcal {U}(i)$を$\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {to}}}:A\to B,\mathord {\textnormal {\textsf {from}}}:B\to A\mathclose {|\negmedspace \} }$と定義する。$A\leftrightarrow B$の要素がある時、$A$と$B$は論理的に同値(logically equivalent)であると言う。反射律、対称律、推移律を次のように構成できる。

• -$\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {to}}}\equiv \mathord {\textnormal {\textsf {id}}},\mathord {\textnormal {\textsf {from}}}\equiv \mathord {\textnormal {\textsf {id}}}\mathclose {|\negmedspace \} }:A\leftrightarrow A$
• -$\lambda e.\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {to}}}\equiv e.\mathord {\textnormal {\textsf {from}}},\mathord {\textnormal {\textsf {from}}}\equiv e.\mathord {\textnormal {\textsf {to}}}\mathclose {|\negmedspace \} }:(A\leftrightarrow B)\to (B\leftrightarrow A)$
• -$\lambda (e,f).\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {to}}}\equiv f.\mathord {\textnormal {\textsf {to}}}\circ e.\mathord {\textnormal {\textsf {to}}},\mathord {\textnormal {\textsf {from}}}\equiv e.\mathord {\textnormal {\textsf {from}}}\circ f.\mathord {\textnormal {\textsf {from}}}\mathclose {|\negmedspace \} }:(A\leftrightarrow B)\to (B\leftrightarrow C)\to (A\leftrightarrow C)$

$i$を階数、$A_{1},A_{2},A_{3}:\mathcal {U}(i)$を型とする。関数$f:A_{1}\to A_{2}$と$g:A_{2}\to A_{3}$と$h:A_{3}\to A_{1}$がある時、各$A_{n}$と$A_{m}$は論理的に同値であることを確かめよ。

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

• -$\mathord {\textnormal {\textsf {Carrier}}}:\mathcal {U}(i)$
• -$\mathord {\textnormal {\textsf {point}}}:\mathord {\textnormal {\textsf {Carrier}}}$

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

• -$\mathord {\textnormal {\textsf {Carrier}}}:\mathcal {U}(i)$
• -$\mathord {\textnormal {\textsf {op}}}:\mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}$

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

• -$\mathord {\textnormal {\textsf {Vertex}}}:\mathcal {U}(i)$
• -$\mathord {\textnormal {\textsf {Edge}}}:\mathord {\textnormal {\textsf {Vertex}}}\to \mathord {\textnormal {\textsf {Vertex}}}\to \mathcal {U}(i)$
• -$\mathord {\textnormal {\textsf {refl}}}:\prod _{x:\mathord {\textnormal {\textsf {Vertex}}}}\mathord {\textnormal {\textsf {Edge}}}(x,x)$

$i$を階数、$A:\mathcal {U}(i)$を型、$B:A\to \mathcal {U}(i)$を型の族、$C:\prod _{x:A}B(x)\to \mathcal {U}(i)$を型の族とする。

• -関数$f:\prod _{z:\sum _{x:A}B(x)}C(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z))$に対し、カリー化(currying)$\mathord {\textnormal {\textsf {curry}}}(f):\prod _{x:A}\prod _{y:B(x)}C(x,y)$を$\lambda (x,y).f(\mathord {\textnormal {\textsf {pair}}}(x,y))$と定義する。
• -関数$g:\prod _{x:A}\prod _{y:B(x)}C(x,y)$に対し、逆カリー化(uncurrying)$\mathord {\textnormal {\textsf {uncurry}}}(g):\prod _{z:\sum _{x:A}B(x)}C(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z))$を$\lambda z.g(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z))$と定義する。

[0014]において、$\mathord {\textnormal {\textsf {uncurry}}}(\mathord {\textnormal {\textsf {curry}}}(f))\equiv f$と$\mathord {\textnormal {\textsf {curry}}}(\mathord {\textnormal {\textsf {uncurry}}}(g))\equiv g$を確かめよ。

$i$を階数、$A:\mathcal {U}(i)$を型、$B:A\to \mathcal {U}(i)$を型の族、$C:\prod _{x:A}B(x)\to \mathcal {U}(i)$を型の族とする。

• -関数$\mathord {\textnormal {\textsf {assoc}}}(C):(\sum _{z:\sum _{x:A}B(x)}C(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z)))\to (\sum _{x:A}\sum _{y:B(x)}C(x,y))$を$\lambda w.\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {proj}}}_{1}(w)),\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{2}(\mathord {\textnormal {\textsf {proj}}}_{1}(w)),\mathord {\textnormal {\textsf {proj}}}_{2}(w)))$と定義する。
• -関数$\mathord {\textnormal {\textsf {assoc}}}^{-1}(C):(\sum _{x:A}\sum _{y:B(x)}C(x,y))\to (\sum _{z:\sum _{x:A}B(x)}C(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z)))$を$\lambda w.\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(w),\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {proj}}}_{2}(w))),\mathord {\textnormal {\textsf {proj}}}_{2}(\mathord {\textnormal {\textsf {proj}}}_{2}(w)))$と定義する。

[0016]において、$\mathord {\textnormal {\textsf {assoc}}}^{-1}(C)\circ \mathord {\textnormal {\textsf {assoc}}}(C)\equiv \mathord {\textnormal {\textsf {id}}}$と$\mathord {\textnormal {\textsf {assoc}}}(C)\circ \mathord {\textnormal {\textsf {assoc}}}^{-1}(C)\equiv \mathord {\textnormal {\textsf {id}}}$を確かめよ。

$i$を階数、$A,B:\mathcal {U}(i)$を型とする。関数$\mathord {\textnormal {\textsf {sym}}}(A,B):A\times B\to B\times A$を$\lambda z.\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{2}(z),\mathord {\textnormal {\textsf {proj}}}_{1}(z))$と定義する。

[0018]において、$\mathord {\textnormal {\textsf {sym}}}(B,A)\circ \mathord {\textnormal {\textsf {sym}}}(A,B)\equiv \mathord {\textnormal {\textsf {id}}}$であることを確かめよ。

$i$を階数、$A:\mathcal {U}(i)$を型、$B:A\to \mathcal {U}(i)$を型の族、$C:\prod _{x:A}B(x)\to \mathcal {U}(i)$を型の族とする。

• -関数$\mathord {\textnormal {\textsf {dist}}}(C):(\prod _{x:A}\sum _{y:B(x)}C(x,y))\to (\sum _{f:\prod _{x:A}B(x)}\prod _{x:A}C(x,f(x)))$を$\lambda h.\mathord {\textnormal {\textsf {pair}}}(\lambda x.\mathord {\textnormal {\textsf {proj}}}_{1}(h(x)),\lambda x.\mathord {\textnormal {\textsf {proj}}}_{2}(h(x)))$と定義する。
• -関数$\mathord {\textnormal {\textsf {dist}}}^{-1}(C):(\sum _{f:\prod _{x:A}B(x)}\prod _{x:A}C(x,f(x)))\to (\prod _{x:A}\sum _{y:B(x)}C(x,y))$を$\lambda k.\lambda x.\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(k(x)),\mathord {\textnormal {\textsf {proj}}}_{2}(k(x)))$と定義する。

[001A]において、$\mathord {\textnormal {\textsf {dist}}}^{-1}(C)\circ \mathord {\textnormal {\textsf {dist}}}(C)\equiv \mathord {\textnormal {\textsf {id}}}$と$\mathord {\textnormal {\textsf {dist}}}(C)\circ \mathord {\textnormal {\textsf {dist}}}^{-1}(C)\equiv \mathord {\textnormal {\textsf {id}}}$を確かめよ。

$i$を階数、$A:\mathcal {U}(i)$を型とする。関数$\mathord {\textnormal {\textsf {diag}}}(A):A\to A\times A$であって、任意の$a:A$に対して$\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {diag}}}(A,a))\equiv a$かつ$\mathord {\textnormal {\textsf {proj}}}_{2}(\mathord {\textnormal {\textsf {diag}}}(A,a))\equiv a$となるものを構成せよ。