[Agda] Re: Forall and product

[Martin Escardo]

On 18/02/15 11:03, Andreas Abel wrote:
> My verbalization is
>
>    Pi    : "dependent function type"
>    Sigma : "dependent pair type"
>
> which is non-ambiguous.  I also avoid "dependent product".

I agree with that.

But when you use type theory (and Agda in particular) to do
mathematics, you may come across things such as "a product of compact
spaces is compact". What is meant in general is that Pi(i:I). C i is
compact if each C i is compact, for any I-indexed family C. And in
particular that A x B is compact if A and B are compact,
regarding A x B as a Pi type as in (3) below.

Martin



> Cheers,
> Andreas
>
> On 17.02.2015 21:51, Martin Escardo wrote:
>>
>>
>> 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.
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe