[Agda] Re: Forall and product

[Andreas Abel]

On 24.02.2015 22:38, Martin Escardo wrote:
> 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.

God bless him!

I guess programmers are more interested in whether something is a pair 
or a function than in Descartes or families of sets.

For mathematicians, this is probably the other way round.  I do not 
object Martin-Löf's terminology, which is very precise, but for everyday 
use I find it a bit unwieldly.

That said, I am not sure "dependent pair type" will catch on like 
"dependent record type" has.

Cheers,
Andreas

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


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/