Re: The boringness of the dual of exponential

Re: The boringness of the dual of exponential

[RJ Wood]

Your observation about lack of symmetry in \set is underscored by the
fact that the yoneda functor for \set has a left adjoint which has
a left adjoint which has a left adjoint which has a left adjoint but
the co-yoneda functor for \set has a right adjoint that fails to
preserve even finite sums.
R_j

> When David originally posted his question, I thought it was rather
> a silly one and that it was quite rightly dismissed by various
> people.   On the other hand, he now says
>
>> However, I am not yet satisfied. Let me precise my thoughts. In the
>> textbooks and lecture notes on category category that I have read,
>> there are always product and coproduct, pullback and pushout,
>> equalizer and coequalizer, monomorphism and epimorphism, and so on.
>> However exponential is always left alone. That is why I assumed it is
>> boring. If it is not boring, why is it never mentioned in textbooks
>> and lecture notes on category theory?
>
> In other words, these things are "idioms" or "naturally occurring
> things" in mathematics, but there is a gap in the obvious symmetries.
>
> Looking for gaps in symmetries is a good thing to do.  For example
> Dirac (whose biography by Graham Farmelo I have just started reading)
> predicted the positron this way.
>
> Actually, if we're looking at the categorical structure of the category
> of sets, it isn't very symmetrical at all.  The second edition of
> Paul Cohn's "Universal Algebra" was evidently influenced by Mac Lane's
> famous textbook, but illustrates how categorists had way overemphasised
> duality.
>
> For example the terminal object yields the classical notion of element
> or point, whereas the initial object is strict and boring.
>
> Products and coproducts of sets are very different.
>
> I explored this kind of thing in my book.   For example, the section
> on coproducts shows how different they are in sets/spaces and algebras.
>
> So David's question becomes a good one that deserves an answer if
> we read it as one about the phenomenology of mathematics rather than
> its technicalities.
>
> Paul Taylor
>
> PS There is a boring technical answer that I don't think anyone has
> mentioned, namely copowers, especially of modules.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Reinhard Boerger]

Hello!

David Leduc is not satisfied:

>> Take any category E where exponentiable is interesting.
>> Then the dual of exponentiable is not boring in E^op.
> 
> Indeed! And this is clearly true of the example given by Thomas, namely
> Set^op.
> 
> However, I am not yet satisfied. Let me precise my thoughts. In the
> textbooks and lecture notes on category category that I have read,
> there are always product and coproduct, pullback and pushout,
> equalizer and coequalizer, monomorphism and epimorphism, and so on.
> However exponential is always left alone. That is why I assumed it is
> boring. If it is not boring, why is it never mentioned in textbooks
> and lecture notes on category theory?

I wonder whether it makes sense to introduce notions, which only in the
duals of familiar categories. Of course, Set^op is equivalent to the
category of complete atomic Boolean algebras, but I do not see that the dual
of exponentiation plays an important role in the theory if these Boolean
algebras.

> Also, in logic, "and" goes in pair with "or", "for all" goes in pair
> with "there exists". But implication is always left alone. Why is it

In classical logic, one can form this "co-implication" but it does not look
very interesting to me. In intuitionistic logic I do not see how to add it
more ore less meaningfully (e.g. in such a way that it is left adjoint to
"or" in the first argument).


Greetings
Reinhard



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

The boringness of the dual of exponential

[David Leduc]

Dear all,

I have a conjecture: the dual of exponential is boring in any
category. Is there a counterexample to this conjecture? If not how can
we prove it?


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[FEJ Linton]

On Sat, 5 Nov 2011 12:52:03 +0000, David Leduc wrote:

>  ... a conjecture: the dual of exponential is boring in any
> category. Is there a counterexample to this conjecture? If not how can
> we prove it?

Is there a definition behind this conjecture? If so, TIA. Cheers, -- Fred

[PS: this also tests submission of posts via Gmane, aka news.gmane.org .]

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Thomas Streicher]

> I have a conjecture: the dual of exponential is boring in any
> category. Is there a counterexample to this conjecture? If not how
> can we prove it?

Well, if boring means non-trivial there are examples, namely opposites
of cartesian closed categories. E.g. Set^op equivalent to CABA
(complete atomic boolean algebras). E.g. for a topological space X the
poset C(X) of closed subsets of X ordered by set inclusion is an example.
There conegation ~A is the closure of the complement of A and A \cap ~A
is the border of A. This received some attention as models of
"dialectical logic". There are also biHeyting algebras meaning that A
and A^op are Heyting algebras. Subobject lattices of objects in
presheaf toposes are examples of this as observed by Lawvere.
But if you mean by coexponential A x (_) having a left adjoint then
in presence of a terminal object 1 this means A is isomorphic to 1 and
indeed they are trivial.

Thomas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[F. William Lawvere]

The lattice of all subtoposes of any given toposis surely not boring.For example the lattice of positive model classes of 
a given theory needs investigating. Bill

> Date: Sun, 6 Nov 2011 22:55:08 +0100
> From: streicher@mathematik.tu-darmstadt.de
> To: david.leduc6@googlemail.com
> CC: categories@mta.ca
> Subject: categories: Re: The boringness of the dual of exponential
> 
>> I have a conjecture: the dual of exponential is boring in any
>> category. Is there a counterexample to this conjecture? If not how
>> can we prove it?
> 
> Well, if boring means non-trivial there are examples, namely opposites
> of cartesian closed categories. E.g. Set^op equivalent to CABA
> (complete atomic boolean algebras). E.g. for a topological space X the
> poset C(X) of closed subsets of X ordered by set inclusion is an example.
> There conegation ~A is the closure of the complement of A and A \cap ~A
> is the border of A. This received some attention as models of
> "dialectical logic". There are also biHeyting algebras meaning that A
> and A^op are Heyting algebras. Subobject lattices of objects in
> presheaf toposes are examples of this as observed by Lawvere.
> But if you mean by coexponential A x (_) having a left adjoint then
> in presence of a terminal object 1 this means A is isomorphic to 1 and
> indeed they are trivial.
> 
> Thomas
> 

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Ross Street]

On 05/11/2011, at 11:52 PM, David Leduc wrote:

> I have a conjecture: the dual of exponential is boring in any
> category. Is there a counterexample to this conjecture? If not how can
> we prove it?

The conjecture is false.
Take any category E where exponentiable is interesting.
Then the dual of exponentiable is not boring in E^op.
==Ross




[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[David Leduc]

On Mon, Nov 7, 2011 at 07:59, Ross Street <ross.street@mq.edu.au> wrote:
> The conjecture is false.
> Take any category E where exponentiable is interesting.
> Then the dual of exponentiable is not boring in E^op.

Indeed! And this is clearly true of the example given by Thomas, namely Set^op.

However, I am not yet satisfied. Let me precise my thoughts. In the
textbooks and lecture notes on category category that I have read,
there are always product and coproduct, pullback and pushout,
equalizer and coequalizer, monomorphism and epimorphism, and so on.
However exponential is always left alone. That is why I assumed it is
boring. If it is not boring, why is it never mentioned in textbooks
and lecture notes on category theory?

Also, in logic, "and" goes in pair with "or", "for all" goes in pair
with "there exists". But implication is always left alone. Why is it
so?
Is it not the case in "dialectical logic" mentioned by Thomas? By the
way, I'd love to have some reference on models of dialectical logic.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

The boringness of the dual of exponential

[Paul Taylor]

When David originally posted his question, I thought it was rather
a silly one and that it was quite rightly dismissed by various
people.   On the other hand, he now says

> However, I am not yet satisfied. Let me precise my thoughts. In the
> textbooks and lecture notes on category category that I have read,
> there are always product and coproduct, pullback and pushout,
> equalizer and coequalizer, monomorphism and epimorphism, and so on.
> However exponential is always left alone. That is why I assumed it is
> boring. If it is not boring, why is it never mentioned in textbooks
> and lecture notes on category theory?

In other words, these things are "idioms" or "naturally occurring
things" in mathematics, but there is a gap in the obvious symmetries.

Looking for gaps in symmetries is a good thing to do.  For example
Dirac (whose biography by Graham Farmelo I have just started reading)
predicted the positron this way.

Actually, if we're looking at the categorical structure of the category
of sets, it isn't very symmetrical at all.  The second edition of
Paul Cohn's "Universal Algebra" was evidently influenced by Mac Lane's
famous textbook, but illustrates how categorists had way overemphasised
duality.

For example the terminal object yields the classical notion of element
or point, whereas the initial object is strict and boring.

Products and coproducts of sets are very different.

I explored this kind of thing in my book.   For example, the section
on coproducts shows how different they are in sets/spaces and algebras.

So David's question becomes a good one that deserves an answer if
we read it as one about the phenomenology of mathematics rather than
its technicalities.

Paul Taylor

PS There is a boring technical answer that I don't think anyone has
mentioned, namely copowers, especially of modules.



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Uwe.Wolter]

Some short remarks from a dilettante in universal algebra, category
theory and philosophy:

I came along the unsatisfactory asymmetry in the category SET when
looking at coalgebras and asking about coequations some years ago.
Having in mind that kernels play a central role in universal algebra I
was expecting that co-kernels should play a similar role in universal
coalgebra. One can easily dualize the kernel reasoning. Such a
dualization, however, looks kind of artificial since a co-kernel just
provides a "strange coding" of the image of a map, i.e., a subset, so
to speak. One can identify the asymmetry by looking at exponentiation,
but isn't the asymmetry already related to the fact that SET is a
distributive category, i.e., that addition is trivial and boring
compared to multiplication?

My interest in coalgebras was also a kind of philosophically
triggered. The "classical western scientific cultur" relies and
focusses on the existence of "objects/things" and the category SET is
somehow the abstract essence of this perception of the world as a
bunch of objects/things which are assumed to be identifiable and
existing until the end of the time. Buddhistic and/or dialectical
reasoning, in contrast, perceives the world as a net of mutual
dependent and interweaved "processes". So, my question was if there is
anything in mathematics reflecting on a formal level this buddhistic
and dialectical reasoning based on "processes". I don't consider
coalgebras in SET as such formalization. Those coalgebras are based on
"object/thing reasoning" thus they can only give an approximation of
the philosophical concept of a "process", namely in terms of
distinctions and observations.

Uwe Wolter

Quoting Paul Taylor <pt11@PaulTaylor.EU>:

> When David originally posted his question, I thought it was rather
> a silly one and that it was quite rightly dismissed by various
> people.   On the other hand, he now says
>
>> However, I am not yet satisfied. Let me precise my thoughts. In the
>> textbooks and lecture notes on category category that I have read,
>> there are always product and coproduct, pullback and pushout,
>> equalizer and coequalizer, monomorphism and epimorphism, and so on.
>> However exponential is always left alone. That is why I assumed it is
>> boring. If it is not boring, why is it never mentioned in textbooks
>> and lecture notes on category theory?
>
> In other words, these things are "idioms" or "naturally occurring
> things" in mathematics, but there is a gap in the obvious symmetries.
>
> Looking for gaps in symmetries is a good thing to do.  For example
> Dirac (whose biography by Graham Farmelo I have just started reading)
> predicted the positron this way.
>
> Actually, if we're looking at the categorical structure of the category
> of sets, it isn't very symmetrical at all.  The second edition of
> Paul Cohn's "Universal Algebra" was evidently influenced by Mac Lane's
> famous textbook, but illustrates how categorists had way overemphasised
> duality.
>
> For example the terminal object yields the classical notion of element
> or point, whereas the initial object is strict and boring.
>
> Products and coproducts of sets are very different.
>
> I explored this kind of thing in my book.   For example, the section
> on coproducts shows how different they are in sets/spaces and algebras.
>
> So David's question becomes a good one that deserves an answer if
> we read it as one about the phenomenology of mathematics rather than
> its technicalities.
>
> Paul Taylor
>
> PS There is a boring technical answer that I don't think anyone has
> mentioned, namely copowers, especially of modules.
>
>
>
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
>




[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Prof. Peter Johnstone]

One point that no-one has mentioned yet is that you can't have
exponentiation and its dual in the same category, unless it is a
preorder. If exponentiation exists, then the initial object 0 is
strict, and so 0 x 0 = 0 (read all equality signs as isomorphisms).
But if A + (-) has a left adjoint then it distributes over product,
so
A = A + 0 = A + (0 x 0) = (A + 0) x (A + 0) = A x A
which implies that any two maps into A (with the same domain)
are equal. Of course, bi-Heyting algebras (posets P such that
both P and P^op are cartesian closed) are of some interest, as has
already been mentioned; but if you want to work in non-preordered
categories then you have to choose one or the other.

Peter Johnstone

On Tue, 8 Nov 2011, Paul Taylor wrote:

> When David originally posted his question, I thought it was rather
> a silly one and that it was quite rightly dismissed by various
> people.   On the other hand, he now says
>
>> However, I am not yet satisfied. Let me precise my thoughts. In the
>> textbooks and lecture notes on category category that I have read,
>> there are always product and coproduct, pullback and pushout,
>> equalizer and coequalizer, monomorphism and epimorphism, and so on.
>> However exponential is always left alone. That is why I assumed it is
>> boring. If it is not boring, why is it never mentioned in textbooks
>> and lecture notes on category theory?
>
> In other words, these things are "idioms" or "naturally occurring
> things" in mathematics, but there is a gap in the obvious symmetries.
>
> Looking for gaps in symmetries is a good thing to do.  For example
> Dirac (whose biography by Graham Farmelo I have just started reading)
> predicted the positron this way.
>
> Actually, if we're looking at the categorical structure of the category
> of sets, it isn't very symmetrical at all.  The second edition of
> Paul Cohn's "Universal Algebra" was evidently influenced by Mac Lane's
> famous textbook, but illustrates how categorists had way overemphasised
> duality.
>
> For example the terminal object yields the classical notion of element
> or point, whereas the initial object is strict and boring.
>
> Products and coproducts of sets are very different.
>
> I explored this kind of thing in my book.   For example, the section
> on coproducts shows how different they are in sets/spaces and algebras.
>
> So David's question becomes a good one that deserves an answer if
> we read it as one about the phenomenology of mathematics rather than
> its technicalities.
>
> Paul Taylor
>
> PS There is a boring technical answer that I don't think anyone has
> mentioned, namely copowers, especially of modules.
>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Vaughan Pratt]

On 11/9/2011 7:58 AM, RJ Wood wrote:
  > Your observation about lack of symmetry in \set is underscored by the
  > fact that the yoneda functor for \set has a left adjoint which has
  > a left adjoint which has a left adjoint which has a left adjoint but
  > but the co-yoneda functor for \set has a right adjoint that fails to
  > preserve even finite sums.
  > R_j

Richard modestly omitted that he and our esteemed moderator showed
(necessarily by classical reasoning) that what Richard just said
characterized \set up to equivalence.

On 11/10/2011 1:29 AM, Prof. Peter Johnstone wrote:
> One point that no-one has mentioned yet is that you can't have
> exponentiation and its dual in the same category, unless it is a
> preorder.

Peter modestly omitted that he is the go-to category theorist when it
comes to toposes.

He also omitted that he was confining himself to cartesian closed
categories when he mentioned his point, understandable given that every
topos is cartesian closed.

To expand a little on my (1965) classmate Ross Street's counterexample
of Set^op, Set x Set^op is yet another counterexample.  Here I've
one-upped Ross (I must be getting competitive in my dotage) by
contradicting Peter and giving a counterexample in which both
exponentiation *and* dual exponentiation are present simultaneously.

How did I know that?  Well, Set x Set^op is equivalent (in fact
isomorphic) to Chu(Set, 1).  For *any* set K, both exponentiation and
dual exponentiation are admissible in Chu(Set,K), product being of the
tensor kind in this case.

How did I know *that*?  Well, every Chu category is a *-autonomous
category in the sense of Barr 1979.  If you don't know why every
*-autonomous category contains both exponentiation and dual
exponentiation, then like Ebert and Siskel I'm not going to give away
the plot and you'll just have to fork out to see the movie, or steal it
if you're a nerd, or watch this space (someone is bound to be a spoiler).

Open question.  At this year's CT, conveniently held 3 km from my
sister's house so I could bike in, I talked about TAC's, or
topoalgebraic categories.  These are defined by picking two sets of
objects from an arbitrary category (TAC's for dummies), some details of
which may be found at http://boole.stanford.edu/pub/sortprop.pdf .  (At
question time PTJ insightfully observed that TACs would cause immense
confusion if I submitted my write-up to TAC.)

A Chu category is precisely a dense complete TAC for which J and L are
singleton monoids.  That is, one sort and one property, both rigid.

The open question:  Characterize those dense complete TAC's admitting
both exponentiation and dual exponentiation.  Chu categories do so, but
what about others?

Many thanks to Ross, Richard, and Jeff Eggers for their respective roles
in the representation of TAC objects (A,r,X) over a profunctor K as a
profunctor morphism r: AX --> K.  (Ross and I would call them bimodules,
much as Mike Barr calls monads triples.)

But toposes are fun too.  *-autonomous categories are to Democrats as
toposes are to Republicans.

Vaughan (donkey) Pratt


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Robert Seely]

On Thu, 10 Nov 2011, Vaughan Pratt wrote:

> ...  Well, Set x Set^op is equivalent (in fact
> isomorphic) to Chu(Set, 1).  For *any* set K, both exponentiation and
> dual exponentiation are admissible in Chu(Set,K), product being of the
> tensor kind in this case.
>
> How did I know *that*?  Well, every Chu category is a *-autonomous
> category in the sense of Barr 1979.  If you don't know why every
> *-autonomous category contains both exponentiation and dual
> exponentiation, then like Ebert and Siskel I'm not going to give away
> the plot and you'll just have to fork out to see the movie, or steal it
> if you're a nerd, or watch this space (someone is bound to be a spoiler).

I hadn't intended to say this, but since Vaughan brought up
*-autonomous cats, here goes.  In Cockett-Seely "Proof theory for full
intuitionistic linear logic, bilinear logic, and MIX categories" (TAC
1997) we showed that bilinear logic, formulated with both exponentials
(ie suitable left adjoints to tensoring with an object) and dual
exponentials (ie suitable right adjoints to co-tensoring ("par'ing")
with an object), are just *-autonomous categories.  So not only do
*-autonomous cats have these two types of "internal homs" (4 operators
in all, in the non-symmetric case), but if (eg) a linearly
distributive category has them all, then it must be *-autonomous.  (In
the paper the result is a bit "finer", since we consider two variants
of bilinear logic, the Lambek-style one as above, and what we call
"Grishin categories", BILL and GILL in the paper.  Both amount to
different presentations of *-autonomous cats.)

So, in the non-Cartesian context, suitable duals to exponentials are
anything but boring ...

-= rags =-


-- 
<rags@math.mcgill.ca>
<www.math.mcgill.ca/rags>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Andrej Bauer]

> Also, in logic, "and" goes in pair with "or", "for all" goes in pair
> with "there exists". But implication is always left alone. Why is it
> so?

I am afraid logic is polyamorous:

1. "and" goes with "implies" because they are adjoint.
2. "and" goes with "or" because they are dual.

By the way:

1. "forall" goes with "weakening" because it is adjoint to it on the right.
2. "exists" goes with "weakening" because it is adjoint to it on the left.

But why is "forall" dual to "exists"?

With kind regards,

Andrej


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Jocelyn Ireson-Paine]

On Wed, 9 Nov 2011, Andrej Bauer wrote:

>> Also, in logic, "and" goes in pair with "or", "for all" goes in pair
>> with "there exists". But implication is always left alone. Why is it
>> so?
>
> I am afraid logic is polyamorous:
> ...
> By the way:
>
> 1. "forall" goes with "weakening" because it is adjoint to it on the right.
> 2. "exists" goes with "weakening" because it is adjoint to it on the left.
>
What's the definition of "weakening"? I've not seen this word used
formally.

> ...
> Andrej
>
Thanks
Jocelyn


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Vaughan Pratt]

On 11/9/2011 4:45 PM, Jocelyn Ireson-Paine wrote:
> What's the definition of "weakening"? I've not seen this word used
> formally.

I had the same question about "boring", which came earlier.  I believe
"sleeping" comes later, then "dreaming," "awakening," and so on.
Eventually the lecture ends and we either resume elsewhere with "boring"
or move on to "eating."

Vaughan


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Patrik Eklund]

Dear Vaughan,

An excellent remark, once again from your side.

The general audience of this remark may, however, not identify the
subtlety of these states with respect to modelling of parallel programs
and what apparently now happens on clouds and grids with services and
brokers, and not even to mention customers using these services.

So perhaps I may suggest to recall e.g. the dining philosophers
paradigm, which was widely used during the early days of CSP
(Communicating Sequential Processes) decades ago. The philosophers go
through only three states, namely, thinking, getting hungry (and thereby
stop thinking), and eating. After eating then go back to thinking, and so
on. They use chopsticks, one by one (in a very non-Asian fashion), and
communicate about using these resources with fellow philosophers around
the table. Simple objectives are e.g. to avoid starvation.

The relationship between states you mention is much more elaborate, they
overlap, and it is not entirely clear when one state is over, and another
one begins. I would even say that some of these states, in the sense of
being members of a "set of states", call for more structure in underlying
categories.

Perhaps you already thought about transforming this into a new paradigm. I
seriously think it would be a challence to the CSP programmers (some of
them fascinated e.g. by Goguen's institutions!) to encode some behaviour
involving those states in conventional CSP, and making the observation
that we may need additional language constructions, and more
underlying structures. The parallel paradigm is still all too
non-categorical.

Cheers,

Patrik



On Sat, 12 Nov 2011, Vaughan Pratt wrote:

>
> On 11/9/2011 4:45 PM, Jocelyn Ireson-Paine wrote:
>> What's the definition of "weakening"? I've not seen this word used
>> formally.
>
> I had the same question about "boring", which came earlier.  I believe
> "sleeping" comes later, then "dreaming," "awakening," and so on.
> Eventually the lecture ends and we either resume elsewhere with "boring"
> or move on to "eating."
>
> Vaughan

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Robert Dawson]

On 14/11/2011 9:36 AM, Patrik Eklund wrote:
> Dear Vaughan,
>
> An excellent remark, once again from your side.
>
> The general audience of this remark may, however, not identify the
> subtlety of these states with respect to modelling of parallel programs
> and what apparently now happens on clouds and grids with services and
> brokers, and not even to mention customers using these services.
>
> So perhaps I may suggest to recall e.g. the dining philosophers
> paradigm, which was widely used during the early days of CSP
> (Communicating Sequential Processes) decades ago. The philosophers go
> through only three states, namely, thinking, getting hungry (and thereby
> stop thinking), and eating. After eating then go back to thinking, and so
> on. They use chopsticks, one by one (in a very non-Asian fashion), and
> communicate about using these resources with fellow philosophers around
> the table. Simple objectives are e.g. to avoid starvation.

 	My recollection was that there were two versions - "dining
philosophers" who had shared access to two forks, either one of which
sufficed; and "dining Chinese philosophers" who had shared access to two
chopsticks of which both were needed.

 	But perhaps I have got it wrong?

 		Robert



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Robert Dawson]

On 16/11/2011 11:47 AM, Jeremy Gibbons wrote:
>
> On 15 Nov 2011, at 13:03, Robert Dawson wrote:
...
>> My recollection was that there were two versions - "dining
>> philosophers" who had shared access to two forks, either one of which
>> sufficed; and "dining Chinese philosophers" who had shared access to two
>> chopsticks of which both were needed.
>
> The dining philosophers need both forks/chopsticks. The point of the
> problem is the competing access to shared resources: how to manage the
> requests to avoid deadlock (eg by everyone picking up their left fork,
> and then blocking on waiting for the right fork).

       It seems to me there was a single fork version too in which the
(intentionally less difficult) problem occurred when the two  neighbours
of one philosopher picked up both the forks to which he had access; and
that the point of the chopsticks was to make one implement  useless.

 	Robert


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Peter Selinger]

David Leduc wrote:
>
> On Mon, Nov 7, 2011 at 07:59, Ross Street <ross.street@mq.edu.au> wrote:
>> The conjecture is false.
>> Take any category E where exponentiable is interesting.
>> Then the dual of exponentiable is not boring in E^op.
>
> Indeed! And this is clearly true of the example given by Thomas,
> namely Set^op.
>
> However, I am not yet satisfied. Let me precise my thoughts. In the
> textbooks and lecture notes on category category that I have read,
> there are always product and coproduct, pullback and pushout,
> equalizer and coequalizer, monomorphism and epimorphism, and so on.
> However exponential is always left alone. That is why I assumed it is
> boring. If it is not boring, why is it never mentioned in textbooks
> and lecture notes on category theory?

For what it's worth, I have seen such co-exponentials natually occur
in programming language semantics. They seem to occur in certain
extensions of lambda calculus. More specifically, in call-by-value
functional programming languages with call/cc style control
operators. When I say they occur "naturally", I mean that they exist
in such languages, not that they are typically used in any meaningful
way by programmers.

Very roughly speaking, in such languages, if A is a type, then (not A)
is the type of environments that can consume an element of type A and
then proceed with some task (called a "continuation" for A in
programming language lingo). A continuation for a function f : A -> B
is a pair of type A * (not B). In other words, an environment hoping
to interact with some function has to supply (1) an input to the
function, which is of type A, and (2) some task to complete after
receiving the output, i.e., something of type (not B).  It so happens
that in a call-by-value language with sufficient support for
continuations, there will be a one-to-one correspondence between
programs of type (A * not B) -> C and programs of type A -> B + C.

This is spelled out in long and very technical detail in my paper
"Control categories and duality" [1], sections 4.2 (definition of
co-control categories) and 7.3 (the call-by-value lambda-mu-calculus
is an internal language for co-control categories). The idea itself is
10 years older and is due to Andrzej Filinski [2], where
co-exponentials appear explicitly on p.33, second paragraph.

[1] http://www.mathstat.dal.ca/~selinger/papers.html#control
[2] http://www.diku.dk/hjemmesider/ansatte/andrzej/papers/DCaCD.ps.gz

-- Peter


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Michael Shulman]

Perhaps you are thinking of dualizing part of the notion of
exponential, but not the other part?

http://ncatlab.org/nlab/show/cocartesian+closed+category

Mike

On Sat, Nov 5, 2011 at 05:52, David Leduc <david.leduc6@googlemail.com> wrote:
> Dear all,
>
> I have a conjecture: the dual of exponential is boring in any
> category. Is there a counterexample to this conjecture? If not how can
> we prove it?
>

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The boringness of the dual of exponential

[Andrej Bauer]

>> 1. "forall" goes with "weakening" because it is adjoint to it on the
>> right.
>> 2. "exists" goes with "weakening" because it is adjoint to it on the left.
>>
> What's the definition of "weakening"? I've not seen this word used formally.

Weakening is the map Sub(A) -> Sub(A x B) which takes a subobject M
>-> A to the subobject M x B >-> A x B, i.e., it is pullback along the
projection pi1 : A x B -> A.

The existential quantifier over B is the left adjoint to weakening,
where Sub(A) and Sub(A x B) are viewed as posetal categories. The
universal quantifier is the right adjoint. Working out the details in
Set is instructive.

As far as I know the terminology comes from logic. The rule of
weakening says that a logical derivation may be "wakened" with an
additional (but unneeded) hypothesis:

Gamma |- A
----------------------
Gamma, H |- A

With kind regards,

Andrej


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]