Data.Category.Discrete

Discrete n, the category with n objects, and as the only arrows their identities.

Documentation

data Z

Instances

Category (Discrete Z)

data S n

Constructors

S n

Instances

Category (Discrete n) => Category (Discrete (S n))

data Discrete where

The arrows in Discrete n, a finite set of identity arrows.

Constructors

IdZ :: Discrete (S n) Z Z

StepS :: Discrete n a a -> Discrete (S n) (S a) (S a)

Instances

Category (Discrete n) => Category (Discrete (S n))

Category (Discrete Z)

magicZ :: Discrete Z a b -> x

magicZO :: Obj (Discrete Z) a -> x

data Next where

Constructors

Next :: (Functor f, Dom f ~ Discrete (S n)) => f -> Next n f

Instances

Functor (Next n f)

data DiscreteDiagram where

Constructors

Nil :: DiscreteDiagram ~> Z ()

::: :: Category ~> => Obj ~> x -> DiscreteDiagram ~> n xs -> DiscreteDiagram ~> (S n) (x, xs)

Instances

Functor (DiscreteDiagram ~> n xs)