[Agda] Re: Forall and product

[Chris Jenkins]

On Tue, Feb 17, 2015 at 4:38 AM, N. Raghavendra <raghu at hri.res.in> wrote:

> At 2015-02-17T11:03:12+01:00, Andrea Vezzosi wrote:
>
> I guess I should get used to the fact that it's only syntactic sugar.
> Whenever I see "forall x -> B x" I keep thinking "\prod_x B(x)".  But I
> think of "(x : _) -> B x" also as "\prod_x B(x)", so I guess it's ok.
>
>
The problem here is in terminology, unfortunately. The "dependent product"
is the pi type (dependent function type), which has a logical
interpretation of "for all". The "dependent sum" is the sigma type
(dependent pair type), which as a logical interpretation of "there exists".
This conflicts with referring to (dependent) pairs as a (Cartesian) product.


-- 
Christopher Jenkins
Embedded Systems Software Engineer
Genesi USA Inc.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150217/d386e788/attachment.html