{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies, TypeOperators, UndecidableInstances, GADTs, FlexibleContexts, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Coproduct
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category.Coproduct where

import Data.Kind (Type)

import Data.Category
import Data.Category.Functor

import Data.Category.NaturalTransformation
import Data.Category.Product
import Data.Category.Unit


data I1 a
data I2 a

data (:++:) :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where
  I1 :: c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
  I2 :: c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)

-- | The coproduct category of categories @c1@ and @c2@.
instance (Category c1, Category c2) => Category (c1 :++: c2) where

  src :: forall a b. (:++:) c1 c2 a b -> Obj (c1 :++: c2) a
src (I1 c1 a1 b1
a)      = forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *).
c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
I1 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src c1 a1 b1
a)
  src (I2 c2 a2 b2
a)      = forall (c2 :: * -> * -> *) a1 b1 (c1 :: * -> * -> *).
c2 a1 b1 -> (:++:) c1 c2 (I2 a1) (I2 b1)
I2 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src c2 a2 b2
a)
  tgt :: forall a b. (:++:) c1 c2 a b -> Obj (c1 :++: c2) b
tgt (I1 c1 a1 b1
a)      = forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *).
c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
I1 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt c1 a1 b1
a)
  tgt (I2 c2 a2 b2
a)      = forall (c2 :: * -> * -> *) a1 b1 (c1 :: * -> * -> *).
c2 a1 b1 -> (:++:) c1 c2 (I2 a1) (I2 b1)
I2 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt c2 a2 b2
a)

  (I1 c1 a1 b1
a) . :: forall b c a.
(:++:) c1 c2 b c -> (:++:) c1 c2 a b -> (:++:) c1 c2 a c
. (I1 c1 a1 b1
b) = forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *).
c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
I1 (c1 a1 b1
a forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. c1 a1 b1
b)
  (I2 c2 a2 b2
a) . (I2 c2 a2 b2
b) = forall (c2 :: * -> * -> *) a1 b1 (c1 :: * -> * -> *).
c2 a1 b1 -> (:++:) c1 c2 (I2 a1) (I2 b1)
I2 (c2 a2 b2
a forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. c2 a2 b2
b)




data Inj1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Inj1
-- | 'Inj1' is a functor which injects into the left category.
instance (Category c1, Category c2) => Functor (Inj1 c1 c2) where
  type Dom (Inj1 c1 c2) = c1
  type Cod (Inj1 c1 c2) = c1 :++: c2
  type Inj1 c1 c2 :% a = I1 a
  Inj1 c1 c2
Inj1 % :: forall a b.
Inj1 c1 c2
-> Dom (Inj1 c1 c2) a b
-> Cod (Inj1 c1 c2) (Inj1 c1 c2 :% a) (Inj1 c1 c2 :% b)
% Dom (Inj1 c1 c2) a b
f = forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *).
c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
I1 Dom (Inj1 c1 c2) a b
f

data Inj2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Inj2
-- | 'Inj2' is a functor which injects into the right category.
instance (Category c1, Category c2) => Functor (Inj2 c1 c2) where
  type Dom (Inj2 c1 c2) = c2
  type Cod (Inj2 c1 c2) = c1 :++: c2
  type Inj2 c1 c2 :% a = I2 a
  Inj2 c1 c2
Inj2 % :: forall a b.
Inj2 c1 c2
-> Dom (Inj2 c1 c2) a b
-> Cod (Inj2 c1 c2) (Inj2 c1 c2 :% a) (Inj2 c1 c2 :% b)
% Dom (Inj2 c1 c2) a b
f = forall (c2 :: * -> * -> *) a1 b1 (c1 :: * -> * -> *).
c2 a1 b1 -> (:++:) c1 c2 (I2 a1) (I2 b1)
I2 Dom (Inj2 c1 c2) a b
f

data f1 :+++: f2 = f1 :+++: f2
-- | @f1 :+++: f2@ is the coproduct of the functors @f1@ and @f2@.
instance (Functor f1, Functor f2) => Functor (f1 :+++: f2) where
  type Dom (f1 :+++: f2) = Dom f1 :++: Dom f2
  type Cod (f1 :+++: f2) = Cod f1 :++: Cod f2
  type (f1 :+++: f2) :% (I1 a) = I1 (f1 :% a)
  type (f1 :+++: f2) :% (I2 a) = I2 (f2 :% a)
  (f1
g :+++: f2
_) % :: forall a b.
(f1 :+++: f2)
-> Dom (f1 :+++: f2) a b
-> Cod (f1 :+++: f2) ((f1 :+++: f2) :% a) ((f1 :+++: f2) :% b)
% I1 Dom f1 a1 b1
f = forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *).
c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
I1 (f1
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f1 a1 b1
f)
  (f1
_ :+++: f2
g) % I2 Dom f2 a2 b2
f = forall (c2 :: * -> * -> *) a1 b1 (c1 :: * -> * -> *).
c2 a1 b1 -> (:++:) c1 c2 (I2 a1) (I2 b1)
I2 (f2
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f2 a2 b2
f)

data CodiagCoprod (k :: Type -> Type -> Type) = CodiagCoprod
-- | 'CodiagCoprod' is the codiagonal functor for coproducts.
instance Category k => Functor (CodiagCoprod k) where
  type Dom (CodiagCoprod k) = k :++: k
  type Cod (CodiagCoprod k) = k
  type CodiagCoprod k :% I1 a = a
  type CodiagCoprod k :% I2 a = a
  CodiagCoprod k
CodiagCoprod % :: forall a b.
CodiagCoprod k
-> Dom (CodiagCoprod k) a b
-> Cod (CodiagCoprod k) (CodiagCoprod k :% a) (CodiagCoprod k :% b)
% I1 k a1 b1
f = k a1 b1
f
  CodiagCoprod k
CodiagCoprod % I2 k a2 b2
f = k a2 b2
f

newtype Cotuple1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) a = Cotuple1 (Obj c1 a)
-- | 'Cotuple1' projects out to the left category, replacing a value from the right category with a fixed object.
instance (Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1) where
  type Dom (Cotuple1 c1 c2 a1) = c1 :++: c2
  type Cod (Cotuple1 c1 c2 a1) = c1
  type Cotuple1 c1 c2 a1 :% I1 a = a
  type Cotuple1 c1 c2 a1 :% I2 a = a1
  Cotuple1 Obj c1 a1
_ % :: forall a b.
Cotuple1 c1 c2 a1
-> Dom (Cotuple1 c1 c2 a1) a b
-> Cod
     (Cotuple1 c1 c2 a1)
     (Cotuple1 c1 c2 a1 :% a)
     (Cotuple1 c1 c2 a1 :% b)
% I1 c1 a1 b1
f = c1 a1 b1
f
  Cotuple1 Obj c1 a1
a % I2 c2 a2 b2
_ = Obj c1 a1
a

newtype Cotuple2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) a = Cotuple2 (Obj c2 a)
-- | 'Cotuple2' projects out to the right category, replacing a value from the left category with a fixed object.
instance (Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2) where
  type Dom (Cotuple2 c1 c2 a2) = c1 :++: c2
  type Cod (Cotuple2 c1 c2 a2) = c2
  type Cotuple2 c1 c2 a2 :% I1 a = a2
  type Cotuple2 c1 c2 a2 :% I2 a = a
  Cotuple2 Obj c2 a2
a % :: forall a b.
Cotuple2 c1 c2 a2
-> Dom (Cotuple2 c1 c2 a2) a b
-> Cod
     (Cotuple2 c1 c2 a2)
     (Cotuple2 c1 c2 a2 :% a)
     (Cotuple2 c1 c2 a2 :% b)
% I1 c1 a1 b1
_ = Obj c2 a2
a
  Cotuple2 Obj c2 a2
_ % I2 c2 a2 b2
f = c2 a2 b2
f


data Cograph c d f :: Type -> Type -> Type where
  I1A :: c a1 b1 -> Cograph c d f (I1 a1) (I1 b1)
  I2A :: d a2 b2 -> Cograph c d f (I2 a2) (I2 b2)
  I12 :: Obj c a -> Obj d b -> f -> f :% (a, b) -> Cograph c d f (I1 a) (I2 b)

-- | The cograph of the profunctor @f@.
instance ProfunctorOf c d f => Category (Cograph c d f) where

  src :: forall a b. Cograph c d f a b -> Obj (Cograph c d f) a
src (I1A c a1 b1
a)       = forall (c :: * -> * -> *) a1 b1 (d :: * -> * -> *) f.
c a1 b1 -> Cograph c d f (I1 a1) (I1 b1)
I1A (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src c a1 b1
a)
  src (I2A d a2 b2
a)       = forall (d :: * -> * -> *) a1 b1 (c :: * -> * -> *) f.
d a1 b1 -> Cograph c d f (I2 a1) (I2 b1)
I2A (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src d a2 b2
a)
  src (I12 Obj c a
a Obj d b
_ f
_ f :% (a, b)
_) = forall (c :: * -> * -> *) a1 b1 (d :: * -> * -> *) f.
c a1 b1 -> Cograph c d f (I1 a1) (I1 b1)
I1A Obj c a
a
  tgt :: forall a b. Cograph c d f a b -> Obj (Cograph c d f) b
tgt (I1A c a1 b1
a)       = forall (c :: * -> * -> *) a1 b1 (d :: * -> * -> *) f.
c a1 b1 -> Cograph c d f (I1 a1) (I1 b1)
I1A (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt c a1 b1
a)
  tgt (I2A d a2 b2
a)       = forall (d :: * -> * -> *) a1 b1 (c :: * -> * -> *) f.
d a1 b1 -> Cograph c d f (I2 a1) (I2 b1)
I2A (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt d a2 b2
a)
  tgt (I12 Obj c a
_ Obj d b
b f
_ f :% (a, b)
_) = forall (d :: * -> * -> *) a1 b1 (c :: * -> * -> *) f.
d a1 b1 -> Cograph c d f (I2 a1) (I2 b1)
I2A Obj d b
b

  (I1A c a1 b1
a) . :: forall b c a.
Cograph c d f b c -> Cograph c d f a b -> Cograph c d f a c
. (I1A c a1 b1
b) = forall (c :: * -> * -> *) a1 b1 (d :: * -> * -> *) f.
c a1 b1 -> Cograph c d f (I1 a1) (I1 b1)
I1A (c a1 b1
a forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. c a1 b1
b)
  (I12 Obj c a
_ Obj d b
b f
f f :% (a, b)
ab) . (I1A c a1 b1
a) = forall (c :: * -> * -> *) a1 (d :: * -> * -> *) b1 f.
Obj c a1
-> Obj d b1
-> f
-> (f :% (a1, b1))
-> Cograph c d f (I1 a1) (I2 b1)
I12 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src c a1 b1
a) Obj d b
b f
f ((f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op c a1 b1
a forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj d b
b)) f :% (a, b)
ab)
  (I2A d a2 b2
b) . (I12 Obj c a
a Obj d b
_ f
f f :% (a, b)
ab) = forall (c :: * -> * -> *) a1 (d :: * -> * -> *) b1 f.
Obj c a1
-> Obj d b1
-> f
-> (f :% (a1, b1))
-> Cograph c d f (I1 a1) (I2 b1)
I12 Obj c a
a (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt d a2 b2
b) f
f ((f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Obj c a
a forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: d a2 b2
b)) f :% (a, b)
ab)
  (I2A d a2 b2
a) . (I2A d a2 b2
b) = forall (d :: * -> * -> *) a1 b1 (c :: * -> * -> *) f.
d a1 b1 -> Cograph c d f (I2 a1) (I2 b1)
I2A (d a2 b2
a forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. d a2 b2
b)

-- | The directed coproduct category of categories @c1@ and @c2@.
newtype (c1 :>>: c2) a b = DC (Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b) deriving forall a b. (:>>:) c1 c2 a b -> Obj (c1 :>>: c2) a
forall a b. (:>>:) c1 c2 a b -> Obj (c1 :>>: c2) b
forall b c a.
(:>>:) c1 c2 b c -> (:>>:) c1 c2 a b -> (:>>:) c1 c2 a c
forall {k} (k :: k -> k -> *).
(forall (a :: k) (b :: k). k a b -> Obj k a)
-> (forall (a :: k) (b :: k). k a b -> Obj k b)
-> (forall (b :: k) (c :: k) (a :: k). k b c -> k a b -> k a c)
-> Category k
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
(Category c1, Category c2) =>
(:>>:) c1 c2 a b -> Obj (c1 :>>: c2) a
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
(Category c1, Category c2) =>
(:>>:) c1 c2 a b -> Obj (c1 :>>: c2) b
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) b c a.
(Category c1, Category c2) =>
(:>>:) c1 c2 b c -> (:>>:) c1 c2 a b -> (:>>:) c1 c2 a c
. :: forall b c a.
(:>>:) c1 c2 b c -> (:>>:) c1 c2 a b -> (:>>:) c1 c2 a c
$c. :: forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) b c a.
(Category c1, Category c2) =>
(:>>:) c1 c2 b c -> (:>>:) c1 c2 a b -> (:>>:) c1 c2 a c
tgt :: forall a b. (:>>:) c1 c2 a b -> Obj (c1 :>>: c2) b
$ctgt :: forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
(Category c1, Category c2) =>
(:>>:) c1 c2 a b -> Obj (c1 :>>: c2) b
src :: forall a b. (:>>:) c1 c2 a b -> Obj (c1 :>>: c2) a
$csrc :: forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
(Category c1, Category c2) =>
(:>>:) c1 c2 a b -> Obj (c1 :>>: c2) a
Category


newtype NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)

-- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@.
instance (Functor f, Functor g, Dom f ~ Dom g, Cod f ~ Cod g) => Functor (NatAsFunctor f g) where

  type Dom (NatAsFunctor f g) = Dom f :**: Cograph Unit Unit (Hom Unit)
  type Cod (NatAsFunctor f g) = Cod f
  type NatAsFunctor f g :% (a, I1 ()) = f :% a
  type NatAsFunctor f g :% (a, I2 ()) = g :% a

  NatAsFunctor (Nat f
f g
_ forall z. Obj (Dom f) z -> Component f g z
_) % :: forall a b.
NatAsFunctor f g
-> Dom (NatAsFunctor f g) a b
-> Cod
     (NatAsFunctor f g) (NatAsFunctor f g :% a) (NatAsFunctor f g :% b)
% (Dom g a1 b1
a :**: I1A Unit a1 b1
Unit) = f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom g a1 b1
a
  NatAsFunctor (Nat f
_ g
g forall z. Obj (Dom f) z -> Component f g z
_) % (Dom g a1 b1
a :**: I2A Unit a2 b2
Unit) = g
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom g a1 b1
a
  NatAsFunctor Nat (Dom f) (Cod f) f g
n           % (Dom g a1 b1
a :**: I12 Unit a a
Unit Unit b b
Unit Hom Unit
Hom Hom Unit :% (a, b)
Unit () ()
Unit) = Nat (Dom f) (Cod f) f g
n forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Dom g a1 b1
a