Snowglobe Models
Posted by John Baez
Last week in my course on Classical vs Quantum Computation, James Dolan said a bit about funny nonstandard models of typed λtheories — like the typed λtheory for high school calculus. He calls these ‘snowglobe models’, because they live ‘inside’ the usual world of sets — but in their own selfcontained miniature universe, like a snowglobe:
I’d like to talk about these a bit before I forget!
Lately in my course I’ve been focusing on ‘classical’ computation, hence closed monoidal categories where the tensor product is the cartesian product. However, the idea of a snowglobe model is more general, so let me talk about it more generally.
Suppose $T$ is a closed symmetric monoidal category, as defined here. Very roughly, this a category where any two objects $x$ and $y$ have a tensor product $x \otimes y \in T$ and also an ‘object of maps’ from $x$ to $y$, denoted $hom(x,y) \in T$. The latter should not be confused with the usual set of morphisms $Hom(x,y)$! It’s often called the ‘internal hom’, since it lives inside $T$.
We can think of $T$ as a theory. A model of this theory in some other closed monoidal category $C$ is a functor
$F: T \to C$
preserving all the relevant structure. Namely:
 The functor $F$ must be symmetric monoidal, as defined here. Very roughly, this means $F$ preserves tensor products.
 The functor $F$ must be closed, meaning that for any pair of objects $x,y \in T$, the godgiven morphism $F(hom(x,y)) \to hom(F(x),F(y))$ is an isomorphism.
Now, suppose we have a functor
$F: T \to C$
which is symmetric monoidal but not closed. We can think of this as a defective model — but it gives a perfectly fine ‘snowglobe model’ in some other category!
Here’s how.
First, let’s form a kind of ‘hybrid’ of $T$ and $C$, having objects of $T$ as its objects, but the objects $F(hom(x,y)) \in C$ as its ‘homobjects’.
This hybrid — let’s call it $\tilde{C}$ — does not begin life as a category, because instead of a set of morphisms from $x$ to $y$, it just has an object in $C$, namely $F(hom(x,y))$. It’s what people call a category enriched over $C$, as defined here.
The terminology is a little confusing to beginners: it’s important to realize that a ‘category enriched over $C$’ is not an actual category. But, just as Pinocchio, who began life as a puppet, eventually became a real boy, $\tilde{C}$ can with sufficient effort become a real category!
To do it, for each pair of objects $x,y \in \tilde{C}$ we define a morphism $f: x \to y$ to be a morphism in $C$ from $I$ (the unit object of $C$) to $F(hom(x,y))$. This sometimes called a point of the homobject $F(hom(x,y))$. These points form an actual set, and with some work $\tilde{C}$ becomes an actual category.
In fact, now that $\tilde C$ is a category, it even becomes a closed symmetric monoidal category in an obvious way!
I know what some of you are thinking:
I felt like that too, the first time Jim showed me this sort of construction a few years ago. But really, once you grok the definitions, the construction is not hard! (Unless, of course, I’m making some mistake.) This is part of the fun of category theory — it gives your brain a real workout, but in the end it all seems perfectly obvious.
Anyway: now our original functor
$F: T \to C$
factors into a first stage
$F_1 : T \to \tilde{C}$
and a second stage
$F_2 : \tilde{C} \to C.$
And, $F_1$ is a closed symmetric monoidal functor! This is more or less by construction. $F_1$ preserves the tensor product because $F$ did. But, $F_1$ also preserves the internal hom, because the internal hom in $\tilde C$ is borrowed from $C$.
So,
$F_1 : T \to \tilde{C}$
is a model of our theory $T$: a snowglobe model. It’s called a snowglobe model because while it comes from a defective model that lives in $C$, it really lives inside the miniature universe $\tilde{C}$.
To really appreciate this construction, you need to look at some examples, like the theory of highschool calculus. But, I’m a bit too tired for that right now. For now, I just wanted to get this down in writing.
I should add for the experts that this factorization of $F$ into two stages is related to the theory of Postnikov towers, as explained in Section 3.1 here.
I’ve corrected this post thanks to comments by Robin Houston, Todd Trimble and James Dolan. Some of their comments won’t make much sense without knowing what my mistakes had been, so here they are:
 I had written $hom(F(x),F(y))$ in lots of places where I should have written $F(hom(x,y))$.

I had defined a symmetric monoidal functor $F: T \to C$ to be ‘closed’ if $F(hom(x,y)) \cong hom(F(x),F(y)).$ In fact, there’s a godgiven morphism $F(hom(x,y)) \to hom(F(x),F(y))$ and $F$ is closed if this is invertible.
To get this godgiven morphism, start with the evaluation $ev: hom(x,y) \otimes x \to y$ in $T$. Then apply $F$: $F(ev): F(hom(x,y) \otimes x) \to F(y)$ Then use the fact that $F$ preserves tensor products up to a specified isomorphism to get the morphism $F(hom(x,y)) \to hom(F(x),F(y)).$
Re: Snowglobe Models
This looks very interesting, but I must be missing something because it isn’t quite making sense.
The way you’ve explained it, the intermediate stage where $\tilde{C}$ is viewed as a $C$enriched category seems to be redundant. A morphism $x\to y$ in $\tilde{C}$ is a point of $\hom(F(x),F(y))$, or in other words an arrow $F(x)\to F(y)$ in $C$!
So this factorisation is the usual factorisation of a functor into a bijectiononobjects followed by a fullandfaithful functor. But then I don’t see why $\tilde{C}$ is closed, unless the functor $F$ was closed in the first place, which rather defeats the object!
Any elucidation would be much appreciated.
Also, a little nit or query. You wrote
I think the definition of closed functor is actually more subtle than that: the monoidality of the functor automatically induces a natural transformation $F(\hom(A,B))\to\hom(F A,F B)$, and a (symmetric monoidal) closed functor is one for which this natural transformation is invertible. I suppose it’s possible that your condition implies mine: is that true?
(On a complete tangent, I wonder whether you could be persuaded that the linear logicinspired notation $x\multimap y$ is a much more pleasant way to denote the internal hom than $\hom(x,y)$, which is easily confused with Hom$(x,y)$. Another advantage of this notation is that it is readily adapted to the nonsymmetric case, where there are two internal homs, by using a leftpointing variant – with the arguments in reverse order – for one of them. (This is unfortunately harder to do on the web, because the leftpointing version doesn’t have a Unicode codepoint. It’s easy in Latex, by rotating or reflecting the rightpointing one.))