gmane.science.mathematics.categories

Re: a historical question

Tierney, Myles — 2013-06-17T21:40:17

Dear Eduardo,

This is Cartier's Bourbaki Seminar talk
of February 1978 on the work of
Lawvere and Tierney.


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

Re: a historical question

Eduardo J. Dubuc — 2013-06-17T13:55:00

There is a Cartier's exposition on the work of Lawvere.

e.d.


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

Re: a historical question

Valeria de Paiva — 2013-06-17T13:18:03

Thank you Prof Benabou for the personal evidence and thank you Urs
Schreiber and Thomas Streicher for the document!!! Really glad to see that
the Seminaire Bourbaki is online and surprised that I couldn't find it
yesterday.
best,
Valeria

On Mon, Jun 17, 2013 at 12:32 AM, Urs Schreiber <
urs.schreiber< at >googlemail.com> wrote:


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

Re: a historical question

Jean Bénabou — 2013-06-17T07:43:04

The only talk related to the subject that Cartier gave at Bourbaki (not a very good one if I may say so since I was present) was about Lawvere- Tierney's  elementary toposes with a brief mention of the fact that they had something to do with intuitionist logic. 





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

Re: a historical question

Urs Schreiber — 2013-06-17T07:32:26

I suppose this is referring to

Pierre Cartier,
"Logique, catégories et faisceaux",
Séminaire Bourbaki, 20 (1977-1978), Exp. No. 513, 24 p.
http://www.numdam.org/item?id=SB_1977-1978__20__123_0



On 6/16/13, Valeria de Paiva <valeria.depaiva< at >gmail.com> wrote:


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

Category Theory 2013 - final call

Richard Garner — 2013-06-17T04:07:21

Dear Category Theorists,

This is a final announcement for the conference CT2013 which will be
taking place in Sydney next month. The deadline for registrations is
21st June, this Friday; if you are planning to attend, but, for
whatever reason, are unable to register by this deadline, could you
please send me an email confirming your intentions.

The conference will be held at Macquarie University from 7-13 July,
and the invited speakers are
         Eugenia Cheng (Sheffield)
         Pieter Hofstra (Ottawa)
         Zurab Janelidze (Stellenbosch)
         Emily Riehl (Harvard)
         Mike Shulman (IAS)
         Ross Street (Macquarie).

There will also be a workshop on Applications of Category Theory taking
place the week before the conference, with lectures by
         Marcelo Aguiar (Texas A&M)
         Richard Garner (Macquarie)
         Scott Morrison (Australian National University)
         Mike Shulman (IAS).

More information about both conference and workshop can be found at
the conference website.

http://web.science.mq.edu.au/groups/coact/seminar/ct2013/

Best wishes,

Richard Garner (for the organizing committee).


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

a historical question

Valeria de Paiva — 2013-06-16T01:08:43

Hi,
I know no one should pay too much attention to what Wikipedia says, but I
wonder if anyone can give me a proper reference for:
"Cartier was to give a Séminaire
Bourbaki<http://en.wikipedia.org/wiki/S%C3%A9minaire_Bourbaki>exposition
of intuitionistic logic."
This is in the Wikipedia entry for Categorical Logic
http://en.wikipedia.org/wiki/Categorical_logic
and as anything that is in Wikipedia is repeated lots of  times, all over
the web.
Does anyone know what this sentence is referring to, please?
Thanks
Valeria

Re: More publicity

David Yetter — 2013-06-13T17:55:48

I'm pleased to see the items quoted from Coecke include "string diagrams" as they are now called.

Although they occur first in Kelly and Laplaza's paper on coherence for compact closed categories, and again
in Street's work with Joyal in the mid-80's, I think I was the first person to use them, in public at least, in the form
with "coupons" (to borrow the term Reshtikhin and Turaev used a few months later) to represent maps
which aren't inherent in the (braided or symmetric compact closed) monoidal structure.

Best Thoughts,
David Y.


On 12 Jun 2013, at 03:41, Ross Street wrote:




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

Re: Publicity

Tom Hirschowitz — 2013-06-13T09:07:00

Dear Steve,

Nice metaphor!

But I'm afraid my point carries over to the new setting, as:

Category-land looks wild and scary from the surrounding fortresses, so
maybe we should be softer towards people trying to make it look
attractive, open, and, above all, safe.

I'll stop bugging the list with this all now, sorry for the noise.
Tom

On 06/13/2013 09:25 AM, Steve Vickers wrote:


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

Re: Publicity

Steve Vickers — 2013-06-13T07:25:15

Dear Tom,

That's the wrong way to look at it. Category-land is really the land _between_ the fortresses. The courage to enter Category-land is the courage to leave the supposed protection of the city walls.

I was lucky enough to do my PhD in a region (Ringland) where they were already getting used to life without having those walls, but for for many of the city dwellers the idea that maths has anything to do with categories is as alien as the idea that milk comes from cows.

Steve.


On 11 Jun 2013, at 13:40, Tom Hirschowitz <tom.hirschowitz< at >univ-savoie.fr> wrote:



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

BOUNCE categories< at >mta.ca: Approval required: (fwd)

Bob Rosebrugh — 2013-06-13T16:00:04

Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes
To: "Marta Bunge" <martabunge< at >hotmail.com>, categories< at >mta.ca, "Tom Hirschowitz" <tom.hirschowitz< at >univ-savoie.fr>
Subject: Re: Publicity
References: <E1UiTcE-000296-Qy< at >mlist.mta.ca>
Date: Thu, 13 Jun 2013 09:40:34 +0300
MIME-Version: 1.0
Content-Transfer-Encoding: Quoted-Printable
From: "Revence Kalibwani" <revence< at >1st.ug>
Message-ID: <op.wylt5wui52s4kz< at >fardeau.ds.co.ug>
In-Reply-To: <E1Umw4g-00036s-IV< at >mlist.mta.ca>

Speaking as one who hated mathematics consistently in school, and then  =

came to be deeply intrigued by category theory (because I have a  =

probably-pathological obsession with corollaries), I am forced to concur=
   =

with Tom. I=E2=80=99ll never be a professional mathematician, but someth=
ing about  =

basic category theory just sounds so human. Analogies, homologies,  =

similarities, memories =E2=80=A6 these are the things our minds process =
every time  =

we look at a face, and category theory says =E2=80=9CI can help you draw=
  a bunch  =

of squiggly stuff for that.=E2=80=9D What=E2=80=99s not to love?

=CE=A4=CE=B7=CE=BD Tue, 11 Jun 2013 15:40:33 +0300,=CE=BF(=CE=B7) Tom Hi=
rschowitz  =

<tom.hirschowitz< at >univ-savoie.fr> =CE=AD=CE=B3=CF=81=CE=B1=CF=88=CE=B5:

h


e

as

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

More publicity

Ross Street — 2013-06-12T08:41:08

Okay, how about this then?

http://blogs.scientificamerican.com/guest-blog/2013/05/16/quantum-mechanical-words-and-mathematical-organisms/

==Ross

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

CFP Post-proceedings TYPES 2013 Types for Proofs and Programs (open call)

Ralph Matthes — 2013-06-12T15:11:14

Call for papers: Types for Proofs and Programs,
    post-proceedings of TYPES 2013 (open call)
----------------------------------------------

TYPES is a major forum for the presentation of research on all aspects
of type theory and its applications. The post-proceedings of TYPES
2013, which was held in Toulouse, are open to everyone, also those who
did not participate in the conference. We would like to invite all
researchers that study type systems to share their results concerning
type-based theorem proving environments or type-based formal modelling, in
particular we welcome submissions on any topic in the following list:

   - Foundations of type theory and constructive mathematics.
   - Applications of type theory.
   - Dependently-typed programming.
   - Industrial uses of type theory technology.
   - Meta-theoretic studies of type systems.
   - Proof-assistants and proof technology.
   - Formalisation of proofs in type theory.
   - Extraction of implementations from proofs.
   - Automation in computer-assisted reasoning.
   - Links between type theory and functional programming.
   - Links between type theory and object-oriented programming.
   - Type theory in linguistics.


Important dates
---------------

Abstract submission deadline:  2013-09-09
Paper submission deadline:     2013-09-16
Notification of acceptance:    2014-02-17

Details
-------

* Papers must be submitted in PDF format using EasyChair:
    https://www.easychair.org/conferences/?conf=types13postproceedin

* Authors have the option to include an attachment (.zip or .tgz)
    containing mechanised proofs, but reviewers are not obliged to take
    these attachments into account. Attachments will not be published
    together with the papers.

* The post-proceedings will be published in LIPIcs (Leibniz
    International Proceedings in Informatics,
    http://www.dagstuhl.de/en/publications/lipics), an open-access series
    of conference proceedings.

* Authors of accepted papers retain copyright, but are expected to sign
    an author agreement with Schloss Dagstuhl?Leibniz-Zentrum f?r
    Informatik, see
    http://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/.

* For information about how to prepare submissions, see
    http://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/.
    In general, please refer to the dedicated web site
    http://www.irit.fr/TYPES2013/Postproceedings.html
    for more detailed/specific information.

* We recommend to keep the length of the contributions in the range of
    15-25 pages, and 25 pages is the upper limit for the submissions.

* In case of questions, please contact one of the editors.

Editors
-------

Ralph Matthes           IRIT (CNRS and University of Toulouse), France
Aleksy Schubert         University of Warsaw, Poland



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

Re: Publicity

Tom Hirschowitz — 2013-06-11T12:40:33

Dear Marta,

Thanks very much for your detailed answer.

First, I agree with you that it is wrong to equate category theory with
logic and computation. I don't know whose mistake this is, but it
certainly is one.

However, it seems to me that people may be led to category theory, or
more generally any interesting subject matter, for bad reasons --- and
that this is sometimes good. (*)

Category-land, as Jean B?nabou calls it, may look like a fortress from
the outside. So maybe we should be softer towards people trying to make
it look attractive and open.

What do you think?

Best wishes,
Tom

(*) It was John Baez, `making a fool of himself' as usual, who made me
think I could enter the fortress back in 2006. I'll probably never be as
fluent as native category theorists, but I nevertheless think my
research has improved since then.




On 06/08/2013 11:39 AM, Marta Bunge wrote:


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

An adjoint functor theorem

Michael Barr — 2013-06-10T21:40:27

We have discovered an adjoint functor theorem that generalizes SAFT and
very nearly generalizes GAFT and I wonder if it has been noted before.

   \thm Suppose \Bsc is a wide complete category and $U:\Bsc\to\Csc$ is a
wide-limit-preserving functor.  Suppose $\Asc\inc\Bsc$ is a subcategory
that cogenerates \Bsc.  Suppose for each object $C\in\Csc$, the comma
category $(C,U|\Asc)$ has a weak initial set.  Then $U$ has a left
adjoint $F$.\eth

Michael

position at Nijmegen

Ieke Moerdijk — 2013-06-10T09:37:03

Dear readers of the categories list,

Radboud University at Nijmegen (The Netherlands) is advertising
for a tenure track position in mathematics at the assistant professor
level.
The position will initially be partially financed by the NWO funded cluster
"Geometry and Quantum Theory".

The ad can be found at

<http://www.ru.nl/vacatures/details/details_vacature_0?recid=527849>

while information about the cluster is at

<http://www.gqt.nl/>

The topology group here is rather categorically inclined. You can get an
impression at

<http://www.math.ru.nl/topology/>


Ieke Moerdijk


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

Re: Publicity

Patrik Eklund — 2013-06-10T07:53:17

These discussions on trinity and similar seem to raise only irritation
where there would be opportunity to provide constructive discussions.

CT has done a good job in explaining and providing rigour. Some like it,
some don't. Type theory is a typical example where computer science is "on
its own", unless trying to understand trinity like suggestions. Take
'lambda', for instance. Church said already back in 1940 that 'lambda' is
an "improper symbol" and that his 'o' type for something in direction of
propositions, but Church says:

"We purposely refrain from making more definite the nature of the types o
and iota" (peklund: the 'type' type!) ", the formal theory admitting of a
variety of interpretations in this regard. Of course the matter of
interpretation is in any case irrelevant to the abstract construction of
the theory, and indeed other and quite different interpretations are
possible (formal consistency assumed)."

'Trinity' also raises irritation and even fear as it refers to the Holy
Trinitiy, and many feel very uncomfortable even talking about these
things.

The wordpress blog mentioned is also very shallow in its introduction,
just mentioning "manifest in three persons". Some may be interested to
look more into the relation of "the three" as it has been part of history
and e.g. the split of the Latin and Greek Churches. The so called Filioque
addition and why it happened, and how it appears in the Latin language is
far beyond just saying "manifests". The way Augustinus opposed Arianism
and his choices of 'language' is, I think, a bit interesting in this
context. Or maybe not.

Rigour to me is just being clear about what is what. For instance,
sentences build upon terms, and satisfaction/entailment needs sentences.
This shold mean we need to be precise about terms, and then closing that
door. Then we are precise about sentences, and closing that door, and so
on. We should somewhere along that path, e.g. after having closed the
"sentences door", come up with new and nice sentences still to be used.
G?del was doing that all the time.

We shouldn't, I think, allow "circadian rhythms" into science and
mathematics, in particular in type theory concerning how types and
propositions are "manifested" in each other.

Cheers,

Patrik



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

Re: Publicity

Fred E.J. Linton — 2013-06-08T21:13:54

Vaughan Pratt <pratt< at >cs.stanford.edu> suggested:


In my estimation, the "rigor" in Rehmeyer's adjective "rigorous" and
the "rigor" in Spivak's quote have about as little to do with each other
as either has to do with the one in the phrase "rigor mortis" :-) . 

Cheers, -- Fred



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

Re: Publicity

Urs Schreiber — 2013-06-08T20:30:02


The term "computational trinitarianism"

   http://ncatlab.org/nlab/show/computational+trinitarianism

refers to the theorem relating category theory and type theory

   http://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory

The further relation between type theory to logic and programming
languages is similarly well established. The term "computational
trinitarianism" was invented by Bob Harper in an expositional blog
post

  http://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/

designed to alert an unspecialized public about these nice and useful
facts. I guess that's what the author of that article about Spivak's
paper picked up.


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

Re: Publicity

Jeremy Gibbons — 2013-06-08T20:09:21

On 8 Jun 2013, at 10:39, Marta Bunge wrote:


Don't blame Rehmayer for the "computational trinitarianism" line; that's Bob Harper's invention, tongue in cheek. 

But I don't think Harper is to blame for equating CT with PL and logic. He does say


   http://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/

All I take him to mean is that logic, languages, and categories offer three complementary perspectives on computation. I don't think you can read this as "computation subsumes category theory".

Jeremy

Jeremy.Gibbons< at >cs.ox.ac.uk
Oxford University Department of Computer Science,
Wolfson Building, Parks Road, Oxford OX1 3QD, UK.
+44 1865 283521
http://www.cs.ox.ac.uk/people/jeremy.gibbons/



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

Conference in Memory of Aurelio Carboni - Second Announcement.

2013-06-08T13:23:07

This is the second announcement for the Conference in Memory of
Aurelio Carboni.

The meeting will be held in Milano, June 24 - 26 2013, at the
Department of Mathematics "Federigo Enriques" (Universit?? degli Studi).

Invited speakers are


      Dominique Bourn (Universit?? du Littoral, Calais, F)
      Marino Gran (Universit?? catholique de Louvain, Be)
      Marco Grandis (Universit?? degli Studi di Genova, I)
      George Janelidze (University of Cape Town, ZA)
      Peter T. Johnstone (University of Cambridge, UK)
      William F. Lawvere (University at Buffalo, US)
      Giuseppe Rosolini (Universit?? degli Studi di Genova, I)
      Enrico M. Vitale (Universit?? catholique de Louvain, Be)
      Robert F. C. Walters (Universit?? degli Studi dell'Insubria, I)
      Richard Wood (Dalhousie University, Ca)


Here follows the conference program.


*Monday 24*

13:30 - 14:40  Registration.
14:30 - 14:45  Opening - Silvio Ghilardi (Head of the Dept.)
14:45 - 15:45  "The mathematical heritage of Aurelio Carboni" - Bill
Lawvere and George Janelidze.

15:45 - 16:15  coffee break

16:15 - 17:15  "The Snail Lemma" - Enrico M. Vitale
17:15 - 18:15  "Racks and Tangled Circuits" - Bob Walters


*Tuesday 25*

9:00 - 10:00  "Mal'cev categories vs protomodular categories" -
Dominique Bourn
10:00 - 11:00  "Monotone-light factorisation systems and torsion
theories" - Marino Gran

11:00 - 11:30  coffee break

11:30 - 12:30  "Projective and affine aspects in categories" - Marco Grandis

15:00 - 16:00  "Towards axiomatic description of categories of
commutative algebras" - George Janelidze

16:00 - 16:30  coffee break

16:30 - 17:30  T.B.A. - Pino Rosolini

          20:00  Conference Dinner


*Wednesday 26*

9:00 - 10:00  "The geometry (?) of realizability toposes" - Peter T. Johnstone
10:00 - 11:00  "The waves of a total category and total
distributivity" - Richard Wood

11:00 - 11:30  coffee break

11:30 - 12:30  "Syntactical Presentations of Objective Abstract
Generals and Axiomatizability, Distributors and Distributions" - Bill
Lawvere




More information about the conference, including the abstracts of the
talks, is available at the following url:


http://math.unipa.it/metere/Aurelio2013/index.html



The conference has no registration fee, and people wishing to
partecipate are strongly encouraged to  register as soon as possible e
in any case within June  15, 2013,  by sending an Email to
sandra.mantovani< at >unimi.it or giuseppe.metere< at >unipa.it.

We hope to see you here soon.


The organizers:

Silvio Ghilardi (Universit?? degli Studi di Milano), Sandra Mantovani
(Universit?? degli Studi di Milano), Giuseppe Metere (Universit?? degli
Studi di Palermo), Robert F.C. Walters (Universit?? degli Studi
dell'Insubria).








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