open import Cat.Prelude

open import Data.Fin

import Data.Nat as Nat

module Cat.Instances.Simplex where

The simplex categoryπŸ”—

The simplex category, Ξ”\Delta, is generally introduced as the category of non-empty finite ordinals and order-preserving maps. We will, for convenience reasons, define it skeletally: Rather than taking actual finite ordinals as objects, we will use the natural numbers as ordinals, each natural standing for the isomorphism class of ordinals of that cardinality.

record Ξ”-map (n m : Nat) : Type where
  field
    map       : Fin (suc n) β†’ Fin (suc m)
    ascending : (x y : Fin (suc n)) β†’ x ≀ y β†’ map x ≀ map y

Ξ” : Precategory lzero lzero
Ξ” .Ob = Nat
Ξ” .Hom n m = Ξ”-map n m
Ξ” .Hom-set = Ξ”-map-is-set

Ξ” .id .map x = x
Ξ” .id .ascending x y p = p

Ξ” ._∘_ f g .map x = f .map (g .map x)
Ξ” ._∘_ f g .ascending x y p = f .ascending _ _ (g .ascending _ _ p)

Ξ” .idr f = Ξ”-map-path Ξ» x β†’ refl
Ξ” .idl f = Ξ”-map-path Ξ» x β†’ refl
Ξ” .assoc f g h = Ξ”-map-path Ξ» x β†’ refl