商类型（Quotient Type），也称划分类型，通过给定义一个定义在某一类型 α 上的关系R：α → α→ ℙ，将类型α 中，满足关系R的元素摘出来，组成该商类型（Quotient），记 α / R。简单来说，有：
a,b : α，R a b ⊢ a,b : α / R
如，定义在自然数（Nat）上的相等关系，即 α ≡ Nat，R ≡ Eq，有商类型 Nat / Eq，其元素包含所有自相等的自然数，即所有自然数，有 | Nat / Eq | = | Nat |。
1. 类型规则（Type Formation Rule）：
2. 构建函数（Introduction Rule）：
3. 使用函数（Eliminator Rule）:
4. 相等规则（Equality Rule）:
5. 步进规则（Progress Rule）:
口
