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
no-eta-equality
field
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!
field
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!
.