data-category-0.7.2: Category theory

Data.Category.Simplex

Description

The (augmented) simplex category.

Synopsis

# Simplex Category

data Simplex :: * -> * -> * 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
 Source # The (augmented) simplex category is the category of finite ordinals and order preserving maps. Instance detailsDefined in Data.Category.Simplex Methodssrc :: Simplex a b -> Obj Simplex a Source #tgt :: Simplex a b -> Obj Simplex b Source #(.) :: Simplex b c -> Simplex a b -> Simplex a c Source # Source # The ordinal 0 is the initial object of the simplex category. Instance detailsDefined in Data.Category.Simplex Associated Typestype InitialObject Simplex :: Type Source # Methods Source # The ordinal 1 is the terminal object of the simplex category. Instance detailsDefined in Data.Category.Simplex Associated Typestype TerminalObject Simplex :: Type Source # Methods Source # Instance detailsDefined in Data.Category.Simplex Source # Instance detailsDefined in Data.Category.Simplex

data Z Source #

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

data S n Source #

Instances
 type Add :% (S m, n) Source # Instance detailsDefined in Data.Category.Simplex type Add :% (S m, n) = S (Add :% (m, n)) type (Replicate f a) :% (S n) Source # Instance detailsDefined in Data.Category.Simplex type (Replicate f a) :% (S n) = f :% (a, Replicate f a :% n)

# Functor

data Forget Source #

Constructors

 Forget
Instances
 Source # Turn Simplex x y arrows into Fin x -> Fin y functions. Instance detailsDefined in Data.Category.Simplex Associated Typestype Dom Forget :: Type -> Type -> Type Source #type Cod Forget :: Type -> Type -> Type Source #type Forget :% a :: Type Source # Methods(%) :: Forget -> Dom Forget a b -> Cod Forget (Forget :% a) (Forget :% b) Source # type Dom Forget Source # Instance detailsDefined in Data.Category.Simplex type Dom Forget = Simplex type Cod Forget Source # Instance detailsDefined in Data.Category.Simplex type Cod Forget = ((->) :: Type -> Type -> Type) type Forget :% n Source # Instance detailsDefined in Data.Category.Simplex type Forget :% n = Fin n

data Fin :: * -> * where Source #

Constructors

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

Constructors

Instances
 Source # Ordinal addition is a bifuntor, it concattenates the maps as it were. Instance detailsDefined in Data.Category.Simplex Associated Typestype Dom Add :: Type -> Type -> Type Source #type Cod Add :: Type -> Type -> Type Source #type Add :% a :: Type Source # Methods(%) :: Add -> Dom Add a b -> Cod Add (Add :% a) (Add :% b) Source # Source # Ordinal addition makes the simplex category a monoidal category, with 0 as unit. Instance detailsDefined in Data.Category.Simplex Associated Typestype Unit Add :: Type Source # MethodsunitObject :: 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 Dom Add Source # Instance detailsDefined in Data.Category.Simplex type Cod Add Source # Instance detailsDefined in Data.Category.Simplex type Cod Add = Simplex type Unit Add Source # Instance detailsDefined in Data.Category.Simplex type Unit Add = Z type Add :% (S m, n) Source # Instance detailsDefined in Data.Category.Simplex type Add :% (S m, n) = S (Add :% (m, n)) type Add :% (Z, n) Source # Instance detailsDefined in Data.Category.Simplex type Add :% (Z, n) = n

# The universal monoid

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
 TensorProduct f => Functor (Replicate f a) Source # Replicate a monoid a number of times. Instance detailsDefined in Data.Category.Simplex Associated Typestype Dom (Replicate f a) :: Type -> Type -> Type Source #type Cod (Replicate f a) :: Type -> Type -> Type Source #type (Replicate f a) :% a :: Type 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 Dom (Replicate f a) Source # Instance detailsDefined in Data.Category.Simplex type Dom (Replicate f a) = Simplex type Cod (Replicate f a) Source # Instance detailsDefined in Data.Category.Simplex type Cod (Replicate f a) = Cod f type (Replicate f a) :% Z Source # Instance detailsDefined in Data.Category.Simplex type (Replicate f a) :% Z = Unit f type (Replicate f a) :% (S n) Source # Instance detailsDefined in Data.Category.Simplex type (Replicate f a) :% (S n) = f :% (a, Replicate f a :% n)