Portability  nonportable 

Stability  experimental 
Maintainer  sjoerd@w3future.com 
Discrete n, the category with n objects, and as the only arrows their identities.
 data Discrete where
 data Z
 data S n
 type Void = Discrete Z
 type Unit = Discrete (S Z)
 type Pair = Discrete (S (S Z))
 magicZ :: Discrete Z a b > x
 data Succ n = Succ
 data DiscreteDiagram where
 Nil :: DiscreteDiagram ~> Z ()
 ::: :: (Category ~>, Category (Discrete n)) => Obj ~> x > DiscreteDiagram ~> n xs > DiscreteDiagram ~> (S n) (x, xs)
 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
Discrete Categories
The arrows in Discrete n, a finite set of identity arrows.
Category (Discrete Z) 

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

(HasLimits (Discrete n) ~>, HasBinaryProducts ~>) => HasLimits (Discrete (S n)) ~>  The product of 
(HasColimits (Discrete n) ~>, HasBinaryCoproducts ~>) => HasColimits (Discrete (S n)) ~>  The coproduct of 
Category (Discrete n) => Category (Discrete (S n)) 

(HasLimits (Discrete n) ~>, HasBinaryProducts ~>) => HasLimits (Discrete (S n)) ~>  The product of 
(HasColimits (Discrete n) ~>, HasBinaryCoproducts ~>) => HasColimits (Discrete (S n)) ~>  The coproduct of 
Functor (DiscreteDiagram ~> n xs) => Functor (DiscreteDiagram ~> (S n) (x, xs))  A diagram with one more object. 
Functors
data DiscreteDiagram whereSource
The functor from Discrete n
to (~>)
, a diagram of n
objects in (~>)
.
Nil :: DiscreteDiagram ~> Z ()  
::: :: (Category ~>, Category (Discrete n)) => Obj ~> x > DiscreteDiagram ~> n xs > DiscreteDiagram ~> (S n) (x, xs) 
Functor (DiscreteDiagram ~> n xs) => Functor (DiscreteDiagram ~> (S n) (x, xs))  A diagram with one more object. 
Category ~> => Functor (DiscreteDiagram ~> Z ())  The empty diagram. 