\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型とする。型\(\mathord {\textnormal {\textsf {Retract}}}(A,B):\mathcal {U}(i)\)を次のレコード型と定義する。

• -\(\mathord {\textnormal {\textsf {retraction}}}:B\to A\)
• -\(\mathord {\textnormal {\textsf {section}}}:A\to B\)
• -\(\mathord {\textnormal {\textsf {r-s}}}:\prod _{x:A}\mathord {\textnormal {\textsf {retraction}}}(\mathord {\textnormal {\textsf {section}}}(x))=x\)

\(\mathord {\textnormal {\textsf {Retract}}}(A,B)\)は\(A\triangleleft B\)と書くこともある。\(A\triangleleft B\)の要素がある時、\(A\)は\(B\)のレトラクト(retract)であると言う。また、\(A\mathrel {\triangleleft \triangleright }B\)を\((A\triangleleft B)\times (B\triangleleft A)\)と定義する。