type-settheory-0.1.2: Type-level sets and functions expressed as types Source code Contents Index

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 hask :: Cat Univ HaskFun 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

hask :: Cat Univ HaskFun Source

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

Produced by Haddock version 2.4.2