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 n) => Category (Discrete (S n))

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

Category (Discrete Z)

Discrete Z is the discrete category with no objects.

data Z

Instances

DiscreteNat Z

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.

(Category (Discrete n), DiscreteNat n) => DiscreteNat (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.

Diagrams

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

type PairDiagram (~>) x y = DiscreteDiagram ~> (S (S Z)) (x, (y, ()))

The functor from Pair to (~>), a diagram of 2 objects in (~>).

arrowPair :: Category ~> => (x1 ~> x2) -> (y1 ~> y2) -> Nat Pair ~> (PairDiagram ~> x1 y1) (PairDiagram ~> x2 y2)

Natural Transformations

discreteNat :: (DiscreteNat n, Functor f, Functor g, Category d, Dom f ~ Discrete n, Dom g ~ Discrete n, Cod f ~ d, Cod g ~ d) => f -> g -> ComList f g n Z -> Nat (Discrete n) d f g

data ComList f g n z where

Constructors

ComNil :: ComList f g Z z

:::: :: Com f g z -> ComList f g n (S z) -> ComList f g (S n) z

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

pairNat :: (Functor f, Functor g, Category d, Dom f ~ Pair, Cod f ~ d, Dom g ~ Pair, Cod g ~ d) => f -> g -> Com f g Z -> Com f g (S Z) -> Nat Pair d f g