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

\(\mathord {\textnormal {\textsf {Magma}}}(i)\)の要素をマグマ(magma)と呼ぶ。