[Agda] Re: Forall and product

Wed Feb 25 11:37:50 CET 2015

Intuitively it is clear that Pi-types generalise functions and Sigma-types
generalise the non-dependent product.

Mathematicians are often affected by their education in destructive
Mathematics and don¹t always have the best taste in terminology.

Cheers,
Thorsten

On 25/02/2015 09:06, "Martin Escardo" <m.escardo at cs.bham.ac.uk> wrote:

>
>
>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
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.