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