Data.Category.Discrete

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

Discrete Categories

data Discrete where

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

Constructors

Z :: Discrete (S n) Z Z

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

Instances

Category (Discrete Z)

Discrete Z is the discrete category with no objects.

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

Discrete (S n) is the discrete category with one object more than Discrete n.

(HasLimits (Discrete n) ~>, HasBinaryProducts ~>) => HasLimits (Discrete (S n)) ~>

(HasColimits (Discrete n) ~>, HasBinaryCoproducts ~>) => HasColimits (Discrete (S n)) ~>

data Z

Instances

Category (Discrete Z)

Discrete Z is the discrete category with no objects.

Category ~> => Functor (DiscreteDiagram ~> Z ())

data S n

Instances

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

Discrete (S n) is the discrete category with one object more than Discrete n.

(HasLimits (Discrete n) ~>, HasBinaryProducts ~>) => HasLimits (Discrete (S n)) ~>

(HasColimits (Discrete n) ~>, HasBinaryCoproducts ~>) => HasColimits (Discrete (S n)) ~>

(Category ~>, Category (Discrete n), Functor (DiscreteDiagram ~> n xs)) => Functor (DiscreteDiagram ~> (S n) (x, xs))

type Void = Discrete Z

Void is the empty category.

type Unit = Discrete (S Z)

Unit is the discrete category with one object.

type Pair = Discrete (S (S Z))

Pair is the discrete category with two objects.

Functors

data Next where

Constructors

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

Instances

(Functor f, Category (PredDiscrete (Dom f))) => Functor (Next f)

data DiscreteDiagram where

The functor from Discrete n to (~>), a diagram of n objects in (~>).

Constructors

Nil :: DiscreteDiagram ~> Z ()

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

Instances

(Category ~>, Category (Discrete n), Functor (DiscreteDiagram ~> n xs)) => Functor (DiscreteDiagram ~> (S n) (x, xs))

Category ~> => Functor (DiscreteDiagram ~> Z ())

Natural Transformations

voidNat :: (Functor f, Functor g, Category d, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d) => f -> g -> Nat Void d f g