Simple Simplices

Simplicial Sets are notoriously annoying to do in proof assistants. Really, the problem comes down to how we define Δ, the simplex category. You really have 2 options here:

1. Define Δ as the category of finite ordinals and monotone maps.
2. Define Δ as a free category generated by face and degeneracy maps, quotiented by the simplicial identities.

Both have appealing characteristics, but each has it's own millstone that will sink any sort of serious attempts to use them. Option number 1 is easy to define, and equalities are simple to think about, but defining functors out of it becomes extremely hairy extremely quick. The problem is that we want to be able to define simplicial sets by how they act on the face and boundary maps, not some random monotonic map! Option 2 solves this problem, but suddenly equality becomes extremely difficult to deal with, as the simplicial identities are not exactly "nice". If only there was a way that we could combine these two approaches…

For reference, the following exploration is written in Agda, using the (excellent) agda-categories library.

As previously mentioned, we want to be able to define simplicial sets by their action on face and boundary maps, so let's take those to be our notion of morphism. We also need to chuck in identities and composites for good measure.

data _Δ⇒_ : ℕ → ℕ → Set where
  ε  : ∀ {n} → n Δ⇒ n
  δ  : ∀ {n} → (i : Fin (suc n)) → n Δ⇒ (suc n)
  σ  : ∀ {n} → (j : Fin n) → (suc n) Δ⇒ n
  _⊚_ : ∀ {l m n} → m Δ⇒ n → l Δ⇒ m → l Δ⇒ n

Now, we don't want to use the simplicial identities, because they are extremely unpleasant to work with. As a refresher, here they are:

δᵢ ∘ δⱼ = δⱼ₊₁ ∘ δᵢ if i ≤ j
σⱼ ∘ σᵢ = σᵢ ∘ σⱼ₊₁ if i ≤ j
σⱼ ∘ δᵢ = δᵢ ∘ σⱼ₋₁ if i < j
σⱼ ∘ δᵢ = id        if i = j or i = j + 1
σⱼ ∘ δᵢ = δᵢ₋₁ ∘ σⱼ if j + 1 < i

Ooof! Those are not going to be fun to use.

Instead, let us appeal to the semantics of our formal chains of morphisms as maps between finite ordinals.

face : ∀ {n} → Fin (ℕ.suc n) → Fin n → Fin (ℕ.suc n)
face Fin.zero    k           = Fin.suc k
face (Fin.suc i) Fin.zero    = Fin.zero
face (Fin.suc i) (Fin.suc k) = Fin.suc (face i k)

degen : ∀ {n} → Fin n → Fin (ℕ.suc n) → Fin n
degen Fin.zero    Fin.zero    = Fin.zero
degen Fin.zero    (Fin.suc k) = k
degen (Fin.suc i) Fin.zero    = Fin.zero
degen (Fin.suc i) (Fin.suc k) = Fin.suc (degen i k)

⟦_⟧ : ∀ {m n} → m Δ⇒ n → (Fin m → Fin n)
⟦ ε ⟧ x = x
⟦ δ i ⟧ x = face i x
⟦ σ j ⟧ x = degen j x
⟦ f ⊚ g ⟧ x = ⟦ f ⟧ (⟦ g ⟧ x)

What we have done here is define a sort of "interpreter" from the language of morphisms of Δ into good, honest functions. Now, what does this buy us? Well, we can define equality of morphisms by appealing to our semantics!

record _≗_ {m n} (f g : m Δ⇒ n) : Set where
  constructor Δ-eq
  field
    Δ-pointwise : ∀ {x} → ⟦ f ⟧ x ≡ ⟦ g ⟧ x

Now, we get the best of both definitions! We can work inductively over morphisms in Δ, while still having a nice, easy way to reason about equality.

Now, if we had a means of decomposing any monotone map Fin m → Fin n into a series of face/degeneracy maps, we could perform a bit of a magic trick. Let's just assume for the sake of argument that we had a function:

decompose : ∀ {m n} → (Fin m → Fin n) → (m Δ⇒ n)

Now, let's assume that this function will yield a sort of "canonical form" for each map. Namely, it ought to return a composition of the form:

δᵢ₁ ∘ ... ∘ δᵢₖ ∘ σⱼ₁ ∘ ... ∘ σⱼₕ

If we had such a function, then we would have a means of writing a solver for morphisms in Δ! We could simply reflect our morphisms in Δ into monotonic maps, then decompose the resulting map to get a canonical form back out. With a bit of metaprogramming, this could easily be wired up to create a solver. Normalization By Evaluation strikes again!

Now, writing such a decompose function is a bit tricky, but isn't impossible. Perhaps some brave soul would like to try!

This presentation is far easier to work with than either of the other two options explored. After trying it out in agda-categories, I've already been able to define some Simplicial Sets that were far out of reach using the monotonic map approach. For instance, it's possible to define the Nerve of a Category quite easily now that we can perform induction on the maps of Δ. If you have any questions or comments, feel free to reach out to me on twitter at @totbwf. I would love to see this idea explored in other proof assistants as well, so let me know if you implement it elsewhere! Furthermore, thanks to the ever helpful sarahzf for listening to my terrible ideas and giving me better ones.