[Agda] Re: Forall and product

[Martin Escardo]

On 25/02/15 08:26, Andreas Abel wrote:
> 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.

Well, for some mathematicians, type theory is becoming everyday use.

Best wishes,
Martin



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

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