Data.Category.Comma

Comma categories.

Documentation

data CommaO :: * -> * -> * -> * where

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)

data (:/\:) :: * -> * -> * -> * -> * where

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

(Category (Dom t), Category (Dom s)) => Category (t :/\: s)

The comma category T \downarrow S

Defined in Data.Category.Comma

Methods

src :: (t :/\: s) a b -> Obj (t :/\: s) a

tgt :: (t :/\: s) a b -> Obj (t :/\: s) b

(.) :: (t :/\: s) b c -> (t :/\: s) a b -> (t :/\: s) a c

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