open import Cat.Prelude

open import Data.Fin

import Data.Nat as Nat

module Cat.Instances.Simplex where

open Precategory


# 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

open Ξ-map

private
unquoteDecl eqv = declare-record-iso eqv (quote Ξ-map)
Ξ-map-is-set : β x y β is-set (Ξ-map x y)
Ξ-map-is-set x y = Isoβis-hlevel 2 eqv \$ hlevel!

Ξ-map-path
: β {n m : Nat} {f g : Ξ-map n m}
β (β x β f .map x β‘ g .map x)
β f β‘ g
Ξ-map-path p i .map x = p x i
Ξ-map-path {f = f} {g} p i .ascending x y w =
is-propβpathp (Ξ» j β Nat.β€-is-prop {to-nat (p x j)} {to-nat (p y j)})
(f .ascending x y w) (g .ascending x y w) i

Ξ : 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