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))
 data Next where
 data DiscreteDiagram where
 Nil :: DiscreteDiagram ~> Z ()
 ::: :: 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)) ~>  
(HasColimits (Discrete n) ~>, HasBinaryCoproducts ~>) => HasColimits (Discrete (S n)) ~> 
Category (Discrete n) => Category (Discrete (S 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)) 
Functors
data DiscreteDiagram whereSource
The functor from Discrete n
to (~>)
, a diagram of n
objects in (~>)
.
Nil :: DiscreteDiagram ~> Z ()  
::: :: Obj ~> x > DiscreteDiagram ~> n xs > DiscreteDiagram ~> (S n) (x, xs) 
(Category ~>, Category (Discrete n), Functor (DiscreteDiagram ~> n xs)) => Functor (DiscreteDiagram ~> (S n) (x, xs))  
Category ~> => Functor (DiscreteDiagram ~> Z ()) 