[Agda] Re: Forall and product

[N. Raghavendra]

At 2015-02-17T12:22:58-06:00, Chris Jenkins wrote:

> 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.

I don't know if there's a conflict.  If A and B are two sets, their
Cartesian product AxB equals the sum or disjoint-union of the constant
family (B(a))_{a:A} which is given by B(a)=B for all a in A.  So the
Cartesian product AxB is a sum also, no?

Cheers,
Raghu.

--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/