Welcome to MathOverflow

Question

0

Hello,

Apparently in COQ the type prod (with one constructor pair) corresponds to cartesian product and the type sig (with one constructor exist) to dependent sum but how is described the fact that the cartesian product is a particular case of dependent sum ? I wonder there is a link between prod and sig but I don't find it explicitely.

Best

flag	asked Dec 12 at 18:25 Asymptotik 225●7

3

Note that if you don't get any help here (wait a few days), you may want to ask on the Coq mailing list, which you can sign up to without trouble (and post a message here saying you've done so). – David Roberts Dec 12 at 23:26

Asymptotik · Answer 1 · 2012-12-28 15:06:43Z UTC

1

Actually, the type prod is more akin to sigT than sig. You can use sigT to define a prod' and show there is a bijection between the two types prod and prod' (but they cannot be definitionally equal).

answered Dec 28 at 15:06

Asymptotik
225●7

	More precisely, `prodT` and `sigT` (which act on Type`s) correspond. I don't know anything `sig-like that corresponds directly to `prod` (which acts on `Set`s). One could also define something `prod`-like that corresponds directly to `sig` (which acts on a `Set` and a (dependent) `Prop`). – Toby Bartels Jan 11 at 15:38
	But these are pretty much technicalities. The differences between `Set` and `Type` are rarely relevant (`Prop` is more so). – Toby Bartels Jan 11 at 15:39

prod and sig in COQ

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

1 Answer

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.