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 DiscreteDiagram where
- Nil :: DiscreteDiagram ~> Z ()
- ::: :: Obj ~> x -> DiscreteDiagram ~> n xs -> DiscreteDiagram ~> (S n) (x, xs)
- type PairDiagram (~>) x y = DiscreteDiagram ~> (S (S Z)) (x, (y, ()))
- arrowPair :: Category ~> => (x1 ~> x2) -> (y1 ~> y2) -> Nat Pair ~> (PairDiagram ~> x1 y1) (PairDiagram ~> x2 y2)
- 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
- 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
Discrete Categories
The arrows in Discrete n, a finite set of identity arrows.
Category (Discrete n) => Category (Discrete (S n)) |
|
(Category (Discrete n), DiscreteNat n) => DiscreteNat (S n) | |
(Category ~>, Category (Discrete n), Functor (DiscreteDiagram ~> n xs)) => Functor (DiscreteDiagram ~> (S n) (x, xs)) |
Diagrams
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 ()) |
type PairDiagram (~>) x y = DiscreteDiagram ~> (S (S Z)) (x, (y, ()))Source
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)Source
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 gSource