types - COQ 中 prod 和 sig 类型的关系

Question

在 COQ 中， prod 类型(具有一对构造函数)对应于笛卡尔积，而类型 sig(存在一个构造函数)对应于依赖和，但是如何描述笛卡尔积是依赖和的特殊情况这一事实？我想知道 prod 和 sig 之间是否存在联系，例如一些定义相等，但我在引用手册中没有明确找到它。

Answer 1

事实上，类型 prod 比 sigT 更类似于 sig :

Inductive prod (A B : Type) : Type :=
  pair : A -> B -> A * B

Inductive sig (A : Type) (P : A -> Prop) : Type :=
  exist : forall x : A, P x -> sig P

Inductive sigT (A : Type) (P : A -> Type) : Type :=
  existT : forall x : A, P x -> sigT P

从元理论的角度来看， prod 只是 sigT 的一个特例，其中 snd 组件不依赖于 fst 组件。也就是说，您可以定义:

Definition prod' A B := @sigT A (fun _ => B).

Definition pair' {A B : Type} : A -> B -> prod' A B := @existT A (fun _ => B).

Definition onetwo := pair' 1 2.

但是，它们不能在定义上相等，因为它们是不同的类型。你可以展示一个双射:

Definition from {A B : Type} (x : @sigT A (fun _ => B)) : prod A B.
Proof. destruct x as [a b]. auto. Defined.

Definition to {A B : Type} (x : prod A B) : @sigT A (fun _ => B).
Proof. destruct x as [a b]. econstructor; eauto. Defined.

Theorem fromto : forall {A B : Type} (x : prod A B), from (to x) = x.
Proof. intros. unfold from, to. now destruct x. Qed.

Theorem tofrom : forall {A B : Type} (x : @sigT A (fun _ => B)), to (from x) = x.
Proof. intros. unfold from, to. now destruct x. Qed.

但这不是很有趣... :)