[Agda] Re: Forall and product

[Martin Escardo]

On 17/02/15 20:15, N. Raghavendra wrote:
> 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.  

There *is* a conflict in the *use of terminology*: some people use
"product" to mean Pi, and other people use "product" to mean "Sigma".

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

And there is an overlap in the *notions* conveyed by the terminologies,
as well.

(1) A + B can be represented by a Sigma type indexed by the two-point
    type 2 with points 0,1:

           C : 2 -> Set
           C 0 = A
           C 1 = B
           A + B = Sigma(n:2).C n.

(2) A x B can be represented by a Sigma type indexed by A, as you say:

           C : A -> Set
           C a = B
           A x B = Sigma(a:A). C a.

(3) A x B can also be represented as a Pi type. Take C as in (1):

           C : 2 -> Set
           C 0 = A
           C 1 = B
           A x B = Pi(n:2). C n.

The relevant particular cases, in my view, are (1) and (3). The
situation (2) can be regarded as a sort of a (useful) "coincidence".

I would advocate calling Pi types "product types" and Sigma types "sum
types". But then we can't change established terminologies, even if
they *are* conflicting: some people mean Sigma when they say "product
types" and other people mean Pi. (And I think it is the people who
mean Pi are the ones who are terminologically correct, in the sense of
being terminologically compatible with e.g. category theory.)

The only way out is to avoid the terminology "product" (unless you
know your audience), at this stage, and instead say "Pi types" and
"Sigma types".

M.