\(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)\)