Portability | non-portable |
---|---|
Stability | experimental |
Maintainer | sjoerd@w3future.com |
- data family Funct c d a b :: *
- data FunctO c d f = (Dom f ~ c, Cod f ~ d) => FunctO f
- type Component f g z = Cod f (F f z) (F g z)
- type :~> f g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Funct c d (FunctO c d f) (FunctO c d g)
- data Diag j (~>) = Diag
- type InitMorF x u = (x :*-: Cod u) :.: u
- type TermMorF x u = (Cod u :-*: x) :.: u
- data InitialUniversal x u a = InitialUniversal (F (InitMorF x u) a) (InitMorF x u :~> (a :*-: Dom u))
- data TerminalUniversal x u a = TerminalUniversal (F (TermMorF x u) a) (TermMorF x u :~> (Dom u :-*: a))
- type Cone f n = Const (Dom f) (Cod f) n :~> f
- type Cocone f n = f :~> Const (Dom f) (Cod f) n
- type Limit f l = TerminalUniversal (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l
- type Colimit f l = InitialUniversal (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l
- data Adjunction f g = Adjunction {}
Documentation
data family Funct c d a b :: *Source
Functor category Funct(C, D), or D^C. Arrows of Funct(C, D) are natural transformations. Each category C needs its own data instance.
Objects of Funct(C, D) are functors from C to D.
(Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA CoprodInHask (FunctO Pair (->) f) (FunctO Pair (->) g) | |
(Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA ProdInHask (FunctO Pair (->) f) (FunctO Pair (->) g) | |
CategoryO (Funct Void d) (FunctO Void d f) | |
(CategoryO (Cod f) (F f Fst), CategoryO (Cod f) (F f Snd)) => CategoryO (Funct Pair d) (FunctO Pair d f) | |
(CategoryO (Cod f) (F f Fls), CategoryO (Cod f) (F f Tru)) => CategoryO (Funct Boolean d) (FunctO Boolean d f) | |
(Dom f ~ Omega, Cod f ~ d, CategoryO (Cod f) (F f Z)) => CategoryO (Funct Omega d) (FunctO Omega d f) |
type :~> f g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Funct c d (FunctO c d f) (FunctO c d g)Source
The diagonal functor from (index-) category J to (~>).
data InitialUniversal x u a Source
data TerminalUniversal x u a Source
type Cone f n = Const (Dom f) (Cod f) n :~> fSource
A cone from N to F is a natural transformation from the constant functor to N to F.