{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude #-}
module Data.Category.Comma where
import Data.Category
import Data.Category.Functor
import Data.Category.Limit
import Data.Category.RepresentableFunctor
data CommaO :: * -> * -> * -> * 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 (:/\:) :: * -> * -> * -> * -> * 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)
commaId :: CommaO t s (a, b) -> Obj (t :/\: s) (a, b)
commaId o :: CommaO t s (a, b)
o@(CommaO Obj (Dom t) a
a k (t :% a) (s :% b)
_ Obj (Dom s) b
b) = CommaO t s (a, b)
-> Dom t a a
-> Dom s b b
-> CommaO t s (a, b)
-> Obj (t :/\: s) (a, b)
forall t s a b a' b'.
CommaO t s (a, b)
-> Dom t a a'
-> Dom s b b'
-> CommaO t s (a', b')
-> (:/\:) t s (a, b) (a', b')
CommaA CommaO t s (a, b)
o Dom t a a
Obj (Dom t) a
a Dom s b b
Obj (Dom s) b
b CommaO t s (a, b)
o
instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s) where
src :: (:/\:) t s a b -> Obj (t :/\: s) a
src (CommaA CommaO t s (a, b)
so Dom t a a'
_ Dom s b b'
_ CommaO t s (a', b')
_) = CommaO t s (a, b) -> Obj (t :/\: s) (a, b)
forall t s a b. CommaO t s (a, b) -> Obj (t :/\: s) (a, b)
commaId CommaO t s (a, b)
so
tgt :: (:/\:) t s a b -> Obj (t :/\: s) b
tgt (CommaA CommaO t s (a, b)
_ Dom t a a'
_ Dom s b b'
_ CommaO t s (a', b')
to) = CommaO t s (a', b') -> Obj (t :/\: s) (a', b')
forall t s a b. CommaO t s (a, b) -> Obj (t :/\: s) (a, b)
commaId CommaO t s (a', b')
to
(CommaA CommaO t s (a, b)
_ Dom t a a'
g Dom s b b'
h CommaO t s (a', b')
to) . :: (:/\:) t s b c -> (:/\:) t s a b -> (:/\:) t s a c
. (CommaA CommaO t s (a, b)
so Dom t a a'
g' Dom s b b'
h' CommaO t s (a', b')
_) = CommaO t s (a, b)
-> Dom t a a'
-> Dom s b b'
-> CommaO t s (a', b')
-> (:/\:) t s (a, b) (a', b')
forall t s a b a' b'.
CommaO t s (a, b)
-> Dom t a a'
-> Dom s b b'
-> CommaO t s (a', b')
-> (:/\:) t s (a, b) (a', b')
CommaA CommaO t s (a, b)
so (Dom t a a'
g Dom t a a' -> Dom t a a -> Dom t a a'
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Dom t a a
Dom t a a'
g') (Dom s b b'
h Dom s b b' -> Dom s b b -> Dom s b b'
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Dom s b b
Dom s b b'
h') CommaO t s (a', b')
to
type (f `ObjectsFUnder` a) = ConstF f a :/\: f
type (f `ObjectsFOver` a) = f :/\: ConstF f a
type (c `ObjectsUnder` a) = Id c `ObjectsFUnder` a
type (c `ObjectsOver` a) = Id c `ObjectsFOver` a
type Arrows c = Id c :/\: Id c
initialUniversalComma :: forall u x c a a_
. (Functor u, c ~ (u `ObjectsFUnder` x), HasInitialObject c, (a_, a) ~ InitialObject c)
=> u -> InitialUniversal x u a
initialUniversalComma :: u -> InitialUniversal x u a
initialUniversalComma u
u = case c (a_, a) (a_, a)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject :: Obj c (a_, a) of
CommaA (CommaO _ mor a) _ _ _ ->
u
-> Obj (Dom u) a
-> Cod u x (u :% a)
-> (forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y)
-> InitialUniversal x u a
forall u a x.
Functor u =>
u
-> Obj (Dom u) a
-> Cod u x (u :% a)
-> (forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y)
-> InitialUniversal x u a
initialUniversal u
u Obj (Dom u) a
Obj (Dom u) b
a k (Const (Dom u) (Cod u) x :% a) (u :% b)
Cod u x (u :% a)
mor forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y
factorizer
where
factorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y
factorizer :: Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y
factorizer Obj (Dom u) y
y Cod u x (u :% y)
arr = case (Obj c (y, y) -> c (a_, a) (y, y)
init (CommaO (Const (Dom u) (Cod u) x) u (y, y)
-> Obj (Const (Dom u) (Cod u) x :/\: u) (y, y)
forall t s a b. CommaO t s (a, b) -> Obj (t :/\: s) (a, b)
commaId (Obj (Dom (Const (Dom u) (Cod u) x)) y
-> Cod u (Const (Dom u) (Cod u) x :% y) (u :% y)
-> Obj (Dom u) y
-> CommaO (Const (Dom u) (Cod u) x) u (y, y)
forall t (k :: * -> * -> *) s a b.
(Cod t ~ k, Cod s ~ k) =>
Obj (Dom t) a
-> k (t :% a) (s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)
CommaO Obj (Dom u) y
Obj (Dom (Const (Dom u) (Cod u) x)) y
y Cod u x (u :% y)
Cod u (Const (Dom u) (Cod u) x :% y) (u :% y)
arr Obj (Dom u) y
y))) of CommaA _ _ f _ -> Dom u a y
Dom u b b'
f
where
init :: Obj c (y, y) -> c (a_, a) (y, y)
init :: Obj c (y, y) -> c (a_, a) (y, y)
init = Obj c (y, y) -> c (a_, a) (y, y)
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize
terminalUniversalComma :: forall u x c a a_
. (Functor u, c ~ (u `ObjectsFOver` x), HasTerminalObject c, (a, a_) ~ TerminalObject c)
=> u -> TerminalUniversal x u a
terminalUniversalComma :: u -> TerminalUniversal x u a
terminalUniversalComma u
u = case c (a, a_) (a, a_)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject :: Obj c (a, a_) of
CommaA (CommaO a mor _) _ _ _ ->
u
-> Obj (Dom u) a
-> Cod u (u :% a) x
-> (forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a)
-> TerminalUniversal x u a
forall u a x.
Functor u =>
u
-> Obj (Dom u) a
-> Cod u (u :% a) x
-> (forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a)
-> TerminalUniversal x u a
terminalUniversal u
u Obj (Dom u) a
Obj (Dom u) a
a k (u :% a) (Const (Dom u) (Cod u) x :% b)
Cod u (u :% a) x
mor forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a
factorizer
where
factorizer :: forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a
factorizer :: Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a
factorizer Obj (Dom u) y
y Cod u (u :% y) x
arr = case (Obj c (y, y) -> c (y, y) (a, a_)
term (CommaO u (Const (Dom u) (Cod u) x) (y, y)
-> Obj (u :/\: Const (Dom u) (Cod u) x) (y, y)
forall t s a b. CommaO t s (a, b) -> Obj (t :/\: s) (a, b)
commaId (Obj (Dom u) y
-> Cod u (u :% y) (Const (Dom u) (Cod u) x :% y)
-> Obj (Dom (Const (Dom u) (Cod u) x)) y
-> CommaO u (Const (Dom u) (Cod u) x) (y, y)
forall t (k :: * -> * -> *) s a b.
(Cod t ~ k, Cod s ~ k) =>
Obj (Dom t) a
-> k (t :% a) (s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)
CommaO Obj (Dom u) y
y Cod u (u :% y) x
Cod u (u :% y) (Const (Dom u) (Cod u) x :% y)
arr Obj (Dom u) y
Obj (Dom (Const (Dom u) (Cod u) x)) y
y))) of CommaA _ f _ _ -> Dom u y a
Dom u a a'
f
where
term :: Obj c (y, y) -> c (y, y) (a, a_)
term :: Obj c (y, y) -> c (y, y) (a, a_)
term = Obj c (y, y) -> c (y, y) (a, a_)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate