类型和算数之间有着紧密的联系：元组对应着乘法。因为元组的元素个数就是元组两侧元素个数的乘积，元组类型就是笛卡尔积。加法则是不交并，也就是它的元素要么是 \( A \) 类型的元素，要么是 \( B \) 类型的元素。如果两个类型重合或者一样，我们也可以知道它是由“左边”还是“右边”生成的。它合法的元素数目是它两边元素的数目加在一起。

函数抽象对应着乘方。\( A \rightarrow B \) 就是 \( B^{A} \)。因为本质上从 \( A \) 到 \( B \) 的映射，对于 \( A \) 的每一个元素选择是 \( B \) 这么多种，例如 \( A \) 有两个元素，\( A \rightarrow B \) 的选择就是 \( B^{2} \) 种。

等价性对应着两个类型之间的同构。例如 \( A \times B \times C = A \times (B \times C) \) 可以指两种不同结构的三元组之间可以互相转换。只有一个元素的类型是 \( 1 \)，没有元素的类型是 \( 0 \)。

再比如说我们知道 \( A^{B \times C} = (A^{B})^{C} \)，它对应的类型就是 \( B \times C \rightarrow A \leftrightarrow C \rightarrow B \rightarrow A \)，也就是柯里化。

依赖积是一种对依赖类型的抽象，它扩展了一般函数。写作 \( \forall x : A, B(x) \)。如果 \( B(x) \) 和 \( x \) 无关，它其实就是 \( A \rightarrow B \)。\( B(x) \) 是一组和 \( x \) 有关的类型。它的每个元素都是一个从 \( A \) 到 \( B(x) \) 的映射。你可以想见，不同的 \( B(x) \) 里的元素数量是不一样的。这个类型中有效的项和函数是很类似的，区别只是每一个元素的选择数目是和 \( x \) 有关的。它是：\[ \prod_{x \in A} B(x) \] 可以注意到，如果 \( B(x) \) 是常函数，例如就是 \( C \)，那么这个乘积就会退化成 \( C^{A} \)，C也就是退化成了一个一般的函数。

另外一种依赖类型的抽象，和依赖积可以互相定义的，是依赖和。它写作 \( \exists x : A, B(x) \)。它扩展了一般元组，也就是第二个元素的类型和第一个元素的值有关系。它的每个元素都是由一个 \( x \) 和一个 \( B(x) \) 类的元素组成。它所有的元素就是对于每个 \( x \) 的 \( B(x) \) 数目加在一起。也就是：\[ \sum_{x \in A} B(x) \] 同样地，如果 \( B(x) \) 是常函数，那么这个和就会退化成 \( A \times B \)，也就是一个元组。