{-# 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.Kind (Type)

import Data.Category
import Data.Category.Adjunction
import Data.Category.Functor
import Data.Category.Limit
import Data.Category.RepresentableFunctor


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)
commaId :: forall t s a b. 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) = forall t s k a b b'.
CommaO t s (k, a)
-> Dom t k b
-> Dom s a b'
-> CommaO t s (b, b')
-> (:/\:) t s (k, a) (b, b')
CommaA CommaO t s (a, b)
o Obj (Dom t) a
a 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 :: forall a b. (:/\:) 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')
_) = forall t s a b. CommaO t s (a, b) -> Obj (t :/\: s) (a, b)
commaId CommaO t s (a, b)
so
  tgt :: forall a b. (:/\:) 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) = 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) . :: forall b c a. (:/\:) 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')
_) = forall t s k a b b'.
CommaO t s (k, a)
-> Dom t k b
-> Dom s a b'
-> CommaO t s (b, b')
-> (:/\:) t s (k, a) (b, b')
CommaA CommaO t s (a, b)
so (Dom t a a'
g 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'
g') (Dom s b b'
h 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'
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


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 :: forall u x (c :: * -> * -> *) a a_.
(Functor u, c ~ ObjectsFUnder u x, HasInitialObject c,
 (a_, a) ~ InitialObject c) =>
u -> InitialUniversal x u a
initialUniversalComma u
u = case forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject :: Obj c (a_, a) of
  CommaA (CommaO Obj (Dom (Const (Dom u) (Cod u) x)) a
_ k (Const (Dom u) (Cod u) x :% a) (u :% b)
mor Obj (Dom u) b
a) Dom (Const (Dom u) (Cod u) x) a a'
_ Dom u b b'
_ CommaO (Const (Dom u) (Cod u) x) u (a', b')
_ ->
    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) b
a k (Const (Dom u) (Cod u) x :% a) (u :% b)
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 :: forall y. 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 (forall t s a b. CommaO t s (a, b) -> Obj (t :/\: s) (a, b)
commaId (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 x (u :% y)
arr Obj (Dom u) y
y)) of CommaA CommaO (Const (Dom u) k x) u (a, b)
_ Dom (Const (Dom u) k x) a a'
_ Dom u b b'
f CommaO (Const (Dom u) k x) u (a', b')
_ -> 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 = 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 :: forall u x (c :: * -> * -> *) a a_.
(Functor u, c ~ ObjectsFOver u x, HasTerminalObject c,
 (a, a_) ~ TerminalObject c) =>
u -> TerminalUniversal x u a
terminalUniversalComma u
u = case forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject :: Obj c (a, a_) of
  CommaA (CommaO Obj (Dom u) a
a k (u :% a) (Const (Dom u) (Cod u) x :% b)
mor Obj (Dom (Const (Dom u) (Cod u) x)) b
_) Dom u a a'
_ Dom (Const (Dom u) (Cod u) x) b b'
_ CommaO u (Const (Dom u) (Cod u) x) (a', b')
_ ->
    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
a k (u :% a) (Const (Dom u) (Cod u) x :% b)
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 :: forall y. 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 (forall t s a b. CommaO t s (a, b) -> Obj (t :/\: s) (a, b)
commaId (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
arr Obj (Dom u) y
y)) of CommaA CommaO u (Const (Dom u) k x) (a, b)
_ Dom u a a'
f Dom (Const (Dom u) k x) b b'
_ CommaO u (Const (Dom u) k x) (a', b')
_ -> 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 = forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate


type Arrows k = Id k :/\: Id k

data IdArrow (k :: Type -> Type -> Type) = IdArrow
instance Category k => Functor (IdArrow k) where
  type Dom (IdArrow k) = k
  type Cod (IdArrow k) = Arrows k
  type IdArrow k :% a = (a, a)
  IdArrow k
IdArrow % :: forall a b.
IdArrow k
-> Dom (IdArrow k) a b
-> Cod (IdArrow k) (IdArrow k :% a) (IdArrow k :% b)
% Dom (IdArrow k) a b
f = forall t s k a b b'.
CommaO t s (k, a)
-> Dom t k b
-> Dom s a b'
-> CommaO t s (b, b')
-> (:/\:) t s (k, a) (b, b')
CommaA
    (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 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Dom (IdArrow k) a b
f) (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Dom (IdArrow k) a b
f) (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Dom (IdArrow k) a b
f))
    Dom (IdArrow k) a b
f
    Dom (IdArrow k) a b
f
    (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 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (IdArrow k) a b
f) (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (IdArrow k) a b
f) (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (IdArrow k) a b
f))

data Src (k :: Type -> Type -> Type) = Src
instance Category k => Functor (Src k) where
  type Dom (Src k) = Arrows k
  type Cod (Src k) = k
  type Src k :% (a, b) = a
  Src k
Src % :: forall a b.
Src k -> Dom (Src k) a b -> Cod (Src k) (Src k :% a) (Src k :% b)
% (CommaA CommaO (Id k) (Id k) (a, b)
_ Dom (Id k) a a'
aa' Dom (Id k) b b'
_ CommaO (Id k) (Id k) (a', b')
_) = Dom (Id k) a a'
aa'

data Tgt (k :: Type -> Type -> Type) = Tgt
instance Category k => Functor (Tgt k) where
  type Dom (Tgt k) = Arrows k
  type Cod (Tgt k) = k
  type Tgt k :% (a, b) = b
  Tgt k
Tgt % :: forall a b.
Tgt k -> Dom (Tgt k) a b -> Cod (Tgt k) (Tgt k :% a) (Tgt k :% b)
% (CommaA CommaO (Id k) (Id k) (a, b)
_ Dom (Id k) a a'
_ Dom (Id k) b b'
bb' CommaO (Id k) (Id k) (a', b')
_) = Dom (Id k) b b'
bb'

-- | Taking the target of an arrow is left adjoint to taking the identity of an object
tgtIdAdj :: Category k => Adjunction k (Arrows k) (Tgt k) (IdArrow k)
tgtIdAdj :: forall (k :: * -> * -> *).
Category k =>
Adjunction k (Arrows k) (Tgt k) (IdArrow k)
tgtIdAdj = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionUnits forall (k :: * -> * -> *). Tgt k
Tgt forall (k :: * -> * -> *). IdArrow k
IdArrow (\(CommaA o :: CommaO (Id k) (Id k) (a, b)
o@(CommaO Obj (Dom (Id k)) a
_ k (Id k :% a) (Id k :% b)
ab Obj (Dom (Id k)) b
b) Dom (Id k) a a'
_ Dom (Id k) b b'
_ CommaO (Id k) (Id k) (a', b')
_) -> forall t s k a b b'.
CommaO t s (k, a)
-> Dom t k b
-> Dom s a b'
-> CommaO t s (b, b')
-> (:/\:) t s (k, a) (b, b')
CommaA CommaO (Id k) (Id k) (a, b)
o k (Id k :% a) (Id k :% b)
ab Obj (Dom (Id k)) b
b (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 (Id k)) b
b Obj (Dom (Id k)) b
b Obj (Dom (Id k)) b
b)) (\Obj k a
o -> Obj k a
o)

-- | Taking the source of an arrow is right adjoint to taking the identity of an object
idSrcAdj :: Category k => Adjunction (Arrows k) k (IdArrow k) (Src k)
idSrcAdj :: forall (k :: * -> * -> *).
Category k =>
Adjunction (Arrows k) k (IdArrow k) (Src k)
idSrcAdj = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionUnits forall (k :: * -> * -> *). IdArrow k
IdArrow forall (k :: * -> * -> *). Src k
Src (\Obj k a
o -> Obj k a
o) (\(CommaA o :: CommaO (Id k) (Id k) (a, b)
o@(CommaO Obj (Dom (Id k)) a
a k (Id k :% a) (Id k :% b)
ab Obj (Dom (Id k)) b
_) Dom (Id k) a a'
_ Dom (Id k) b b'
_ CommaO (Id k) (Id k) (a', b')
_) -> forall t s k a b b'.
CommaO t s (k, a)
-> Dom t k b
-> Dom s a b'
-> CommaO t s (b, b')
-> (:/\:) t s (k, a) (b, b')
CommaA (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 (Id k)) a
a Obj (Dom (Id k)) a
a Obj (Dom (Id k)) a
a) Obj (Dom (Id k)) a
a k (Id k :% a) (Id k :% b)
ab CommaO (Id k) (Id k) (a, b)
o)