Portability | non-portable |
---|---|
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 ()) |