Data.Category.Simplex

The (augmented) simplex category.

Simplex Category

data Simplex where

Constructors

Z :: Simplex Z Z

Y :: Simplex x y -> Simplex x (S y)

X :: Simplex x (S y) -> Simplex (S x) (S y)

Instances

Category Simplex

The (augmented) simplex category is the category of finite ordinals and order preserving maps.

HasBinaryCoproducts Simplex

The coproduct in the simplex category is a merge operation.

HasInitialObject Simplex

The ordinal 0 is the initial object of the simplex category.

HasTerminalObject Simplex

The ordinal 1 is the terminal object of the simplex category.

data Z

data S n

suc :: Obj Simplex n -> Obj Simplex (S n)

Functor

data Forget

Constructors

Forget

Instances

Functor Forget

Turn Simplex x y arrows into Fin x -> Fin y functions.

data Fin where

Constructors

Fz :: Fin (S n)

Fs :: Fin n -> Fin (S n)

data Add

Constructors

Add

Instances

Functor Add

Ordinal addition is a bifuntor, it concattenates the maps as it were.

TensorProduct Add

Ordinal addition makes the simplex category a monoidal category, with 0 as unit.

The universal monoid

universalMonoid :: MonoidObject (CoproductFunctor Simplex) (S Z)

The maps 0 -> 1 and 2 -> 1 form a monoid, which is universal, c.f. Replicate.

data Replicate f a

Constructors

Replicate f (MonoidObject f a)

Instances

(Category (Dom (Replicate f a)), Category (Cod (Replicate f a)), TensorProduct f) => Functor (Replicate f a)

Replicate a monoid a number of times.