License	BSD-style (see the file LICENSE)
Maintainer	sjoerd@w3future.com
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Category.Comma

Description

Comma categories.

Synopsis

data CommaO :: Type -> Type -> Type -> Type where
- CommaO :: (Cod t ~ k, Cod s ~ k) => Obj (Dom t) a -> k (t :% a) (s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)
data (:/\:) :: Type -> Type -> Type -> Type -> Type where
- CommaA :: CommaO t s (a, b) -> Dom t a a' -> Dom s b b' -> CommaO t s (a', b') -> (t :/\: s) (a, b) (a', b')
commaId :: CommaO t s (a, b) -> Obj (t :/\: s) (a, b)
type ObjectsFUnder f a = ConstF f a :/\: f
type ObjectsFOver f a = f :/\: ConstF f a
type ObjectsUnder c a = Id c `ObjectsFUnder` a
type ObjectsOver c a = Id c `ObjectsFOver` a
initialUniversalComma :: forall u x c a a_. (Functor u, c ~ (u `ObjectsFUnder` x), HasInitialObject c, (a_, a) ~ InitialObject c) => u -> InitialUniversal x u a
terminalUniversalComma :: forall u x c a a_. (Functor u, c ~ (u `ObjectsFOver` x), HasTerminalObject c, (a, a_) ~ TerminalObject c) => u -> TerminalUniversal x u a
type Arrows k = Id k :/\: Id k
data IdArrow (k :: Type -> Type -> Type) = IdArrow
data Src (k :: Type -> Type -> Type) = Src
data Tgt (k :: Type -> Type -> Type) = Tgt
tgtIdAdj :: Category k => Adjunction k (Arrows k) (Tgt k) (IdArrow k)
idSrcAdj :: Category k => Adjunction (Arrows k) k (IdArrow k) (Src k)

Documentation

Constructors

CommaO :: (Cod t ~ k, Cod s ~ k) => Obj (Dom t) a -> k (t :% a) (s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)

Constructors

CommaA :: CommaO t s (a, b) -> Dom t a a' -> Dom s b b' -> CommaO t s (a', b') -> (t :/\: s) (a, b) (a', b')

Instances details

(Category (Dom t), Category (Dom s)) => Category (t :/\: s :: Type -> Type -> Type) Source #	The comma category T \downarrow S
Instance details Defined in Data.Category.Comma Methods src :: forall (a :: k) (b :: k). (t :/\: s) a b -> Obj (t :/\: s) a Source # tgt :: forall (a :: k) (b :: k). (t :/\: s) a b -> Obj (t :/\: s) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). (t :/\: s) b c -> (t :/\: s) a b -> (t :/\: s) a c Source #

commaId :: CommaO t s (a, b) -> Obj (t :/\: s) (a, b) Source #

Constructors

Instances details

Category k => Functor (IdArrow k) Source #
Instance details Defined in Data.Category.Comma Associated Types type Dom (IdArrow k) :: Type -> Type -> Type Source # type Cod (IdArrow k) :: Type -> Type -> Type Source # type (IdArrow k) :% a Source # Methods (%) :: IdArrow k -> Dom (IdArrow k) a b -> Cod (IdArrow k) (IdArrow k :% a) (IdArrow k :% b) Source #
type Cod (IdArrow k) Source #
Instance details Defined in Data.Category.Comma type Cod (IdArrow k) = Arrows k
type Dom (IdArrow k) Source #
Instance details Defined in Data.Category.Comma type Dom (IdArrow k) = k
type (IdArrow k) :% a Source #
Instance details Defined in Data.Category.Comma type (IdArrow k) :% a = (a, a)

data Src (k :: Type -> Type -> Type) Source #

Constructors

Instances details

Category k => Functor (Src k) Source #
Instance details Defined in Data.Category.Comma Associated Types type Dom (Src k) :: Type -> Type -> Type Source # type Cod (Src k) :: Type -> Type -> Type Source # type (Src k) :% a Source # Methods (%) :: Src k -> Dom (Src k) a b -> Cod (Src k) (Src k :% a) (Src k :% b) Source #
type Cod (Src k) Source #
Instance details Defined in Data.Category.Comma type Cod (Src k) = k
type Dom (Src k) Source #
Instance details Defined in Data.Category.Comma type Dom (Src k) = Arrows k
type (Src k) :% (a, b) Source #
Instance details Defined in Data.Category.Comma type (Src k) :% (a, b) = a

data Tgt (k :: Type -> Type -> Type) Source #

Constructors

Instances details

Category k => Functor (Tgt k) Source #
Instance details Defined in Data.Category.Comma Associated Types type Dom (Tgt k) :: Type -> Type -> Type Source # type Cod (Tgt k) :: Type -> Type -> Type Source # type (Tgt k) :% a Source # Methods (%) :: Tgt k -> Dom (Tgt k) a b -> Cod (Tgt k) (Tgt k :% a) (Tgt k :% b) Source #
type Cod (Tgt k) Source #
Instance details Defined in Data.Category.Comma type Cod (Tgt k) = k
type Dom (Tgt k) Source #
Instance details Defined in Data.Category.Comma type Dom (Tgt k) = Arrows k
type (Tgt k) :% (a, b) Source #
Instance details Defined in Data.Category.Comma type (Tgt k) :% (a, b) = b

Taking the target of an arrow is left adjoint to taking the identity of an object

Taking the source of an arrow is right adjoint to taking the identity of an object