License	BSD-style (see the file LICENSE)
Maintainer	sjoerd@w3future.com
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Category.Simplex

Contents

Simplex Category
Functor
The universal monoid

Description

The (augmented) simplex category.

Synopsis

data Simplex :: * -> * -> * where
- Z :: Simplex Z Z
- Y :: Simplex x y -> Simplex x (S y)
- X :: Simplex x (S y) -> Simplex (S x) (S y)
data Z
data S n
suc :: Obj Simplex n -> Obj Simplex (S n)
data Forget = Forget
data Fin :: * -> * where
- Fz :: Fin (S n)
- Fs :: Fin n -> Fin (S n)
data Add = Add
universalMonoid :: MonoidObject Add (S Z)
data Replicate f a = Replicate f (MonoidObject f a)

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

Instances details

Category Simplex #	The (augmented) simplex category is the category of finite ordinals and order preserving maps.
Instance details Defined in Data.Category.Simplex Methods src :: forall (a :: k) (b :: k). Simplex a b -> Obj Simplex a # tgt :: forall (a :: k) (b :: k). Simplex a b -> Obj Simplex b # (.) :: forall (b :: k) (c :: k) (a :: k). Simplex b c -> Simplex a b -> Simplex a c #
HasInitialObject Simplex #	The ordinal `0` is the initial object of the simplex category.
Instance details Defined in Data.Category.Simplex Associated Types type InitialObject Simplex :: Kind k # Methods initialObject :: Obj Simplex (InitialObject Simplex) # initialize :: forall (a :: k). Obj Simplex a -> Simplex (InitialObject Simplex) a #
HasTerminalObject Simplex #	The ordinal `1` is the terminal object of the simplex category.
Instance details Defined in Data.Category.Simplex Associated Types type TerminalObject Simplex :: Kind k # Methods terminalObject :: Obj Simplex (TerminalObject Simplex) # terminate :: forall (a :: k). Obj Simplex a -> Simplex a (TerminalObject Simplex) #
type InitialObject Simplex #
Instance details Defined in Data.Category.Simplex type InitialObject Simplex = Z
type TerminalObject Simplex #
Instance details Defined in Data.Category.Simplex type TerminalObject Simplex = S Z

data Z #

Instances

Instances details

type Add :% (Z, n) #
Instance details Defined in Data.Category.Simplex type Add :% (Z, n) = n
type (Replicate f a) :% Z #
Instance details Defined in Data.Category.Simplex type (Replicate f a) :% Z = Unit f

data S n #

Instances

Instances details

type Add :% (S m, n) #
Instance details Defined in Data.Category.Simplex type Add :% (S m, n) = S (Add :% (m, n))
type (Replicate f a) :% (S n) #
Instance details Defined in Data.Category.Simplex 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

Instances details

Functor Forget #	Turn `Simplex x y` arrows into `Fin x -> Fin y` functions.
Instance details Defined in Data.Category.Simplex Associated Types type Dom Forget :: Type -> Type -> Type # type Cod Forget :: Type -> Type -> Type # type Forget :% a # Methods (%) :: Forget -> Dom Forget a b -> Cod Forget (Forget :% a) (Forget :% b) #
type Dom Forget #
Instance details Defined in Data.Category.Simplex type Dom Forget = Simplex
type Cod Forget #
Instance details Defined in Data.Category.Simplex type Cod Forget = (->) :: Type -> Type -> Type
type Forget :% n #
Instance details Defined in Data.Category.Simplex type Forget :% n = Fin n

data Fin :: * -> * where #

Constructors

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

data Add #

Constructors

Add

Instances

Instances details

Functor Add #	Ordinal addition is a bifuntor, it concattenates the maps as it were.
Instance details Defined in Data.Category.Simplex Associated Types type Dom Add :: Type -> Type -> Type # type Cod Add :: Type -> Type -> Type # 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.
Instance details Defined in Data.Category.Simplex 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 #
Instance details Defined in Data.Category.Simplex type Dom Add = Simplex :**: Simplex
type Cod Add #
Instance details Defined in Data.Category.Simplex type Cod Add = Simplex
type Unit Add #
Instance details Defined in Data.Category.Simplex type Unit Add = Z
type Add :% (S m, n) #
Instance details Defined in Data.Category.Simplex type Add :% (S m, n) = S (Add :% (m, n))
type Add :% (Z, n) #
Instance details Defined in Data.Category.Simplex 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

Instances details

TensorProduct f => Functor (Replicate f a) #	Replicate a monoid a number of times.
Instance details Defined in Data.Category.Simplex Associated Types type Dom (Replicate f a) :: Type -> Type -> Type # type Cod (Replicate f a) :: Type -> Type -> Type # type (Replicate f a) :% a # Methods (%) :: Replicate f a -> Dom (Replicate f a) a0 b -> Cod (Replicate f a) (Replicate f a :% a0) (Replicate f a :% b) #
type Dom (Replicate f a) #
Instance details Defined in Data.Category.Simplex type Dom (Replicate f a) = Simplex
type Cod (Replicate f a) #
Instance details Defined in Data.Category.Simplex type Cod (Replicate f a) = Cod f
type (Replicate f a) :% Z #
Instance details Defined in Data.Category.Simplex type (Replicate f a) :% Z = Unit f
type (Replicate f a) :% (S n) #
Instance details Defined in Data.Category.Simplex type (Replicate f a) :% (S n) = f :% (a, Replicate f a :% n)