[Agda] Re: Forall and product

[Jon Sterling]

I use the following terms, which I think disambiguate it quite nicely:

Pi : "family cartesian product"
Sg : "family disjoint union"

This approach scales nicely to other quantifiers too. For instance, we
have the intersection of a family, and the union of a family as well
(though not in Agda).

I think that these terms were used in Nordström/Kent/Smith's
"Programming in Martin-Löf Type Theory" in the development of the theory
of sets.

If I recall correctly, nowadays Martin-Löf uses the term "dependent
function" to denote a *type* (x:α)β in his logical framework, as opposed
to a *set* Pi(A; [x]B). He uses the dependent function type to represent
hypothetico-general judgement in his object languages, including his
monomorphic theory of sets.

JMS


On Wed, Feb 18, 2015, at 03:03 AM, Andreas Abel wrote:
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda