April 2013 - Categories - categories.org.au

Partial functor
by David Leduc 17 Mar '15

17 Mar '15

Hi, A partial functor from C to D is given by a subcategory S of C and a functor from S to D. What is the appropriate notion of natural transformation between partial functors that would allow to turn small categories, partial functors and those "natural transformations" into a bicategory? The difficulty is that two partial functors from C to D might not have the same definition domain. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

7 6

Research positions
by Maria Manuel Clementino 26 Feb '14

26 Feb '14

5-YEAR RESEARCH POSITIONS The Centre for Mathematics of the University of Coimbra (CMUC) invites applications for five 5-year research positions in all areas of Mathematics. Applicants should have a PhD in Mathematics and at least three years of post-doctoral experience, with an international-level publication record and demonstrated ability to perform independent research. Preference will be given to candidates working in one of the areas in which the members of CMUC are currently active. A very good command of English is required. The appointments will be made for three years, renewable for two more. Successful applicants are expected to develop research within the areas of interest of CMUC. They should also contribute to graduate studies, supervising students from the Department of Mathematics. The basic salary is equivalent to the index 195 of the Portuguese research career (in the order of 42 500 euros a year), in accordance with the Ciência 2008 guidelines http://alfa.fct.mctes.pt/apoios/contratacaodoutorados/edital2008 Benefits include private health insurance and social security. Applicants should send • cover sheet (available from www.mat.uc.pt/cmuc/coversheet.pdf) including names and contact information of three persons who can provide a letter of recommendation • curriculum vitae (publication list included) • a 5-year research proposal (2 pages max), emphasizing their own research goals as pdf files to cmuc(a)mat.uc.pt. The subject of the e-mail message must include the job reference C2008 FCTUC CMUC v15-v19. The deadline for applications is *September 10, 2008.* ------------------------------ More information can be found at www.mat.uc.pt

1 1

separable locale
by Thomas Streicher 17 May '13

17 May '13

Recently rereading Fourman's "Continuous Truth" I came across the term "separable locale" but could nowhere find an explanation. Does it mean a cHa A for which there exists a countable subset B such that ever a in A is the supremum of those b in B with b leq a. This would be the point free account of "second countable", i.e. having a countable basis. Of course, second countable T_) spaces are separable, i.e. have a countable dense set. Is this reading the "usual" one? Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

5 4

Re: Terminology
by Thomas Streicher 03 May '13

03 May '13

Dear Jean, > What would you call a category X such that the functor X --> 1 is > full and faithful? Please don't tell me what they are, I know that. Sticking to the pattern I suggested I'd call it "essentially subterminal". > Non evil is essentially evil. > I rather like this conclusion, don't you? Of course, that's brilliant dialectics! I'd expect the people abhoring evilness would say that full and faithful and essentially surjective is an "evil" notion of equivalence as opposed to the "good" one of adjoint pair where unit and counit are isos. The latter makes sense in any 2-category whereas the former doesn't. However, often you just get the "evil" version when not having a strong form of AC (for classes) available. That's why your dialectics definitely applies! Best regards, Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

6 7

"Semantics of proofs and certified mathematics", IHP trimester, Paris, spring 2014: resgistration now open
by Pierre-Louis Curien 30 Apr '13

30 Apr '13

We are pleased to announce that registration is now open for the trimester "Semantics of proofs and certified mathematics" (previously announced on the categories list). Details are enclosed below. Pierre-Louis Curien, Hugo Herbelin, and Paul-André Melliès ********************** Dear colleague, It is our pleasure to announce a programme on "Semantics of proofs and certified mathematics" organised by the Centre Emile Borel of Henri Poincare Institute in Paris, from April 7th to July 11th, 2014. The organisers are Pierre-Louis Curien, Hugo Herbelin and Paul-Andre Mellies. Information on the programme can be found at : http://www.ihp.fr/en or at http://ihp2014.pps.univ-paris-diderot.fr/ Registration for the programme is free and recommended on: http://www.ihp.fr/en/program/10226/register BE CAREFUL : Deadline to apply for financial support is September 16th, 2013 During this trimester: - A summerschool at CIRM is organized from April 7th to April 18th, 2014: If you intend to participate in this event, it will be necessary to make a pre registration through this link: http://www.ihp.fr/en/program/10225/conference/register The number of participants to CIRM Summer School being limited, if necessary a selection among the applications will have to be made by the organisers. and - 5 workshops will take place: 1) « Formalization of mathematics in proof assistants » - May 5th to 9th (except Thursday, 8th- bank holiday) 2) « Constructive mathematics and models of type theory » - June 2th to 6th 3) « Semantics of proofs and programs » June 10th to 14th (Tuesday through Saturday- Monday, 9th-bank holiday) 4) « Abstraction and verification in semantics » June 23rd to 27th 5) « Certification of high-level and low-level programs » July 7th to 11th If you intend to participate to one or several of these events please register first to the whole programme. Registrations for these workshops will be opened later on. I will at that time send you a message informing you about it. We are looking forward to welcoming you in Paris! The poster of the trimester programme may be downloaded from the site http://ihp2014.pps.univ-paris-diderot.fr/ PS: do not hesitate to forward this e-mail to your colleagues and students. Sorry for multiple e-mails reception. -- Claire Bérenger CEB Program Coordinator Institut Henri Poincare 11 rue Pierre et Marie Curie 75005 Paris FRANCE Tel: 01 44 27 67 64 Fax: 01 44 07 09 37 **************************************** Chers Collègues, Nous avons le plaisir de vous annoncer l'organisation d'un programme sur la "Sémantique des preuves et des programmes et formalisation des mathématiques" au Centre Emile Borel (CEB) de l Institut Henri Poincaré de Paris, du 7 avril au 11 juillet 2014. Les organisateurs sont: Pierre-Louis Curien, Hugo Herbelin et Paul- Andre Mellies. Vous pouvez consulter le programme à l'adresse suivante: http://www.ihp.fr/fr ou directement à cette adresse: http://ihp2014.pps.univ-paris-diderot.fr/ L'inscription au programme est gratuite et cependant recommandée sur la page suivante: http://www.ihp.fr/fr/program/10225/register Attention : la date limite pour les demandes de support financier est fixée au 16 septembre 2013. Durant ce trimestre: - une école d été est organisée au CIRM (Marseille) du 7 au 18 avril 2014. Si vous avez l'intention de participer à ce programme en particulier une pré-inscription est nécessaire sur le site suivant: http://www.ihp.fr/fr/program/10225/conference/register Le nombre de participants à l'école d'été du CIRM etant limité, si necessaire une selection au vu des candidatures sera faite par les organisateurs scientifiques. et - 5 conferences auront lieu: 1) « Formalization of mathematics in proof assistants » - du 5 au 9 mai (à l exception du jeudi 8 mai- jour férié) 2) « Constructive mathematics and models of type theory » - du 2 au 6 juin 3) « Semantics of proofs and programs » June 10th to 14th (du mardi au samedi- Lundi 9 - jour férié) 4) « Abstraction and verification in semantics » du 23 au 27 juin 5) « Certification of high-level and low-level programs » du 7 au 11 juillet Si vous avez l'intention de participer à une ou plusieurs de ces conférences merci de vous inscrire dans un premier temps au programme dans son ensemble. Les conférences seront ouvertes aux inscriptions ultérieurement. Je vous en informerai par courriel. C'est avec plaisir que nous vous accueillerons a Paris! L'affiche du programme du trimestre peut être téléchargée depuis le site http://ihp2014.pps.univ-paris-diderot.fr/. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

John Reynolds
by Uday S Reddy 30 Apr '13

30 Apr '13

[Note from moderator: The following item appeared on the types list, and many categories readers will want to be made aware of this sad news.] Dear friends and colleagues, I am sorry to bring the sad news that John Reynolds, whose work and insights I have mentioned and recounted in my recent exchanges, has passed away on Sunday in Pittsburgh. John has not only done seminal work on a wide range of programming language topics, but he was also a guiding spirit and a great friend to many of us. We will dearly miss him. At this juncture, we might take a moment to reflect on his life time of accomplishment: http://www.cs.cmu.edu/~jcr/ Uday -- Prof. Uday Reddy Tel: +44 121 414 2740 Professor of Computer Science Fax: +44 121 414 4281 School of Computer Science Email: U.S.Reddy(a)cs.bham.ac.uk University of Birmingham Edgbaston Birmingham B15 2TT Web: http://www.cs.bham.ac.uk/~udr [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Terminology
by Thomas Streicher 29 Apr '13

29 Apr '13

In reply to David Roberts's message. Of course, category theorists do study weaker notions than equivalence in the 2-categorical sense and that's worthwhile to do. But it only makes sense when you still have a notion of equality of objects, i.e. a category in the ordinary sense of the word. If equality and (weak) equivalence were the same then one would not need to study model categories and/or related structures. Now it is certainly a fascinating extremist thought experiment to investigate logical systems where part of the structure they speak about is made invisible. This Martin Hofmann and I suggested when studying the groupoid model of type theory. There are nonstandard logical systems (intensional type theory) with a treatment of equality very different from the usual one. The main deviating feature is that ordinary replacement of equals is not valid anymore. Instead one always has to specify along which proof of equality one replaces. That's not convenient but necessary for keeping type checking decidable. But this inconvenience allows one to interpret this nonstandard equality as isomorphism in a category which does have equality of objects!. It is just that the formal system cannot speak about it. But ordinary equality is still required for interpreting judgemental equality! I don't know of any way to interpret type theory directly in a weak higher dimensional. It's always interpreted in a representing model category with its equality of objects. As the name says HoTT seems to be a fine ambience for doing synthetic homotopy theory. It is less clear for me how useful it is as a setting for developing category theory. I have made some experiments with the cases of indexed categories and monoidal categories which were disappointing. One might expect that you get coheence conditions for free or are at least forced to impose them. But this is not the case you just get a further level of generality not witnessed by interesting examples. I would be glad to see some positive uses of identifying equality and isomorphism when doing or at least formalizing category theory. According to my understanding what Jean wanted to say was that for getting enough equivalences you need choice for classes in order to find "quasi-inverses" to weak equivalences. This certainly is the situation when you reason about categories in ZF with a couple of Grothendieck universes. You need choice to identify strong and weak equivalence. It is presumably better (at least sometimes) to distinguish these notions. The situation is quite different when you use type theory with Univalence Axiom (UA) for speaking about categories. As always in type theory you have a kind of AC available because you interpret existential quantification as dependent sums. So one might think that everything's fine. But actually, since equality is interpreted in a deviating way if you write down isomorphism of types it turns out to mean weak equivalence (e.g. in the simplicial sets model). This means that what looks strong is actually very weak. But this is not a contradiction since existence and equality have very different meanings in these two settings. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Terminology
by Jean Bénabou 29 Apr '13

29 Apr '13

Dear Thomas, Dear all, My definition of poset is: "preordered set". I don't know if there is a general agreement, since some answers seemed to suppose that I meant "partially ordered set". It is because I feared this confusion that i specified by adding: equivalent to a discrete category. Of course I knew that they were "equivalence relations", and had also many other simple characterizations. One which I like and need is: X is equivalent to a discrete category iff the functor X --> 1 is faithful and conservative (i.e. reflects isos) because it has the following generalization: Let P: X --> S be a prefibration. The following are equivalent: (i) P is equivalent to a discrete fibration. (ii) P is faithful and consevative. (iii) each fiber of P is equivalent to a discrete category. Thus my question was not: what are such categories, for which I knew perfectly many answers, but : is there a well established name for them? Suggestions such as "setoids" or "essentially discrete" show that this is not the case. I don't like very much "setoids", and I am very tempted by "essentially discrete" as Thomas suggested. But I shall make my question a bit more difficult. What would you call a category X such that the functor X --> 1 is full and faithful? Please don't tell me what they are, I know that. I'm not even asking if there is a we'll established name for them. I don't think there is one. What I ask is: Could you suggest one? Preferably a name which would be suitable when we work with categories internal to a Topos E where supports don't split. As a side remark, let me say that I don't care very much for the distinction between "evil" and "non evil". Apart from obvious moral or philosophical reasons, for the following purely mathematical one: Non-evilness depends on the notion of equivalence of categories. And this in turn may heavily depend on which notion of equivalence you chose. And some of these notions depend on the axiom of choice, which I might be tempted to call "evil". Thus we'd reach the following conclusion: Non evil is essentially evil. I rather like this conclusion, don't you? Best regards, Jean Le 27 avr. 2013 à 15:08, Thomas Streicher a écrit : > Dear Jean, > a > >> As many of you I presume, I have for ages, and very often, had to deal with categories which are both groupoïds and posets, or again which are equivalent to a discrete category. Is there a well established name for them? > > What about "essentially discrete" like in "essentially small" or > "essentially surjective". Generally, for any property P of categories > I would say a category is "essentially P" if it is equivalent to a > category with property P. > So "essentially" is a kind of magic word transforming "evil" properties > into "non-evil" ones. (I don't think one should always do this!) > > Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1

European Master's Program in Computational Logic
by Bertram Fronhöfer 29 Apr '13

29 Apr '13

Dear all, Please spread this information as wide as possible among friends and colleagues, at your old universities and the places, where you currently live and work. Many thanks -- Steffen ******************************************************************************************************* The European Master's Program in Computational Logic We are glad to announce to you the possibility to join our European Master's Program of Computational Logic. This program is offered jointly at the Free-University of Bozen-Bolzano in Italy, the Technische Universit?t Dresden in Germany, the Universidade Nova de Lisboa in Portugal and the Technische Universit?t Wien in Austria. Within this program you have the choice to study at two /three of the four European universities. In addition you can do your project work at the National ICT of Australia (NICTA). You will graduate with a MSc in Computer Science and obtain a multiple degree. Information on the universities and the program is provided here: http://www.emcl-study.eu/home.html Language of instruction is English. Tuition fees are 3.000 EUR (for non-European students) and 1.000 (for European students) per year. The ERASMUS-MUNDUS consortium offers tuition fee waivers and small grants (http://www.emcl-study.eu/grants.html) More information on the application procedure is available from: http://www.emcl-study.eu/application.html Application deadline is 31 May, applicants must use our online application system. Do not hesitate to contact us again if you have any further questions. Kind regards -- Steffen H?lldobler Prof. Dr. Steffen Hoelldobler International Center for Computational Logic Technische Universit?t Dresden 01062 Dresden, Germany phone: [+49](351)46 33 83 40 fax: [+49](351)46 33 83 42 email: sh(a)iccl.tu-dresden.de [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

categories of Categories
by Dr. Keith G. Bowden 28 Apr '13

28 Apr '13

Dear All, I remember once seeing a Venn diagram of overlapping categories of Categories, such as Abelian Cats, Cartesian Closed cats, Topoi, Concrete Cats, etc etc. Can anyone remind me where it was, or point me to something similar (preferably on the web). Thanks, Keith Bowden [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0