{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Comma
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Comma categories.
-----------------------------------------------------------------------------
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

-- | The comma category T \\downarrow S
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