{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies, TypeOperators, UndecidableInstances, GADTs, FlexibleContexts, NoImplicitPrelude #-}
module Data.Category.Coproduct where
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 (:++:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
I1 :: c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
I2 :: c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)
instance (Category c1, Category c2) => Category (c1 :++: c2) where
src :: (:++:) c1 c2 a b -> Obj (c1 :++: c2) a
src (I1 c1 a1 b1
a) = c1 a1 a1 -> (:++:) c1 c2 (I1 a1) (I1 a1)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *).
c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
I1 (c1 a1 b1 -> c1 a1 a1
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) = c2 a2 a2 -> (:++:) c1 c2 (I2 a2) (I2 a2)
forall (c2 :: * -> * -> *) a2 b2 (c1 :: * -> * -> *).
c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)
I2 (c2 a2 b2 -> c2 a2 a2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src c2 a2 b2
a)
tgt :: (:++:) c1 c2 a b -> Obj (c1 :++: c2) b
tgt (I1 c1 a1 b1
a) = c1 b1 b1 -> (:++:) c1 c2 (I1 b1) (I1 b1)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *).
c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
I1 (c1 a1 b1 -> c1 b1 b1
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) = c2 b2 b2 -> (:++:) c1 c2 (I2 b2) (I2 b2)
forall (c2 :: * -> * -> *) a2 b2 (c1 :: * -> * -> *).
c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)
I2 (c2 a2 b2 -> c2 b2 b2
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) . :: (:++:) c1 c2 b c -> (:++:) c1 c2 a b -> (:++:) c1 c2 a c
. (I1 c1 a1 b1
b) = c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *).
c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
I1 (c1 a1 b1
a c1 a1 b1 -> c1 a1 a1 -> c1 a1 b1
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. c1 a1 a1
c1 a1 b1
b)
(I2 c2 a2 b2
a) . (I2 c2 a2 b2
b) = c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)
forall (c2 :: * -> * -> *) a2 b2 (c1 :: * -> * -> *).
c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)
I2 (c2 a2 b2
a c2 a2 b2 -> c2 a2 a2 -> c2 a2 b2
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. c2 a2 a2
c2 a2 b2
b)
data Inj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj1
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 % :: 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 = c1 a b -> (:++:) c1 c2 (I1 a) (I1 b)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *).
c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
I1 c1 a b
Dom (Inj1 c1 c2) a b
f
data Inj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj2
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 % :: 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 = c2 a b -> (:++:) c1 c2 (I2 a) (I2 b)
forall (c2 :: * -> * -> *) a2 b2 (c1 :: * -> * -> *).
c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)
I2 c2 a b
Dom (Inj2 c1 c2) a b
f
data f1 :+++: f2 = f1 :+++: 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
_) % :: (f1 :+++: f2)
-> Dom (f1 :+++: f2) a b
-> Cod (f1 :+++: f2) ((f1 :+++: f2) :% a) ((f1 :+++: f2) :% b)
% I1 f = Cod f1 (f1 :% a1) (f1 :% b1)
-> (:++:) (Cod f1) (Cod f2) (I1 (f1 :% a1)) (I1 (f1 :% b1))
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *).
c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
I1 (f1
g f1 -> Dom f1 a1 b1 -> Cod f1 (f1 :% a1) (f1 :% b1)
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 f = Cod f2 (f2 :% a2) (f2 :% b2)
-> (:++:) (Cod f1) (Cod f2) (I2 (f2 :% a2)) (I2 (f2 :% b2))
forall (c2 :: * -> * -> *) a2 b2 (c1 :: * -> * -> *).
c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)
I2 (f2
g f2 -> Dom f2 a2 b2 -> Cod f2 (f2 :% a2) (f2 :% b2)
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 :: * -> * -> *) = CodiagCoprod
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 % :: CodiagCoprod k
-> Dom (CodiagCoprod k) a b
-> Cod (CodiagCoprod k) (CodiagCoprod k :% a) (CodiagCoprod k :% b)
% I1 f = k a1 b1
Cod (CodiagCoprod k) (CodiagCoprod k :% a) (CodiagCoprod k :% b)
f
CodiagCoprod k
CodiagCoprod % I2 f = k a2 b2
Cod (CodiagCoprod k) (CodiagCoprod k :% a) (CodiagCoprod k :% b)
f
data Cotuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple1 (Obj c1 a)
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
_ % :: 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 f = c1 a1 b1
Cod
(Cotuple1 c1 c2 a1)
(Cotuple1 c1 c2 a1 :% a)
(Cotuple1 c1 c2 a1 :% b)
f
Cotuple1 Obj c1 a1
a % I2 _ = Obj c1 a1
Cod
(Cotuple1 c1 c2 a1)
(Cotuple1 c1 c2 a1 :% a)
(Cotuple1 c1 c2 a1 :% b)
a
data Cotuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple2 (Obj c2 a)
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 % :: 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 _ = Obj c2 a2
Cod
(Cotuple2 c1 c2 a2)
(Cotuple2 c1 c2 a2 :% a)
(Cotuple2 c1 c2 a2 :% b)
a
Cotuple2 Obj c2 a2
_ % I2 f = c2 a2 b2
Cod
(Cotuple2 c1 c2 a2)
(Cotuple2 c1 c2 a2 :% a)
(Cotuple2 c1 c2 a2 :% b)
f
data Cograph f :: * -> * -> * where
I1A :: Dom f ~ (Op c :**: d) => c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I2A :: Dom f ~ (Op c :**: d) => d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I12 :: Dom f ~ (Op c :**: d) => Obj c a -> Obj d b -> f -> f :% (a, b) -> Cograph f (I1 a) (I2 b)
instance (Functor f, Dom f ~ (Op c :**: d), Cod f ~ (->), Category c, Category d) => Category (Cograph f) where
src :: Cograph f a b -> Obj (Cograph f) a
src (I1A c a1 b1
a) = c a1 a1 -> Cograph f (I1 a1) (I1 a1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (c a1 b1 -> c a1 a1
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) = d a2 a2 -> Cograph f (I2 a2) (I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (d a2 b2 -> d a2 a2
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)
_) = Obj c a -> Cograph f (I1 a) (I1 a)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A Obj c a
a
tgt :: Cograph f a b -> Obj (Cograph f) b
tgt (I1A c a1 b1
a) = c b1 b1 -> Cograph f (I1 b1) (I1 b1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (c a1 b1 -> c b1 b1
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) = d b2 b2 -> Cograph f (I2 b2) (I2 b2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (d a2 b2 -> d b2 b2
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)
_) = Obj d b -> Cograph f (I2 b) (I2 b)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A Obj d b
b
(I1A c a1 b1
a) . :: Cograph f b c -> Cograph f a b -> Cograph f a c
. (I1A c a1 b1
b) = c a1 b1 -> Cograph f (I1 a1) (I1 b1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (c a1 b1
a c a1 b1 -> c a1 a1 -> c a1 b1
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. c a1 a1
c a1 b1
b)
(I12 Obj c a
_ Obj d b
b f
f f :% (a, b)
ab) . (I1A c a1 b1
a) = Obj c a1
-> Obj d b -> f -> (f :% (a1, b)) -> Cograph f (I1 a1) (I2 b)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 (c a1 b1 -> Obj c a1
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 f -> Dom f (a, b) (a1, b) -> Cod f (f :% (a, b)) (f :% (a1, b))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (c a1 b1 -> Op c b1 a1
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op c a1 b1
a Op c b1 a1 -> Obj d b -> (:**:) (Op c) d (b1, b) (a1, b)
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) = Obj c a
-> Obj d b2 -> f -> (f :% (a, b2)) -> Cograph f (I1 a) (I2 b2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj c a
a (d a2 b2 -> Obj d b2
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 f -> Dom f (a, a2) (a, b2) -> Cod f (f :% (a, a2)) (f :% (a, b2))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Obj c a -> Op c a a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op Obj c a
a Op c a a -> d a2 b2 -> (:**:) (Op c) d (a, a2) (a, b2)
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, a2)
f :% (a, b)
ab)
(I2A d a2 b2
a) . (I2A d a2 b2
b) = d a2 b2 -> Cograph f (I2 a2) (I2 b2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (d a2 b2
a d a2 b2 -> d a2 a2 -> d a2 b2
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. d a2 a2
d a2 b2
b)
newtype (c1 :>>: c2) a b = DC (Cograph (Const (Op c1 :**: c2) (->) ()) a b) deriving (:>>:) c1 c2 a b -> Obj (c1 :>>: c2) a
(:>>:) c1 c2 a b -> Obj (c1 :>>: c2) b
(:>>:) c1 c2 b c -> (:>>:) c1 c2 a b -> (:>>:) c1 c2 a c
(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)
-> Category (c1 :>>: c2)
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
. :: (:>>:) 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 :: (:>>:) 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 :: (:>>:) 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
data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)
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 (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
_) % :: NatAsFunctor f g
-> Dom (NatAsFunctor f g) a b
-> Cod
(NatAsFunctor f g) (NatAsFunctor f g :% a) (NatAsFunctor f g :% b)
% (a :**: I1A Unit) = f
f f -> Dom f a1 b1 -> Cod f (f :% a1) (f :% b1)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f a1 b1
Dom g a1 b1
a
NatAsFunctor (Nat f
_ g
g forall z. Obj (Dom f) z -> Component f g z
_) % (a :**: I2A Unit) = g
g g -> Dom g a1 b1 -> Cod g (g :% a1) (g :% b1)
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 % (a :**: I12 Unit Unit Hom Unit) = Nat (Dom f) (Cod f) f g
Nat (Dom g) (Cod g) f g
n Nat (Dom g) (Cod g) f g -> Dom g a1 b1 -> Cod g (f :% a1) (g :% b1)
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