data-category-0.11: Category theory
LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Category.Simplex

Description

The (augmented) simplex category.

Synopsis

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 #

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 #

type InitialObject Simplex Source # 
Instance details

Defined in Data.Category.Simplex

type TerminalObject Simplex Source # 
Instance details

Defined in Data.Category.Simplex

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)

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 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 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)