Let \(T_{1}\) be a type theory and let \(T_{2}\) be a type theory internal to \(T_{1}\). We work in \(T_{2}\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\), let \(A:\mathord {\textnormal {\textsf {Type}}}(i)\) in \(T_{1}\), and let \(B(x):\mathord {\textnormal {\textsf {Type}}}(i)\) under assumption \(x:A\). We say \(T_{2}\) has the product of \(B\) if the following rules are derivable.

• -\(\prod _{x:A}B(x):\mathord {\textnormal {\textsf {Type}}}(i)\).
• -Let \(b(x):B(x)\) under assumption \(x:A\). Then \(x\mapsto b(x):\prod _{x:A}B\).
• -Let \(a:A\) and let \(f:\prod _{x:A}B\). Then \(f(a):B(a)\).
• -Let \(a:A\) and let \(b(x):B(x)\) under assumption \(x:A\). Then \((x\mapsto b(x))(a)\equiv b(a)\).
• -Let \(f:\prod _{x:A}B\). Then \(f\equiv x\mapsto f(x)\).