In intuitionistic type theory there are primitive type formers \(\Sigma\) and \(\Pi\) for general sums and products, and \(\I\) for identity types, analogous to the set-theoretic constructions described above. The identity type \(\I(\N,m,n)\) corresponding to the set \(\E_{m,n}\) is an example of a dependent type since it depends on \(m\) and \(n\). It is also called an indexed family of types since it is a family of types indexed by \(m\) and \(n\). Similarly, we can form the general disjoint sum \(\Sigma x {:} A.\, B\) and the general cartesian product \(\Pi x {:} A.\, B\) of such a family of types \(B\) indexed by \(x {:} A\), corresponding to the set theoretic sum and product operations above.