关于《同伦型论》（HoTT）书中乘积类型唯一性原理证明的循环性疑问

你提出的这个循环性困惑，其实是很多刚接触HoTT的学习者都会碰到的核心问题——本质上是混淆了「归纳类型的消除规则设计逻辑」和「我们要证明的唯一性命题」这两个不同层面的内容。我来帮你拆解清楚：

首先先回顾你提到的书中关键内容：

The way to construct pairs is obvious: given $a : A$ and $b : B$, we may form $(a,b) : A \times B$. ... We expect that “every element of $A \times B$ is a pair”, which is the uniqueness principle for products; we do not assert this as a rule of type theory, but we will prove it later on as a propositional equality.

Now, how can we use pairs, i.e. how can we define functions out of a product type? Let us first consider the definition of a non-dependent function $f : A \times B \to C$. Since we intend the only elements of $A \times B$ to be pairs, we expect to be able to define such a function by prescribing the result when f is applied to a pair $(a, b)$. We can prescribe these results by providing a function $g: A \to B \to C$. Thus, we introduce a new rule (the elimination rule for products), which says that for any such $g$, we can define a function $f: A \times B \to C$ by $f((a,b)) :\equiv g(a)(b)$.

你觉得矛盾的点在于：消除规则里直接用$(a,b)$作为$f$的参数，看起来像是已经默认了「所有$A×B$的元素都是对」，但书中又说这个结论是要后续证明的，这不是循环吗？

核心澄清：消除规则不是“假设结论”，而是归纳类型的定义属性 #

这里的关键是理解：归纳类型的消除规则（比如乘积类型的函数定义规则），是归纳类型本身的定义组成部分，而非基于“所有元素都是构造器生成的”这个前提。

对于任意归纳类型（比如自然数、乘积类型、和类型），消除规则的本质是：

• 要定义一个从该归纳类型到任意类型$C$的函数，只需要指定这个函数在所有构造器生成的元素上的行为即可。
  这是归纳类型的核心特性——它不是在“假设所有元素都是构造器生成的”，而是在定义“如何合法地构造从这个类型出发的函数”。就像自然数的递归规则：要定义$Nat \to C$的函数，你只需要指定0的取值，以及给定$n:Nat$时后继$succ(n)$的取值，不需要先证明“所有自然数都是0或后继”。

回到乘积类型的消除规则：
$f((a,b)) :\equiv g(a)(b)$这句话的意思，不是“因为每个元素都是$(a,b)$所以我们这么定义”，而是：我们定义函数$f$时，只需要说明它在构造器生成的对$(a,b)$上的取值，剩下的由归纳原理自动保证这个函数对所有$A×B$的元素都是良定义的。

唯一性原理的证明为什么不循环？ #

我们用这个消除规则来构造唯一性的见证函数uniq_{A×B}: ∏_{x:A×B} ((pr₁(x), pr₂(x)) =_{A×B} x)，具体定义是：

• 当$x$是构造器生成的对$(a,b)$时，uniq((a,b)) :≡ refl_{(a,b)}——因为$pr₁((a,b))=a$、$pr₂((a,b))=b$，所以$(pr₁((a,b)), pr₂((a,b)))=(a,b)$，用自反性refl即可。

而根据消除规则，这个定义可以自动扩展到所有$x:A×B$的元素——不管$x$是不是“看起来像”对，消除规则都保证了uniq函数对所有$x$都有合法的取值。最终我们得到的这个函数，就是“每个元素都命题等于某个对”的见证，也就是我们要证明的唯一性原理。

总结 #

这里没有循环：消除规则是归纳类型的定义工具，它允许我们基于构造器来定义函数；而唯一性原理是这个工具的推论——我们用消除规则构造出了见证唯一性的函数，而不是预先假设了唯一性才能使用消除规则。

备注：内容来源于stack exchange，提问作者Xiaojia Rao