Internal Category Theory

I’d like to draw your attention to some incredibly cool mathematics being done over at the 1lab: Internal categories - 1Lab!

You may be familiar with the fact that you can think about categories “internal” to a fixed category \mathcal{C} that has pullbacks. If not, you can briefly refresh by consulting either the nlab page or Evan Patterson’s notes.

Classically, this is done via pullbacks. However, this is not so nice to think about; I want to write composition as a function \mathrm{Hom}(x,y) \times \mathrm{Hom}(y,z) \to \mathrm{Hom}(x,z) rather than thinking about some big pullback diagram.

The 1lab uses generalized elements to get this nice syntax while secretly working with pullbacks under the hood. It looks something like this:

record Internal-cat-on {C₀ C₁} (src tgt : Hom C₁ C₀) : Type (o ⊔ ℓ) where
    idi : ∀ {Γ} → (x : Hom Γ C₀) → Internal-hom src tgt x x
    _∘i_ : ∀ {Γ} {x y z : Hom Γ C₀}
         → Internal-hom src tgt y z → Internal-hom src tgt x y
         → Internal-hom src tgt x z

If you squint past all of the Agda stuff, you can see that idi and _∘i_ look very similar to how you might want to define normal categories: I have an identity, which is in \mathrm{Hom}(x,x) and a composition, which takes a \mathrm{Hom}(x,y) and a \mathrm{Hom}(y,z) and produces a \mathrm{Hom}(x,z).

And then the laws look very similar to the normal laws too!

    idli : ∀ {Γ} {x y : Hom Γ C₀} (f : Internal-hom src tgt x y)
         → idi y ∘i f ≡ f
    idri : ∀ {Γ} {x y : Hom Γ C₀} (f : Internal-hom src tgt x y)
         → f ∘i idi x ≡ f
    associ : ∀ {Γ} {w x y z : Hom Γ C₀}
           → (f : Internal-hom src tgt y z)
           → (g : Internal-hom src tgt x y)
           → (h : Internal-hom src tgt w x)
           → f ∘i g ∘i h ≡ (f ∘i g) ∘i h

Very cool stuff, and very well typeset and explained as well: note that you can choose between sans font and serif font, and also choose between justified and ragged right alignments in the upper left corner. Looking forward to seeing more stuff in 1lab!

1 Like

I misread the title as “Infernal Category Theory” and now I think this should be a thing.

1 Like

I think that’s just set theory :upside_down_face:.

I’m so glad to see that! For a long time I have had handwritten notes on a very similar matter without having the time to write them up. My motivation was a bit different (but the result similar): I was working with parameterized morphisms, as in the Para construction, and frustrated that eg Para(Set) doesn’t have equalizers even though Set does. The problem is that an equalizer in Para(Set) would have its object accordingly parameterized by the parameters of the morphisms it equalizers, but of course this is not allowed in Para(Set). So I started working with internal categories and a notion of parameterization there, which I called “proxying”: and a ‘proxy’ is just what that 1Lab page calls an “internal morphism”. Of course, in this world, you now have parameters on your objects (the arrow x:\Gamma\to X in the third diagram on that page), and so you can talk about things like “parameterized limits” and so on.

I guess I really should get around to writing that stuff up one day…

Rereading this again because I didn’t understand it the first time – this point about “parameterized objects” is quite interesting. In general, when you have morphisms that are “object-y” (i.e. the horizontal morphisms of a double category), it really does seem like you’d get a quite different notion of internal category than one is used to; I don’t have a good intuition at all for what that looks like. Please do write up these notes!

This is a cool idea. Basically, we ask for a category object in presheaves on our original category whose presheaf of objects and presheaf of morphisms are representable. If our underlying category has pullbacks, then the pullbacks in presheaves of these representables are themselves representable; in this case everything takes place inside the underlying category. This ends up being nicer because reasoning gets to take place in our base type theory (which the presheaves land in), rather than in our underlying category.