記法\(\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 \} }\)のこととする。

この形の型をレコード型(record type)と呼ぶ。また、記法\(\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}x_{1}\equiv a_{1},\dots ,x_{n}\equiv a_{n}\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 \} })\)のこととする。

これらの記法は、各\(a_{i}\)が\(A_{i}[x_{1}\mapsto a_{1},\dots ,x_{i-1}\mapsto a_{i-1}]\)の要素の時に\(\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}x_{1}\equiv a_{1},\dots ,x_{n}\equiv a_{n}\mathclose {|\negmedspace \} }\)が\(\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}x_{1}:A_{1},\dots ,x_{n}:A_{n}\mathclose {|\negmedspace \} }\)の要素になるように設計されている。さらに、\(a:\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}x_{1}:A_{1},\dots ,x_{n}:A_{n}\mathclose {|\negmedspace \} }\)を要素、\(y\)を\(x_{1}\)から\(x_{n}\)のいずれかとする時、記法\(a.y\)を次のように定める。

• -\(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\)のこととする。

この記法は\(a.x_{i}:A_{i}[x_{1}\mapsto a.x_{1},\dots ,x_{i-1}\mapsto a.x_{i-1}]\)となるように設計されている。また、\((\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}x_{1}\equiv a_{1},\dots ,x_{n}\equiv a_{n}\mathclose {|\negmedspace \} }).x_{i}\equiv a_{i}\)であることと\(a\equiv \mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}x_{1}\equiv a.x_{1},\dots ,x_{n}\equiv a.x_{n}\mathclose {|\negmedspace \} }\)であることを確かめられる。