Todd Trimble HomePage

This is the private area of Todd Trimble within the nLab. I plan to use this page to discuss some ideas I’ve had over the years, which might not ever get officially published but which might still be interesting to some people.

Three topos theorems in one

This appears to be a new theorem in topos theory which I found maybe about twelve years ago. I was reminded of it when there was recent discussion on the blog about local modalities.

Surface diagrams

I hope the existence of the nLab, with its excellent software and supportive community, will help inspire me to finally write up notes on surface diagrams, which some people have asked about over the years. At the time I left academe, I was unhappy with the still embryonic state in which I left this project, and was reluctant to attempt to publish any of it. But I’ve nothing to lose now by taking this up again.


This is a name for a 2-categorical concept which is supposed to be a “paradise” in which to do enriched category theory without being plagued by irritating foundational issues. It looks to me like a semantically viable concept, but right now it’s just a language, somewhat in the way that lambda calculus was just a language before the introduction of legitimate models. There’s a nice string/surface diagram calculus to go along with it.

Some n-category combinatorics?

Some thoughts on the “machines” for constructing those big diagrams for tetracategories, and beyond. Includes some speculations on semi-strictification.

Notes on operads and the Lie operad

This will be an updated version of an old preprint of mine on various constructions of the Lie operad due to Joyal and to Ginzburg-Kapranov, and a comparison map between them.

Notes on the Lie Operad

This is to be a fairly faithful reconstruction of an unpublished paper of mine from about 1997, which John Baez has archived at his web site. I will however take the liberty of correcting some mistakes and changing some words here and there, with the hope of improving the exposition.

I should probably use the other article, Notes on operads and the Lie operad, to improve the actual mathematical content.

Revised version of my doctoral dissertation?

The central problem on which I wrote my thesis is the coherence problem for closed categories, focusing in particular on the case of symmetric monoidal closed categories, but with applications to other cases like that of **-autonomous categories.

My thesis was defended in 1993, and the finishing touches completed after I had begun post-doctoral work under Ross Street, sometime in 1994. It has remained unpublished. I hope this revised version satisfies some of the demand for publication of the original.

Further developments on Trimble n-categories

Urs Schreiber? has been encouraging me to push the theory further. What can you do with these n-categories? Is there an (n+1)(n+1)-category of nn-categories? Is there a viable nerve construction? What is the status of the homotopy hypothesis? Is there a good notion of stable (symmetric monoidal) nn-category? There are many other questions to be asked. I hope to make some groping attempts to begin addressing them here.

Further developments on Trimble higher categories?

These notes are intended as partially rewriting or replacement of the earlier “further developments”. They are spurred by a thread at the nLab which emanated from Mike Shulman?‘s observation that Trimble ω\omega-categories (defined as objects in a certain terminal coalgebra structure, following work by Tom Leinster? and Eugenia Cheng?) admit a slick coinductive definition.

For the moment, I want to see if I can make headway with (1) universal contractible bimodules over contractible globular operads, and (2) the idea that Trimble ω\omega-categories are the algebras of a globular (Batanin) operad which is the inverse limit of the incoherent globular operads introduced by Leinster and Cheng.

Buildings for category theorists

At some point I’ll adapt this material for a Café post, but I’ll try to put down some things here.

Games and Mac Lane's conjecture?

Here’s another project that sort of petered out. There’s a conjecture in coherence theory by Mac Lane, that if a diagram in a free symmetric monoidal closed category on a discrete category is noncommutative, then the diagram is non-commutative under some interpretation of that diagram in the category of vector spaces. This was proven correct by Soloviev in a very technical paper; in the same paper he shows that vector spaces can be replaced by pointed sets.

My interest (together with Geraldine Brady) was to develop a simpler, less technical proof which would take advantage of game semantics similar to those developed for linear logic, and which would give some abstract conditions on a symmetric monoidal closed category which would enable it to be a “test category” (like VectVect in Mac Lane’s conjecture). A conjecture along these lines is that sets equipped with a permutation (which fails the test category criteria set out by Soloviev) would do just fine for example.


A dippy little result: a compact convex set is a ball. I really just want to see if I can write out a proof and keep it around somewhere.


In just about every reference I’ve seen, the proof that the l pl^p norm (on a finite-dimensional space n\mathbb{R}^n let’s say) is in fact a norm first requires a proof of Hölder’s inequality. This is somewhat unsatisfying to me, because it’s something of a magic trick, or at least not the method one would first think of. I wanted to see whether I could write down a more natural and straightforwardly geometric proof.

Characterizations of compactness

Years ago I learned from Walter Tholen that the topological condition that the projection π:X×YY\pi: X \times Y \to Y is a closed map for every space YY is equivalent to compactness of XX. Due to a question and answer session at Math Overflow, I learned (from Andrej Bauer) of an elegant paper by Martin Escardo which gives a proof which doesn’t rely on choice principles (an improvement on my own efforts, where I freely invoked the ultrafilter theorem). Here I’m going to record some snippets from what I’ve learned.

Notes on Unitary Irreps of the Poincare Group?

Where I finally attempt to write up some basic foundational material for particles in quantum field theory.

Some basic Stone-von Neumann spectral theory

This is a preliminary exercise for getting into some other foundational approaches that deal with eigenket expansions in quantum mechanics, following Dirac, but made rigorous using the formalism of rigged Hilbert spaces.

Notes on predicate logic

This is to be exported to the nLab once these notes are hammered into shape a little bit.

Proving lemmas on monoidal categories

There is some interest in learning how to automate proofs of those fiddly lemmas on units in monoidal categories that were proved by Max Kelly in 1964. These are preliminary to proving the coherence theorem. The approach is to consider the diagrams for these proofs as cells in certain definable polytopes similar to the associahedra, but involving units instead of just associativities.

Notes on conversations with James Dolan

These will be notes on conversations I’ll be having with James (aka Jim) Dolan on various aspects of mathematics, according to my own understanding.

Spans of groupoids

These will be some notes in conjunction with some correspondence between me and Alex Hoffnung on the structure of the tricategory of spans of groupoids (in a finitely complete category).

Stuff on coalgebras

To be exported in the nLab soon.

Associated idempotent monad of a monad

Where I try to recall Fakir’s theorem (correctly this time; the nLab page has some misinformation which should be corrected).

Notes on Homotopy Type Theory?

I’ve begun reading Mike Shulman’s fantastic Café posts on the brave new world of homotopy-intensional type theory, which I suppose may be seen as new foundations for (,1)(\infty, 1)-categorical mathematics. This stuff is just mind-blowing, and I want to try to pursue it a little in my own words, without suggesting for a moment that I intend to “improve” upon it in any way. These are notes by myself, for myself, and if you like them then that is an extra bonus.

Notes on Boolean algebras?

Just some easy observations.

Notes on Euler factors

For James Dolan. This is to write out some vague ideas we were discussing.

Notes on SU(2) reps

Really basic stuff.

Frobenius reciprocity implies Frobenius laws

Trying to upload something here which is to be referred to in the nLab.

Some notes on the theme of well-foundedness

Bits and pieces I’m trying to put together on the coalgebraic approach to recursion, algebraic set theory, and other things.

Small cocompletions

I got interested in determining the structure of the free completion of SetSet with respect to small colimits, and in the analogous problem where SetSet is replaced by a Grothendieck topos EE. Some findings will be recorded here.

Completeness of polynomials

I just wanted to record a simple proof of something that was bothering me recently, about proving completeness of polynomials in a Hilbert space with respect to a weighted measure.

Lemma on wide pushouts

Recording here a technical result which arose from a Math Overflow discussion.

Nerve of opposite category

On whether the “classifying space” of a category is homeomorphic to that of its opposite. Seems obviously true, but there’s nothing like a proof!


The notion of tree is slightly fiddly when it is asked to accommodate free theories on signatures which include constants. Here we will try to get it right.

Functional completeness for cartesian closed categories

To be exported to the nLab.

Theory of units and tabulations in allegories

Some technical material, to be exported to the nLab.

Note on power allegories

Freyd and Scedrov initially define a power allegory to be an allegory 𝒜\mathcal{A} where the inclusion i:Map(𝒜)𝒜i \colon Map(\mathcal{A}) \to \mathcal{A} has a right adjoint P:𝒜Map(𝒜)P \colon \mathcal{A} \to Map(\mathcal{A}). Almost immediately they back off from this definition, and redefine it to be a division allegory with certain properties, but without ever showing that a power allegory is a division allegory according to the initial definition. In fact it is an interesting and slightly non-trivial matter to show this; this is the aim of this note.

Cartesian closure of internal categories

If EE is finitely complete and cartesian closed, then is it true that Cat(E)Cat(E) is also? I aim to find out.

Closed structure on modules over a commutative monoid

“Buschi Sergio” at MathOverflow asked a question about this, and I had given a morally correct but somewhat desultory answer. This is an expansion which might be more helpful to him and others.

Morphisms between tensor functors

In answer to another question at MathOverflow. Big frickin’ diagram.

Countable unions of locally compact Hausdorff spaces?

If XX and YY are countable unions of locally compact Hausdorff spaces, equipped with the colimit topologies, then the topological product agrees with the compactly generated product. This is technically extremely useful, and yet it’s hard to find a proof on the internet. Well, not anymore.

Initial algebras and terminal coalgebras

Using Paul Taylor’s development of recursion theory in his book, we give some simple conditions where initial algebras may be constructed inside terminal colgebras.

Monic endomorphisms on the subobject classifier

A famous exercise in Johnstone’s Topos Theory is that these are isomorphisms, in fact involutions. I located a write-up I made of this a few decades ago, and am recording here what I wrote up then.

Cyclic operads

This is to be a conceptual treatment.

Towards a doctrine of operads

I’ll be recording some examples of operad-like concepts (nonpermutative, permutative, braided, cartesian, etc.) hopefully working up to a general doctrinal theory of operads.

Some combinatorics on trees and functions

In response to an intriguing (and nontrivial) MO question.

Varieties of algebras

This was an nLab article that I and others had some quibbles with and wanted to correct.

Dippy disproof of infinitary extensivity of affine schemes

I started this discussion in the nForum about a claim spotted in the nLab, and here I will end it.

Hyperdoctrine version of Gödel incompleteness

If you understand hyperdoctrines, this might have some appeal.

Continuity of the exponential function

This is in response to a discussion we had on the nForum about teaching calculus.

digraph stuff

This is a very nuts-and-bolts description of the cartesian closed structure of the category of sets equipped with a binary relation.

Notes on group objects

Mainly for the category of cocommutative coalgebras.

Characterization of sine

This came up with regard to the nLab page on pi (the mathematical constant) and related nForum discussion. Just recording my findings here.

Whitney trick

The proof that right duals in a braided monoidal category are also left duals is essentially an algebraic rendering of the so-called Whitney trick for knots. I’ll spell it out here.

multisorted Lawvere theories

This is for John Baez.

classical well-foundedness

It’s a very cute fact that in a topos E\mathbf{E}, as soon as there is an object XX with an inhabited binary relation \prec that is classically well-founded (in the sense that for any inhabited subobject PP of XX, the subobject of \prec-minimal elements of PP is also inhabited), the topos must be Boolean. We will prove that fact here.

quotients of reals

I had asked at MathOverflow about characterizing spaces that admit continuous surjections from \mathbb{R}. After thinking about it some more, it could be that a more fruitful thing to consider is the category of topological quotients of \mathbb{R}, or what I’ll call LP-spaces. I’ll record some notes on this here.



Or abstract manifold theory.

Karoubi envelope

In response to a discussion at MathOverflow.

elementary sequence question

In response to a question at MathOverflow.

finitely generated projective

In response to a question at MathOverflow.

discrete harmonic functions

In response to a closed question at MathOverflow.

remark on Cantor-Schroeder-Bernstein

epimorphisms in the category of groups

They are surjections. Just wanted to have a place to put this.

distributivity implies monicity of coproduct inclusions

Cantor's theorem for posets

(Lawvere’s fixed-point theorem is not enough, so what’s the proof?)

An elementary approach to elementary topos theory

Revisions of a long article on an approach introduced to me by Myles Tierney.

Tychonoff theorem for locales

Hopefully to be exported to the nLab.


Lagrange four squares theorem

I wanted to write out a clean proof that I could refer to.

sup-lattices in quasitoposes

(This attempt is pretty flawed.)

category of simple graphs

I wanted to preserve a version of the current article at the nLab and maybe work on it more here.

graph minor

See the previous comment.

core-compact spaces are exponentiable

I wanted to record a succinct proof of this important fact.

Revised on July 29, 2019 at 13:30:23 by Todd Trimble