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

Data.Category.Simplex

Contents

Simplex Category
Functor
The universal monoid

Description

The (augmented) simplex category.

Synopsis

data Simplex :: Type -> Type -> Type 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 :: Type -> Type 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 :: Type -> Type -> Type where Source #

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 Source #	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 Source # tgt :: forall (a :: k) (b :: k). Simplex a b -> Obj Simplex b Source # (.) :: forall (b :: k) (c :: k) (a :: k). Simplex b c -> Simplex a b -> Simplex a c Source #
HasInitialObject Simplex Source #	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 Source # Methods initialObject :: Obj Simplex (InitialObject Simplex) Source # initialize :: forall (a :: k). Obj Simplex a -> Simplex (InitialObject Simplex) a Source #
HasTerminalObject Simplex Source #	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 Source # Methods terminalObject :: Obj Simplex (TerminalObject Simplex) Source # terminate :: forall (a :: k). Obj Simplex a -> Simplex a (TerminalObject Simplex) Source #
type InitialObject Simplex Source #
Instance details Defined in Data.Category.Simplex type InitialObject Simplex = Z
type TerminalObject Simplex Source #
Instance details Defined in Data.Category.Simplex type TerminalObject Simplex = S Z

data Z Source #

Instances

Instances details

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

data S n Source #

Instances

Instances details

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

Functor

data Forget Source #

Constructors

Forget

Instances

Instances details

Functor Forget Source #	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 Source # type Cod Forget :: Type -> Type -> Type Source # type Forget :% a Source # Methods (%) :: Forget -> Dom Forget a b -> Cod Forget (Forget :% a) (Forget :% b) Source #
type Cod Forget Source #
Instance details Defined in Data.Category.Simplex type Cod Forget = (->)
type Dom Forget Source #
Instance details Defined in Data.Category.Simplex type Dom Forget = Simplex
type Forget :% n Source #
Instance details Defined in Data.Category.Simplex type Forget :% n = Fin n

data Fin :: Type -> Type where Source #

Constructors

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

data Add Source #

Constructors

Add

Instances

Instances details

Functor Add Source #	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 Source # type Cod Add :: Type -> Type -> Type Source # type Add :% a Source # Methods (%) :: Add -> Dom Add a b -> Cod Add (Add :% a) (Add :% b) Source #
TensorProduct Add Source #	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 :: Kind (Cod f) Source # Methods unitObject :: Add -> Obj (Cod Add) (Unit Add) Source # leftUnitor :: Cod Add ~ k => Add -> Obj k a -> k (Add :% (Unit Add, a)) a Source # leftUnitorInv :: Cod Add ~ k => Add -> Obj k a -> k a (Add :% (Unit Add, a)) Source # rightUnitor :: Cod Add ~ k => Add -> Obj k a -> k (Add :% (a, Unit Add)) a Source # rightUnitorInv :: Cod Add ~ k => Add -> Obj k a -> k a (Add :% (a, Unit Add)) Source # 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))) Source # 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)) Source #
type Cod Add Source #
Instance details Defined in Data.Category.Simplex type Cod Add = Simplex
type Dom Add Source #
Instance details Defined in Data.Category.Simplex type Dom Add = Simplex :**: Simplex
type Unit Add Source #
Instance details Defined in Data.Category.Simplex type Unit Add = Z
type Add :% (S m, n) Source #
Instance details Defined in Data.Category.Simplex type Add :% (S m, n) = S (Add :% (m, n))
type Add :% (Z, n) Source #
Instance details Defined in Data.Category.Simplex type Add :% (Z, n) = n

The universal monoid

universalMonoid :: MonoidObject Add (S Z) Source #

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

data Replicate f a Source #

Constructors

Replicate f (MonoidObject f a)

Instances

Instances details

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