 where \(\Sigma x {:} A.\, B\) is the disjoint sum of the \(A\)-indexed family of types \(B\) and \(\Pi x {:} A.\, B\) is its cartesian product. The canonical elements of \(\Sigma x {:} A.\, B\) are pairs \((a,b)\) such that \(a {:} A\) and \(b {:} B[x:=a]\) (the type obtained by substituting all free occurrences of \(x\) in \(B\) by \(a\)). The elements of \(\Pi x {:} A.\, B\) are (computable) functions \(f\) such that \(f\,a {:} B[x:=a]\), whenever \(a {:} A\).