July 2019 - Categories - categories.org.au

Re: "First" use of 'Category theory' to describe our field
by David Roberts 23 Feb '24

23 Feb '24

Dear Ross, no, that's pretty good! It's mildly surprising that it took ~20 years for the name to 'stick', but maybe less so given that the field grew slowly to start. Thanks, David David Roberts Webpage: https://ncatlab.org/nlab/show/David+Roberts Blog: https://thehighergeometer.wordpress.com On Thu, 11 Jul 2019 at 08:21, Ross Street <ross.street(a)mq.edu.au> wrote: > > Dear David > > From memory, the Pure Mathematics Honours (USyd) course that Max Kelly taught in 1965 > was called ``Category Theory''. It concentrated on different kinds of morphisms > and factorizations in a category, and finished with adjoint functors. > Also John Gray's (UIllinois) 1968-69 graduate course had that name. > > From Eilenberg I heard that each person using categories should have their own category of expertise. > I told this to John Gray who said that was fine; the time had come for that category to be Cat. > > I would suggest that the first category theorists to think of themselves as such were Eilenberg's students at Columbia. > However, Mac Lane was definitely a category theorist. > > This is probably not the verifiable stuff you were seeking. > > Ross > > > On 10 Jul 2019, at 10:01 PM, David Roberts <droberts.65537(a)gmail.com> wrote: > > Hi all, > > the (idle) question is: when did the phrase 'category theory' catch on > for the field? Clearly it didn't leap from either of the heads of > Eilenberg or Mac Lane full-grown, since they used the phrase 'General > theory of natural equivalences'. There are the old 'Reports of the > Midwest Category Seminar' lecture notes (the first in 1967), which > hints that 'category theory' wasn't quite the name in use. > > Even more interesting: who was the first "category theorist", by that name? > > Answers referring to verifiable sources would be best. > > Thoughts? > > David > > > > David Roberts > Webpage: https://ncatlab.org/nlab/show/David+Roberts > Blog: https://thehighergeometer.wordpress.com > [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

3 4

Postdoc at the University of Leeds
by Nicola Gambino 31 Jul '19

31 Jul '19

Dear friends and colleagues, The School of Mathematics of the University of Leeds is inviting applications for a fixed-term Research Fellowship in Pure Mathematics, to work on homotopy type theory and its connections to higher category theory. Please see the web page https://jobs.leeds.ac.uk/vacancy.aspx?ref=MAPMA1114 for details. The deadline for applications is Tuesday 27th August. This is a fixed-term position until 31st August 2020, with a possibility of extension for up to 12 months of employment in total (subject to approval by the funding body). Please feel free to email me at n.gambino(a)leeds.ac.uk if you have any queries. With best regards, Nicola Gambino = Dr Nicola Gambino School of Mathematics, University of Leeds [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

constructive Brouwer fixed point theorem
by Paul Taylor 29 Jul '19

29 Jul '19

Constructive Brouwer fixed point theorem I would like some help from a homotopy theorist who is fluent in the low-level old-fashioned techniques of the subject such as dividing up polyhedra but who is not frightened by the word "constructive". In particular I would like to know whether there is a name or some theory for a certain kind of higher connectiveness. Of course I would also like to know whether anyone has already proved the result that I sketch below, since it does seem rather a natural one. The Intermediate Value Theorem and Brouwer's Fixed Point Theorem, as usually presented, are non-constructive because the proofs assume that equality in R is decidable, ie you can do one thing if a=b and another if a<b or a>b. The counterexample for the IVT is a function that rises to a "shelf", where it "hovers" for a bit and then rises again, where the height of the shelf is a value a for which we don't know whether a=0, a<0 or a>0 and therefore whether the zero is at the right or left end of the shelf. There are constructive versions of both results that find places where the function is zero/fixed within epsilon, without restricting the (continuous) function. However, my interest is in identifying the appropriate restriction on the function to obtain "exact" results. Other constructivity questions may also be raised, such as the use of Dependent Choice and the "finite open sub-cover" definition of compactness, but I do not believe that there is any interesting theorem without these. For the IVT, the condition on the function is that, in any inhabited open interval, there is some point where it is nonzero/nonfixed. The Brouwer fixed point theorem has a counterexample in 2D: there is a computable endofunction of the square all of whose fixed points have one or other coordinate non-computable. Topologically, these fixed points form a rectangular grid, so that the subspace of non-fixed points is highly disconnected. Returning to the theorem, there is a well known proof based on Sperner's Lemma, which is about sub-dividing simplices. This proof is non-constructive because it assumes at the outset that the function is non-fixed EVERYWHERE. However, what is actually needed to make the proof work is to be able to construct the sub-division in such a way that the function be non-fixed on the (n-1)-skeleton. Therefore the condition on the function that we need to prove the theorem and avoid the counterexample is a certain higher connectedness of the (open) subspace of nonfixed points: Any filled-in (n-1)-simplex such that the function is non-fixed on its (n-2)-boundary is homotopic (within any neighbourhood) to a filled-in (n-1)-simplex with the same (n-2)-boundary such that the function is non-fixed throughout. This condition is a variant on (n-1)-connectedness, but is not the same as LOCAL (n-1)-connectedness and I do not know a name for it. Recall that a space U is k-connected if for each h <= k, every continuous map s : S^h -> U is contractible (to a point). This can be said more abstractly in the form that all of the homotopy groups pi_n(U) are trivial, but we need a more concrete form: any hollow k-simplex in U may be filled in within U. I have a sketch proof of the Brouwer fixed point theorem based on this hypotheses. However, a lot of infrastructure about sub-dividing polyhedra is needed, but this is not my subject and I am not familiar with it. Besides, there is no point on working on this if someone else has already done it. Also, my real interest is not in the fixed point theorem itself but in the Sperner proof as an example of the notion of an OVERT SUBSPACE. References: For an introduction to overtness using the IVT as an example, see my paper "A Lambda Calculus for Real Analysis" Journal of Logic and Analysis, 2 (2010) 1-115. www.paultaylor.eu/ASD/lamcra This 3-page lecture note by Jacob Fox (formerly of MIT, now Stanford) contains - a neat combinatorial proof of Sperner's Lemma and - its application to the classical Brouwer Fix Point Theorem: - but not actually the manner of sub-dividing simplices. math.mit.edu/~fox/MAT307-lecture03.pdf I don't recall the details of the counterexample in 2D, which is due to G\"unter Baigger, but Petrus Potgieter sketched it for me when I went to Pretoria in 2006 and in the paper below: G\"unter Baigger, Die Nichtkonstruktivit\"at des Brouwerschen Fixpunktsatzes, Arch. Math. Log., 1985 Petrus Potgieter, Computable counter-examples to the Brouwer fixed-point theorem, arxiv.org/abs/0804.3199 Paul Taylor [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

ETAPS 2020 1st joint call for papers
by Tarmo Uustalu 29 Jul '19

29 Jul '19

****************************************************************** JOINT CALL FOR PAPERS 23rd European Joint Conferences on Theory and Practice of Software ETAPS 2020 Dublin, Ireland, 25-30 April 2020 http://www.etaps.org/2020 ****************************************************************** -- ABOUT ETAPS -- ETAPS is the primary European forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of four annual conferences, accompanied by satellite workshops. ETAPS 2020 is the twenty-third event in the series. -- MAIN CONFERENCES (27-30 April) -- * ESOP: European Symposium on Programming (PC chair: Peter Müller, ETH Zürich, Switzerland) * FASE: Fundamental Approaches to Software Engineering (PC chairs: Heike Wehrheim, Universität Paderborn, Germany, and Jordi Cabot, Universitat Oberta de Catalunya, Spain) * FoSSaCS: Foundations of Software Science and Computation Structures (PC chairs: Barbara König, Univ Duisburg-Essen, Germany, and Jean Goubault-Larrecq, LSV, ENS Paris-Saclay, France) * TACAS: Tools and Algorithms for the Construction and Analysis of Systems (PC chairs: Armin Biere, Johannes-Kepler-Univ Linz, Austria, and David Parker, University of Birmingham, United Kingdom) TACAS '20 will host the 9th Competition on Software Verification (SV-COMP). POST, which was an ETAPS conference 2012-2019, has been discontinued. -- INVITED SPEAKERS -- * Unifying speakers: Lars Birkedal (Aarhus Universitet, Denmark) Jane Hillston (University of Edinburgh, United Kingdom) * ESOP invited speaker: Isil Dillig (University of Texas at Austin, USA) * FASE invited speaker: Willem Visser (Stellenbosch University, South Africa) -- IMPORTANT DATES * Papers due: 24 October 2019 23:59 AoE (=GMT-12) * Rebuttal (ESOP, FoSSaCS and, for selected papers, TACAS): 9 December 00:01 AoE - 10 December 23:59 AoE * Notification: 23 December 2019 * Camera-ready versions due: 22 February 2020 -- SUBMISSION INSTRUCTIONS -- The four main conferences of ETAPS 2020 solicit contributions of the following types: * ESOP: regular research papers of max 25 pp (excl bibl) * FASE: regular research papers and empirical evaluation papers of max 18 pp (excl bibl), tool demonstration papers of 6+6 pp * FoSSaCS: regular research papers of max 18 pp (excl bibl) * TACAS: regular research papers, case study papers and regular tool papers of max 16 pp (excl bibl), tool demonstration papers of 6 pp For definitions of the different paper types and specific instructions, where they are present, see the webpages of the individual conferences. All accepted papers will appear in the conference proceedings and have presentations during the conference. A condition of submission is that, if the submission is accepted, one of the authors attends the conference to give the presentation. Submitted papers must be in English presenting original research. They must be unpublished and not submitted for publication elsewhere. In particular, simultaneous submission of the same contribution to multiple ETAPS conferences is forbidden. Submissions must follow the formatting guidelines of Springer's LNCS and be submitted electronically in pdf through the Easychair author interface of the respective conference. Submissions not adhering to the specified format and length may be rejected immediately. FASE will use double-blind reviewing. Authors are asked to omit their names and institutions; refer to own prior work in the third person; not to include acknowledgements that might identify them. Regular tool paper and tool demonstration paper submissions to TACAS must be accompanied by an artifact. The artifact will be evaluated and the outcome will be taken into account in the acceptance decision of the paper. ESOP and FoSSaCS will use an author rebuttal phase. TACAS will have rebuttal for selected papers. -- PUBLICATION The proceedings will be published in the Advanced Research in Computing and Software Science (ARCoSS) subline of Springer's LNCS series. The proceedings volumes will appear in gold open access, so the published versions of all papers will be available for everyone to download from the publisher's website freely, from the date of online publication, perpetually. The copyright of the papers wiil remain with the authors. -- SATELLITE EVENTS (25-26 April) -- A number of satellite workshops will take place before the main conferences. * 25-26 April (two days): CMCS, GALOP, SynCoP, VerifyThis, VPT, WADT, WRLA * 25 April: CREST, InterAVT, MSFP, TEASE-LP * 26 April: HCVS, MARS, MeTRiD, PLACES, RW -- CITY AND HOST INSTITUTION -- Dublin (Baile Átha Cliath) is the capital and largest city of the Republic of Ireland. It is situated on the East coast of Ireland, at the mouth of the River Liffey, at the centre of the Greater Dublin area with 1.9 million inhabitants. Dublin is a historical and contemporary centre for education, the arts, administration and industry. As of 2018 the city was listed by the Globalization and World Cities Research Network (GaWC) as a global city, with a ranking of Alpha-, which places it among the top thirty cities in the world. ETAPS 2020 is organised by the University of Limerick in cooperation with Lero, the Irish Software Research Centre spanning 9 Universities and ITs in the Republic of Ireland. -- ORGANIZERS -- General chair: Tiziana Margaria (University of Limerick and Lero, Ireland) Workshop chairs: Falk Howar (Technische Universität Dortmund, Germany) and Peter Höfner (Data61, Australia) Practical organization: Easy Conferences -- FURTHER INFORMATION -- Please do not hesitate to contact the general chair at <tiziana.margaria(a)lero.ie>. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

RAMiCS2020 - 2nd CFP
by Michael Winter 26 Jul '19

26 Jul '19

2nd CALL FOR PAPERS 18th International Conference on Relational and Algebraic Methods in Computer Science RAMiCS 2020 08. April to 11. April 2020, Palaiseau, France URL: http://ramics18.gforge.inria.fr/ IMPORTANT DATES: Abstract Submission: 06. October 2019 Paper Submission: 13. October 2019 Author Notification: 15. December 2019 Final Version: 16. January 2020 RAMiCS 2020: 08. April to 11. April 2020 GENERAL INFORMATION: Since 1994, the RAMiCS conference series has been the main venue for research on relation algebras, Kleene algebras and similar algebraic formalisms, and their applications as conceptual and methodological tools in computer science and beyond. TOPICS: We invite submissions in the general fields of algebras relevant to computer science and applications of such algebras. Topics include but are not limited to: * Theory - algebras such as semigroups, residuated lattices, semirings, Kleene algebras, relation algebras and quantales - their connections with program logics and other logics - their use in the theories of automata, concurrency, formal languages, games, networks and programming languages - the development of algebraic, algorithmic, category-theoretic, coalgebraic and proof-theoretic methods for these theories - their formalisation with theorem provers * Applications - tools and techniques for program correctness, specification and verification - quantitative and qualitative models and semantics of computing systems and processes - algorithm design, automated reasoning, network protocol analysis, social choice, optimisation and control - industrial applications WATA 2020 WATA 2020, the 10th International Workshop on Weighted Automata: Theory and Applications, will take place just after RAMICS, from 14 to 17 April, in Marseille. We encourage participants to combine the two events. SUBMISSION INSTRUCTIONS: Submission is via EasyChair at https://www.easychair.org/conferences/?conf=ramics2020 All papers will be peer-reviewed by at least three referees. The proceedings will be published in an LNCS volume by Springer, ready at the conference. Submissions must not be published or under review for publication elsewhere. Submissions must be in English using a PDF not exceeding 16 pages in LNCS style. Submissions must provide sufficient information to judge their merits. Additional material may be provided in a clearly marked appendix or by a reference to a manuscript on a web site. Experimental data, software or mathematical components for theorem provers must be available in sufficient detail for referees. Deviation from these requirements may lead to rejection. One author of each accepted paper is expected to present the paper at the conference. Accepted papers must be produced with LaTeX. Formatting instructions and LNCS style files are available at http://www.springer.de/comp/lncs/authors.html As for earlier RAMiCS conferences, we intend to publish a journal special issue with revised and extended versions of a selection of the best papers. COMMITTEES: Organising Committee -------------------- Conf. & PC Co-Chair: Peter Jipsen, Chapman University, USA Conf. & PC Co-Chair: Uli Fahrenberg, École polytechnique, France Conf. & PC Co-Chair: Michael Winter, Brock University, Canada Programme Committee ------------------- Roland Backhouse University of Nottingham, UK Rudolf Berghammer Kiel University, Germany Manuel Bodirsky TU Dresden, Germany Jules Desharnais Laval University, Canada Amina Doumane PPS, France Uli Fahrenberg École polytechnique, France Hitoshi Furusawa Kagoshima University, Japan Mai Gehrke LIAFA, France Walter Guttmann University of Canterbury, New Zealand Robin Hirsch University College London, UK Peter Höfner CSIRO, Australia Marcel Jackson La Trobe University, Australia Jean-Baptiste Jeannin University of Michigan, USA Peter Jipsen Chapman University, USA Stef Joosten Open Universiteit, Netherlands Wolfram Kahl McMaster University, Canada Dexter Kozen Cornell University, USA Tadeusz Litak FAU Erlangen-Nürnberg, Germany Wendy MacCaull St. Francis Xavier University, Canada Roger Maddux Iowa State University, USA Annabelle McIver Macquarie University, Australia Szabolcs Mikulas University of London, UK Ali Mili NJIT, USA Jose Oliveira University of Minho, Portugal Alessandra Palmigiano Technical University of Delft, Netherlands Damien Pous CNRS - ENS Lyon, France Mehrnoosh Sadrzadeh Queen Mary University of London, UK Luigi Santocanale LIS, Aix-Marseille Université, France John Stell University of Leeds, UK Georg Struth University of Sheffield, UK Michael Winter Brock University, Canada [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Postdoc Opportunity at Augusta University
by Harley D. Eades III 25 Jul '19

25 Jul '19

Hi, everyone. Please see the postdoc announcement attached. Part of my work on the Granule Project is the study of new categorical models for all things graded. Thus, any category theorist's that are interested are encouraged to apply. Very best, Harley The ForML -- formal methods and computational logic -- Lab at Augusta University [1] is looking for a postdoc. The start date, length of term, and salary are all negotiable, but the latter will be competitive with respect to US based postdoc salaries. We are looking for those who are interested in working with myself and/or Dr. Clement Aubert. My current project is called the Granule Project [2] whose goal is to study the theory and application of graded modalities to type-based programming languages, formal verification, and logic. Dr. Aubert's project is on the semantics and applications concurrency in programming languages [3]. I will be attending ICFP 2019 [4] this year, and if anyone who is also attending or who is near Berlin would like to chat about this opportunity, then please do not hesitate to contact me. The official ad is below, but please send informal inquires to me directly. When officially applying please indicate in your statement of purpose that you are interested in working with the ForML Lab. Very best, Harley Eades Clement Aubert [1] https://the-au-forml-lab.github.io/index.html [2] https://granule-project.github.io/ [3] http://spots.augusta.edu/caubert/ [4] https://icfp19.sigplan.org/ ==Official Ad=== The formal methods group is led by Paul Attie, Clement Aubert, Harley Eades, and Alexander Schwarzmann. We are interested in state of the art theory and its application. Among our envisaged directions is the application of formal methods to cybersecurity and sophisticated distributed systems (both hardware and software). PhD students who expect to graduate within a year are encouraged to apply. The formal methods group is located in the Georgia Cyber Center ( https://www.gacybercenter.org/) a $100 M facility which is ``the single largest investment in a cybersecurity facility by a state government to date.'' The Georgia Cyber Center seeks to prove the USA with a ``decisive advantage in cyberspace,'' by means of a unique industry-government-academia partnership. The Georgia Cyber Center hosts companies involved in cybersecurity work, and together with the US Army Cyber Command headquartered in Fort Gordon, Augusta, ( https://www.arcyber.army.mil/) and local academia, provides a unique ecosystem where challenge problems from military and industry feed into academic research, and research results feed back into industry and government practice. Ms. Regina White RHULL(a)augusta.edu Please include in your application a CV, a statement of purpose, and contact information for at least three referees. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Reminder: International Conference on Homotopy Type Theory 2019
by Michael Shulman 24 Jul '19

24 Jul '19

************************************************************** Reminder: INTERNATIONAL CONFERENCE ON HOMOTOPY TYPE THEORY 12-17 August 2019 Carnegie Mellon University, Pittsburgh USA https://hott.github.io/HoTT-2019 ************************************************************** The Invited Speakers will be: - Ulrik Buchholtz (TU Darmstadt, Germany) - Dan Licata (Wesleyan University, USA) - Andrew Pitts (University of Cambridge, UK) - Emily Riehl (Johns Hopkins University, USA) - Christian Sattler (University of Gothenburg, Sweden) - Karol Szumilo (University of Leeds, UK) There will also be a special Vladimir Voevodsky Memorial Lecture given by - André Joyal (Université du Québec à Montréal, Canada) The schedule, programme, and registered participants list so far is now available on the web site, as is a link to register: https://hott.github.io/HoTT-2019/ We encourage everyone who is planning to come to register soon, so we can get an accurate count for catering purposes. After 1 August, the registration fee will increase from $60/$90 (for the summer school and conference, respectively) to $80/$120. In addition, there are still some rooms still available at the Hotel Indigo at a discounted price for the conference, but these must be reserved by 29 July. The topics and instructors for the associated Homotopy Type Theory Summer School, in the preceding week August 7th to 10th, are: - Cubical methods: Anders Mortberg - Formalization in Agda: Guillaume Brunerie - Formalization in Coq: Kristina Sojakova - Higher topos theory: Mathieu Anel - Semantics of type theory: Jonas Frey - Synthetic homotopy theory: Egbert Rijke We look forward to seeing you in Pittsburgh! The Scientific Committee Steven Awodey Andrej Bauer Thierry Coquand Nicola Gambino Peter LeFanu Lumsdaine Michael Shulman, chair [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

I really mucked up that story.
by Michael Barr, Prof. 22 Jul '19

22 Jul '19

Of course, what Heinrich told him was that in that case it should be "la foncteuse". Thanks to Jack Duskin for (gently) calling the gaffe to my intention. Michael [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

None
by Marco Grandis 20 Jul '19

20 Jul '19

The following article is downloadable: Marco Grandis - George Janelidze, >>From torsion theories to closure operators and factorization systems, Categ. Gen. Algebr. Struct. Appl., in press. Downloadable from CGASA: http://cgasa.sbu.ac.ir/article_87116.html Abstract. Torsion theories are here extended to categories equipped with an ideal of ‘null morphisms’, or equivalently a full subcategory of ‘null objects’. Instances of this extension include closure operators viewed as generalised torsion theories in a ‘category of pairs’, and factorization systems viewed as torsion theories in a category of morphisms. The first point has essentially been treated in [15]. Regards Marco and George [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Categories and functors, Funktor
by Johannes Huebschmann 19 Jul '19

19 Jul '19

Dear All For fun: The German term for functor is "der Funktor". "Das Funktor" translates to remote control gate. Best regards Johannes [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

4 3