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.

Methods

src :: Simplex a b -> Obj Simplex a

tgt :: Simplex a b -> Obj Simplex b

(.) :: Simplex b c -> Simplex a b -> Simplex a c

HasInitialObject Simplex

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

Associated Types

type InitialObject (Simplex :: * -> * -> *) :: *

Methods

initialObject :: Obj Simplex (InitialObject Simplex)

initialize :: Obj Simplex a -> Simplex (InitialObject Simplex) a

HasTerminalObject Simplex

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

Associated Types

type TerminalObject (Simplex :: * -> * -> *) :: *

Methods

terminalObject :: Obj Simplex (TerminalObject Simplex)

terminate :: Obj Simplex a -> Simplex a (TerminalObject Simplex)

type InitialObject Simplex

type InitialObject Simplex = Z

type TerminalObject Simplex

type TerminalObject Simplex = S Z

data Z

Instances

type Add :% (Z, n)

type Add :% (Z, n) = n

type (Replicate f a) :% Z

type (Replicate f a) :% Z = Unit f

data S n

Instances

type Add :% (S m, n)

type Add :% (S m, n) = S ((:%) Add (m, n))

type (Replicate f a) :% (S n)

type (Replicate f a) :% (S n) = (:%) f (a, (:%) (Replicate f a) 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.

Associated Types

type Dom Forget :: * -> * -> *

type Cod Forget :: * -> * -> *

type Forget :% a :: *

Methods

(%) :: Forget -> Dom Forget a b -> Cod Forget (Forget :% a) (Forget :% b)

type Dom Forget

type Dom Forget = Simplex

type Cod Forget

type Cod Forget = (->)

type Forget :% n

type Forget :% n = Fin n

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.

Associated Types

type Dom Add :: * -> * -> *

type Cod Add :: * -> * -> *

type Add :% a :: *

Methods

(%) :: Add -> Dom Add a b -> Cod Add (Add :% a) (Add :% b)

TensorProduct Add

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

Associated Types

type Unit Add :: *

Methods

unitObject :: Add -> Obj (Cod Add) (Unit Add)

leftUnitor :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> k (Add :% (Unit Add, a)) a

leftUnitorInv :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> k a (Add :% (Unit Add, a))

rightUnitor :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> k (Add :% (a, Unit Add)) a

rightUnitorInv :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> k a (Add :% (a, Unit Add))

associator :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> Obj k b -> Obj k c -> k (Add :% (Add :% (a, b), c)) (Add :% (a, Add :% (b, c)))

associatorInv :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> Obj k b -> Obj k c -> k (Add :% (a, Add :% (b, c))) (Add :% (Add :% (a, b), c))

type Dom Add

type Dom Add = (:**:) Simplex Simplex

type Cod Add

type Cod Add = Simplex

type Unit Add

type Unit Add = Z

type Add :% (S m, n)

type Add :% (S m, n) = S ((:%) Add (m, n))

type Add :% (Z, n)

type Add :% (Z, n) = n

The universal monoid

universalMonoid :: MonoidObject Add (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

TensorProduct f => Functor (Replicate f a)

Replicate a monoid a number of times.

Associated Types

type Dom (Replicate f a) :: * -> * -> *

type Cod (Replicate f a) :: * -> * -> *

type (Replicate f a) :% a :: *

Methods

(%) :: Replicate f a -> Dom (Replicate f a) a b -> Cod (Replicate f a) (Replicate f a :% a) (Replicate f a :% b)

type Dom (Replicate f a)

type Dom (Replicate f a) = Simplex

type Cod (Replicate f a)

type Cod (Replicate f a) = Cod f

type (Replicate f a) :% Z

type (Replicate f a) :% Z = Unit f

type (Replicate f a) :% (S n)

type (Replicate f a) :% (S n) = (:%) f (a, (:%) (Replicate f a) n)