[Agda] Re: Forall and product

[Andreas Abel]

My verbalization is

   Pi    : "dependent function type"
   Sigma : "dependent pair type"

which is non-ambiguous.  I also avoid "dependent product".

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/