open import Cat.Prelude open import Data.Fin import Data.Nat as Nat module Cat.Instances.Simplex where
The simplex categoryπ
The simplex category, , 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