[Agda] Re: Forall and product

[Martin Escardo]

On 24/02/15 21:23, Andreas Abel wrote:
> I am using terminology compatible with the rest of IT. ;-)

:-)

Look at page 26 of Bibliopolis
https://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf
Chapter "Cartesian product of a family of sets", which defines Pi.

The look at page 39.
Chapter "Disjoint union of a family of sets", which defines Sigma.

Martin-Loef himself is using the same terminology as the rest of
mathematicians.

Best wishes,
Martin


> 
> On 18.02.2015 15:11, Martin Escardo wrote:
>> It would be good if people used terminology compatible with the rest of
>> mathematics:
>>
>> https://en.wikipedia.org/wiki/Cartesian_product#Infinite_products
>> https://en.wikipedia.org/wiki/Disjoint_union
>>
>> M.
>>
>> On 18/02/15 11:20, Martin Escardo wrote:
>>>
>>>
>>> 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