Data.Category
Description
This module is a stub!
Synopsis
data Cat ob hom = Cat {
 homIsFun :: ((ob :×: ob) :~>: Univ) hom getid :: forall a. (a :∈: ob) -> ExId hom a getc :: forall a b c. (a :∈: ob) -> (b :∈: ob) -> (c :∈: ob) -> ExC hom a b c
}
data ExId hom a where
 ExId :: (((a, a), aa) :∈: hom) -> aa -> ExId hom a
data ExC hom a b c where
 ExC :: (((b, c), bc) :∈: hom) -> (((a, b), ab) :∈: hom) -> (((a, c), ac) :∈: hom) -> (bc -> ab -> ac) -> ExC hom a b c
kleisli :: Monad m => Cat Univ (KleisliHom m)
fromControlCategory :: Category hom => Cat Univ (BiGraph hom)
makeCat :: ((ob :×: ob) :~>: Univ) hom -> (forall a aa. (((a, a), aa) :∈: hom) -> aa) -> (forall a b c bc ab ac. (((b, c), bc) :∈: hom) -> (((a, b), ab) :∈: hom) -> (((a, c), ac) :∈: hom) -> bc -> ab -> ac) -> Cat ob hom
idauto :: Fact (a :∈: ob) => Cat ob hom -> ExId hom a
cauto :: (Fact (a :∈: ob), Fact (b :∈: ob), Fact (c :∈: ob)) => Cat ob hom -> ExC hom a b c
data GFunctor ob1 hom1 ob2 hom2 f = GFunctor {
 omapIsFun :: (ob1 :~>: ob2) f getfmap :: forall a b. (a :∈: ob1) -> (b :∈: ob1) -> ExFmap hom1 hom2 f a b
}
data ExFmap hom1 hom2 f a b where
 ExFmap :: ((a, fa) :∈: f) -> ((b, fb) :∈: f) -> (((a, b), ab) :∈: hom1) -> (((fa, fb), fafb) :∈: hom2) -> (ab -> fafb) -> ExFmap hom1 hom2 f a b
fromFunctor :: Functor f => GFunctor Univ HaskFun Univ HaskFun (Graph f)
Documentation
 data Cat ob hom Source
Category with type-level set of objects and type-level hom function, but value-level composition and value-level definition of identity functions.
Constructors
Cat
 homIsFun :: ((ob :×: ob) :~>: Univ) hom getid :: forall a. (a :∈: ob) -> ExId hom a getc :: forall a b c. (a :∈: ob) -> (b :∈: ob) -> (c :∈: ob) -> ExC hom a b c Composition
 data ExId hom a where Source
Existential wrapping of the identity function on a
Constructors
 ExId :: (((a, a), aa) :∈: hom) -> aa -> ExId hom a
 data ExC hom a b c where Source
Existential wrapping of the composition for types a,b,c
Constructors
 ExC :: (((b, c), bc) :∈: hom) -> (((a, b), ab) :∈: hom) -> (((a, c), ac) :∈: hom) -> (bc -> ab -> ac) -> ExC hom a b c
 kleisli :: Monad m => Cat Univ (KleisliHom m) Source
 fromControlCategory :: Category hom => Cat Univ (BiGraph hom) Source
 makeCat :: ((ob :×: ob) :~>: Univ) hom -> (forall a aa. (((a, a), aa) :∈: hom) -> aa) -> (forall a b c bc ab ac. (((b, c), bc) :∈: hom) -> (((a, b), ab) :∈: hom) -> (((a, c), ac) :∈: hom) -> bc -> ab -> ac) -> Cat ob hom Source
Lemma for constructing categories; abstracts the usage of the hom function's total
 idauto :: Fact (a :∈: ob) => Cat ob hom -> ExId hom a Source
 cauto :: (Fact (a :∈: ob), Fact (b :∈: ob), Fact (c :∈: ob)) => Cat ob hom -> ExC hom a b c Source
 data GFunctor ob1 hom1 ob2 hom2 f Source
Constructors
GFunctor
 omapIsFun :: (ob1 :~>: ob2) f getfmap :: forall a b. (a :∈: ob1) -> (b :∈: ob1) -> ExFmap hom1 hom2 f a b
 data ExFmap hom1 hom2 f a b where Source
Constructors
 ExFmap :: ((a, fa) :∈: f) -> ((b, fb) :∈: f) -> (((a, b), ab) :∈: hom1) -> (((fa, fb), fafb) :∈: hom2) -> (ab -> fafb) -> ExFmap hom1 hom2 f a b
 fromFunctor :: Functor f => GFunctor Univ HaskFun Univ HaskFun (Graph f) Source