As a matter of fact, the type prod
is more akin to sigT
than 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
From a meta-theoretic point of view, prod is just a special case of sigT where your snd
component does not depend on your fst
component. That is, you could define:
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.
They can not be definitionally equal though, since they are different types. You could show a bijection:
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.
But that's not very interesting... :)