Posts with this logo use 
January 30, 2013
The King of France
Posted by David Corfield
You may have seen me pondering over the years how to convince my philosophical colleagues that they ought to invest some time learning category theory. Now, of course philosophers of mathematics should do so, and there’s an excellent case to make that philosophers of physics should do so too, but what of someone working in what are taken to be areas more at the core?
In an as yet undetermined number of posts here, I want to see how we might motivate such attention. Let me start then with a classic from the philosophy of language, involving what are known as ‘definite descriptions’. The use of logic is very common here, so with our new freedom from logic, we ought to have something to say.
January 29, 2013
7th Scottish Category Theory Seminar
Posted by Tom Leinster
Organized at lightning speed, the 7th Scottish Category Theory Seminar will take place at the end of next week: Friday 8 February, 12.30 to 3.15, at the International Centre for Mathematical Sciences in central Edinburgh.
Our three star speakers are:
- Martín Escardó (Computer Science, Birmingham): Sheaves in type theory: a model of uniform continuity
- Danny Stevenson (Mathematics and Statistics, Glasgow): A generalized Eilenberg–Zilber theorem for simplicial sets
- The Café’s very own Simon Willerton (Mathematics and Statistics, Sheffield): A tale of two constructions by Isbell
As an added attraction, Don Zagier will be giving a colloquium shortly afterwards (not as part of our seminar!): Modular forms and black holes: from Ramanujan to Hawking.
For abstracts, see the web page. And thanks to the Glasgow Mathematical Journal Learning and Research Support Fund for funding us.
January 26, 2013
This Week’s Finds at 20
Posted by Tom Leinster
A quiet conversation has been going on about this at the Azimuth thread, but it deserves its own entry. This Week’s Finds recently turned 20.
Jordan Ellenberg had the excellent idea of writing a tribute piece, This Week’s Finds in Number Theory, and encouraged others to do something similar. Valeria de Paiva took up the challenge, with This Week’s Finds in Categorical Logic. And Joachim Kock has just followed up with a wonderful appreciation of This Week’s Finds: String Diagrams, the Number 5, and the Moons of Jupiter.
Update: Now hilbertthm90 has written This Week’s Finds in Arithmetic Geometry.
January 20, 2013
Tight Spans, Isbell Completions and Semi-Tropical Modules
Posted by Simon Willerton
Some time ago, in a response to a comment on a post (?!) I said that I wanted to understand if the tight span construction for metric spaces could be thought of in enriched category theory terms. Tom suggested that it might have something to do with what he calls the Isbell completion construction. Elsewhere, in a response to a post on Equipments I was wondering about connections between metric spaces as enriched categories and tropical mathematics. I have finally got round to writing up a paper on these things. The draft can be found in the following place.
The paper was written to be accessible to people (such as metric geometers or tropical algebraists) with essentially no background in category theory, but to show how categorical methods apply. Consequently, parts of the paper on cocompletion might be seen as a bit pedestrian by some of the categorical cognoscenti. I would be interested to hear thoughts that people have. I will give an overview below the fold.
January 17, 2013
Carleson’s Theorem
Posted by Tom Leinster
I’ve just started teaching an advanced undergraduate course on Fourier analysis — my first lecturing duty in my new job at Edinburgh.
What I hadn’t realized until I started preparing was the extraordinary history of false beliefs about the pointwise convergence of Fourier series. This started with Fourier himself about 1800, and was only fully resolved by Carleson in 1964.
The endlessly diverting index of Tom Körner’s book Fourier Analysis alludes to this:
January 16, 2013
The Universal Property of Categories
Posted by Mike Shulman
Finally, the third paper I promised about generalized category theory is out:
- Richard Garner and Mike Shulman, Enriched categories as a free cocompletion, arXiv
This paper has two parts. The first part is about the theory of enriched bicategories. For any monoidal bicategory , we (or, rather, Richard, who did most of this part) define -enriched bicategories, assemble them into a tricategory, define -profunctors (modules) and weighted bilimits and bicolimits, and construct free cocompletions under such. It’s all a fairly straightforward categorification of ordinary enriched category theory, but although a number of people have defined and used enriched bicategories in the past, I think this is the most comprehensive development so far of their basic theory.
The second part is an application, which uses the theory of enriched bicategories to describe a universal property satisfied by the construction of enriched categories. I’ll explain a bit further below the fold, but the introduction of the paper gives an equivalently good (and more detailed) summary. You can also have a look at these slides from Octoberfest 2012.
January 11, 2013
Two Dimensional Monadicity
Posted by Mike Shulman
(guest post by John Bourke)
This blog is about my recent preprint Two dimensional monadicity which is indeed about two dimensional monadicity. However, the monadicity theorems are an application, and the paper is really about how the weaker kinds of homomorphism that arise in 2-dimensional universal algebra — like strong, lax or colax monoidal functors between monoidal categories — are unique in satisfying certain properties. These properties relate the weak homomorphisms with the more easily understood strict homomorphisms and so are -categorical, rather than 2-categorical, in nature. If you want to understand what I mean then read on.
January 7, 2013
From Set Theory to Type Theory
Posted by Mike Shulman
The discussion on Tom’s recent post about ETCS, and the subsequent followup blog post of Francois, have convinced me that it’s time to write a new introductory blog post about type theory. So if you’ve been listening to people talk about type theory all this time without ever really understanding it—or if you’re a newcomer and this is the first you’ve heard of type theory—this post is especially for you.
I used to be a big proponent of structural set theory, but although I still like it, over the past few years I’ve been converted to type theory instead. There are lots of reasons for this, the most important of which I won’t say much about until the end. Instead I mostly want to argue for type theory mainly from a purely philosophical point of view, following on from some of the discussion on Tom’s and Francois’ posts.
I do want to emphasize again some things that sometimes get lost sight of (and which I sometimes lose sight of myself in the heat of a discussion). All foundational systems are based on valid philosophical points of view, and have their uses. The real reason for preferring one foundation over another should be practical. Type theory, of course, has lots of practical advantages, including a computational interpretation, direct categorical semantics, and especially the potential for a homotopical version; but other foundational choices have different practical advantages. But aside from practical concerns, philosophy is interesting and fun to talk about, and can be helpful when getting used to a new way of thinking when trying to learn a new foundational system—as long as we all try to keep an open mind, and focus on understanding the philosophy behind things that are unfamiliar to us, rather than insisting that they must be wrong because they’re different from what we’re used to.
My goal for this post is to start from material set theories (like ZFC) and structural set theories (like ETCS), and show how type theory can arise naturally out of an attempt to take the best of both worlds. At the end, I’ll argue that to really resolve all the problems, we need univalent type theory.