我试图在 Coq 中定义不同类型的等式。在大学课程中，我的教授给了我们四种不同类型的规则，如下（我只提供规则的链接）：
这四种类型的区别在于C型。
我试图证明它们之间的同构。不幸的是，我在将第一个和第二个声明为归纳类型时遇到了一些麻烦，因为我找不到指定类型 C 的方法。我有第三个和第四个的定义，并且我已经证明了它们之间的同构。
提前致谢。
你不能完全使用归纳类型来获得完全体现前两个原则的东西而不得到其他两个原则。原因是 Coq 归纳数据类型自动支持强依赖消除，这意味着允许结果类型引用被消除的元素。这就是您在给出的最后两组规则中看到的内容：C允许类型引用p两点a和b相等的证明。任何合理的归纳定义等式类型将自动支持规则 3 和 4，因此支持更弱的规则 1 和 2。例如，下面是如何通过 Coq 的标准相等得到 1 和 2。
Section Gentzen.
Variables (A : Type) (C : A -> A -> Type).
Definition e_id_g {a b : A} (p : a = b) (c : C a a) : C a b :=
match p with eq_refl => fun c => c end c.
Definition c_id_g (a : A) (c : C a a) : e_id_g (eq_refl a) c = c :=
eq_refl.
End Gentzen.
Section Leibniz.
Variables (A : Type) (C : A -> A -> Type).
Definition e_id_l {a b : A} (p : a = b) (c : forall x, C x x) : C a b :=
match p with eq_refl => c a end.
Definition c_id_l (a : A) (c : forall x, C x x) :
e_id_l (eq_refl a) c = c a :=
eq_refl.
End Leibniz.
通过使用相等的Church 编码，可以给出仅支持规则 1 和 2，但不支持规则 3 和 4 的不同定义：
Definition eq {A} (a b : A) : Prop :=
forall P : A -> Prop, P a -> P b.
Definition refl {A} (a : A) : eq a a :=
fun P x => x.
这里的想法 - 就像 lambda 演算中数据类型的类似编码一样 - 是将类型定义为其（非依赖）消除器或折叠的类型。这个定义有时被称为 Leibniz 等式，并且确实提供了与您在 1 和 2 中得到的基本相同的证明规则，如下面的脚本所示。
Section Gentzen.
Variables (A : Type) (C : A -> A -> Prop).
Definition e_id_g {a b : A} (p : eq a b) (c : C a a) : C a b :=
p (C a) c.
Definition c_id_g (a : A) (c : C a a) : e_id_g (refl a) c = c :=
eq_refl.
End Gentzen.
Section Leibniz.
Variables (A : Type) (C : A -> A -> Prop).
Definition e_id_l {a b : A} (p : eq a b) (c : forall x, C x x) : C a b :=
p (C a) (c a).
Definition c_id_l (a : A) (c : forall x, C x x) :
e_id_l (refl a) c = c a :=
eq_refl.
End Leibniz.
（这些原则实际上有点不同：它们被限制为Prop，由于 Coq 的基本理论中的限制与所谓的不可预测性有关。但这是一个正交问题。）
如果不断言额外的公理，就不可能为这种新的平等编码获得原则 3 和 4。证明这一点需要对 type 的元素进行案例分析forall P, P a -> P b，并论证所有这些元素都是refl应用于某物的形式。但是，这是一种函数，在 Coq 的基础理论中没有办法对它们进行案例分析。请注意，这个论点超出了 Coq 的理论：断言 3 和 4 对于这种新类型是有效的作为额外公理并不矛盾；如果没有这些公理，就不可能证明这一点。