packages feed

extended-categories 0.1.0 → 0.2.0

raw patch · 16 files changed

+453/−133 lines, 16 files

Files

+ Adjoint.hs view
@@ -0,0 +1,47 @@+module Adjoint where++import Data.Constraint+import Data.Proxy+import Data.Tagged++import Category+import Category.Product+import Functor+import Functor.Product+import NatTr++class (FunctorOf f c1 c2, FunctorOf g c2 c1) => Adjoint (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) f g | f -> c1, f -> c2, g -> c1, g -> c2 where+    leftAdjunct :: NatTr (Op c1 :><: c2) (->)+        (Comp ('KProxy :: KProxy (o2, o2)) (Hom c2) (Dual f :***: IdentityF c2))+        (Comp ('KProxy :: KProxy (o1, o1)) (Hom c1) (IdentityF (Op c1) :***: g))+    rightAdjunct :: NatTr (Op c1 :><: c2) (->)+        (Comp ('KProxy :: KProxy (o1, o1)) (Hom c1) (IdentityF (Op c1) :***: g))+        (Comp ('KProxy :: KProxy (o2, o2)) (Hom c2) (Dual f :***: IdentityF c2))++phiL :: forall (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) f g (x :: o1) (w :: o2).+    (Adjoint c1 c2 f g, Object c1 x) => Tagged '(f, g) (c2 (FMap f x) w -> c1 x (FMap g w))+phiL = Tagged f where+    f m | Dict <- observeObjects m = proxy morphMap (Proxy :: Proxy (AppNat '(x, w) (Op c1 :><: c2) (->))) adj m+    adj :: NatTr (Op c1 :><: c2) (->)+        (Comp ('KProxy :: KProxy (o2, o2)) (Hom c2) (Dual f :***: IdentityF c2))+        (Comp ('KProxy :: KProxy (o1, o1)) (Hom c1) (IdentityF (Op c1) :***: g))+    adj = leftAdjunct++phiR :: forall (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) f g (x :: o1) (w :: o2).+    (Adjoint c1 c2 f g, Object c2 w) => Tagged '(f, g) (c1 x (FMap g w) -> c2 (FMap f x) w)+phiR = Tagged f where+    f m | Dict <- observeObjects m = proxy morphMap (Proxy :: Proxy (AppNat '(x, w) (Op c1 :><: c2) (->))) adj m+    adj :: NatTr (Op c1 :><: c2) (->)+        (Comp ('KProxy :: KProxy (o1, o1)) (Hom c1) (IdentityF (Op c1) :***: g))+        (Comp ('KProxy :: KProxy (o2, o2)) (Hom c2) (Dual f :***: IdentityF c2))+    adj = rightAdjunct++unit :: forall c1 (c2 :: o2 -> o2 -> *) f g. Adjoint c1 c2 f g => NatTr c1 c1 (IdentityF c1) (Comp ('KProxy :: KProxy o2) g f)+unit = NatTr t where+    t :: forall x. Object c1 x => Tagged x (c1 x (FMap g (FMap f x :: o2)))+    t = Tagged (proxy phiL (Proxy :: Proxy '(f, g)) (id :: c2 (FMap f x) (FMap f x))) \\ proxy objectMap (Proxy :: Proxy '(f, x))++counit :: forall (c1 :: o1 -> o1 -> *) c2 f g. Adjoint c1 c2 f g => NatTr c2 c2 (Comp ('KProxy :: KProxy o1) f g) (IdentityF c2)+counit = NatTr t where+    t :: forall y. Object c2 y => Tagged y (c2 (FMap f (FMap g y :: o1)) y)+    t = Tagged (proxy phiR (Proxy :: Proxy '(f, g)) (id :: c1 (FMap g y) (FMap g y))) \\ proxy objectMap (Proxy :: Proxy '(g, y))
Category.hs view
@@ -30,3 +30,12 @@     id = refl     observeObjects = P.const Dict     (.) = trans++-- |Dual categories+newtype Op c a b = Op {unOp :: c b a}++instance Category c => Category (Op c) where+    id = Op id+    (Op f) . (Op g) = Op (g . f)+    type Object (Op c) a = Object c a+    observeObjects (Op c) = case observeObjects c of Dict -> Dict
Category/Product.hs view
@@ -1,11 +1,8 @@ module Category.Product where  import Data.Constraint-import Data.Proxy-import Data.Tagged  import Category-import Functor  data (c1 :><: c2) a b where     (:><:) :: (a ~ '(L a, R a), b ~ '(L b, R b))  => c1 (L a) (L b) -> c2 (R a) (R b) -> (c1 :><: c2) a b@@ -19,11 +16,3 @@     observeObjects (f :><: g)         | Dict <- observeObjects f, Dict <- observeObjects g = Dict     (f1 :><: f2) . (g1 :><: g2) = (f1 . g1) :><: (f2 . g2)--data Diag c where Diag :: Category c => Diag c--instance Category c => Functor (Diag (c :: k -> k -> *)) ('KProxy :: KProxy (k -> (k, k))) where-    type Domain (Diag c) = c-    type Codomain (Diag c) = c :><: c-    type FMap (Diag c) (a :: k) = '(a, a)-    morphMap = Tagged (\f -> f :><: f)
+ Coproduct.hs view
@@ -0,0 +1,38 @@+module Coproduct where++import qualified Prelude as P+import Data.Constraint+import Data.Tagged+import Data.Proxy++import Adjoint+import Category+import Category.Product+import Functor+import Functor.Product+import NatTr++data CoproductF (c :: o -> o -> *) where CoproductF :: CoproductCategory c => CoproductF c+class Adjoint (c :><: c) c (CoproductF c) (Diag c) => CoproductCategory c+type Coproduct c a b = FMap (CoproductF c) '(a, b)++inj1 :: CoproductCategory c => NatTr (c :><: c) c (Proj1 c c) (CoproductF c)+inj1 = idL . compFR retractProj1 . assocL .  compFL unit . idRInv++inj2 :: CoproductCategory c => NatTr (c :><: c) c (Proj2 c c) (CoproductF c)+inj2 = idL . compFR retractProj2 . assocL .  compFL unit . idRInv++coproduct :: forall c x y z. CoproductCategory c => c x z -> c y z -> c (Coproduct c x y) z+coproduct f g | Dict <- observeObjects g = proxy phiR (Proxy :: Proxy '(CoproductF c, Diag c)) (f :><: g)++instance Functor (CoproductF (->)) ('KProxy :: KProxy ((*, *) -> *)) where+    type Domain (CoproductF (->)) = (->) :><: (->)+    type Codomain (CoproductF (->)) = (->)+    type FMap (CoproductF (->)) '(a, b) = P.Either a b+    morphMap = (Tagged (\(f :><: g) -> coproduct (appNat inj1 . f) (appNat inj2 . g)))++instance Adjoint ((->) :><: (->)) (->) (CoproductF (->)) (Diag (->)) where+    leftAdjunct = NatTr (Tagged (\f -> (f . P.Left) :><: (f . P.Right)))+    rightAdjunct = NatTr (Tagged (\(f :><: g) -> P.either f g))++instance CoproductCategory (->)
Functor.hs view
@@ -6,6 +6,7 @@ import Data.Tagged  import Category+import Category.Product  -- |The class of functors @f@ from @Domain f@ to @Codomain f@. Rather than -- indexing functors on the type of their object mapping, Functor is indexed on@@ -30,11 +31,19 @@ fmap :: forall f (a :: o1) (b :: o1). Functor f ('KProxy :: KProxy (o1 -> o2)) => f -> Domain f a b -> Codomain f (FMap f a :: o2) (FMap f b :: o2) fmap _ = proxy morphMap (Proxy :: Proxy f) +type EndoFunctor f = (Functor f ('KProxy :: KProxy (k -> k)), (Domain f :: k -> k -> *) ~ Codomain f)++type EndoFunctorOf f (c :: k -> k -> *) = (Functor f ('KProxy :: KProxy (k -> k)), Domain f ~ c, Codomain f ~ c)++type FunctorOf f (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) = (Functor f ('KProxy :: KProxy (o1 -> o2)), Domain f ~ c1, Codomain f ~ c2)+ -- |The composition of functors. The type variable @k@ is a proxy for the kind of the objects of the codomain of @g@. data Comp (k :: KProxy o2) (f :: *) (g :: *) where     (:.:) :: (Functor f ('KProxy :: KProxy (o2 -> o3)), Functor g ('KProxy :: KProxy (o1 -> o2)), (Domain f :: o2 -> o2 -> *) ~ Codomain g) =>         f -> g -> Comp ('KProxy :: KProxy o2) f g +type f :.: g = Comp ('KProxy :: KProxy *) f g+ instance (Functor f ('KProxy :: KProxy (o2 -> o3)), Functor g ('KProxy :: KProxy (o1 -> o2)), (Domain f :: o2 -> o2 -> *) ~ Codomain g)         => Functor (Comp ('KProxy :: KProxy o2) f g) ('KProxy :: KProxy (o1 -> o3)) where     type FMap (Comp ('KProxy :: KProxy o2) f g) a = FMap f (FMap g a :: o2)@@ -45,18 +54,35 @@ -- |The identity functor. data IdentityF c where IdentityF :: Category c => IdentityF c +type Id = IdentityF (->)+ instance Category c => Functor (IdentityF (c :: k -> k -> *)) ('KProxy :: KProxy (k -> k)) where     type Domain (IdentityF c) = c     type Codomain (IdentityF c) = c     type FMap (IdentityF c) (a :: k) = a     morphMap = Tagged id --- |Functors derived from Prelude's Functor.-data CanonicalF (f :: * -> *) where-    CanonicalF :: P.Functor f => CanonicalF f+data Dual f -instance P.Functor f => Functor (CanonicalF f) ('KProxy :: KProxy (* -> *)) where-    type FMap (CanonicalF f) a = f a-    type Domain (CanonicalF f) = (->)-    type Codomain (CanonicalF f) = (->)+instance Functor f ('KProxy :: KProxy (o1 -> o2)) => Functor (Dual f) ('KProxy :: KProxy (o1 -> o2)) where+    type Domain (Dual f) = Op (Domain f)+    type Codomain (Dual f) = Op (Codomain f)+    type FMap (Dual f) a = FMap f a+    morphMap = Tagged (\(Op f) -> Op (proxy morphMap (Proxy :: Proxy f) f))++data Hom c++instance Category c => Functor (Hom (c :: o -> o -> *)) ('KProxy :: KProxy ((o, o) -> *)) where+    type Domain (Hom c) = Op c :><: c+    type Codomain (Hom c) = (->)+    type FMap (Hom c) '(a, b) = c a b+    morphMap = Tagged (\(Op f :><: g) h -> g . h . f)++-- |Functors from Prelude.Functor+data Ftag f where Ftag :: P.Functor f => Ftag f++instance P.Functor f => Functor (Ftag f) ('KProxy :: KProxy (* -> *)) where+    type Domain (Ftag f) = (->)+    type Codomain (Ftag f) = (->)+    type FMap (Ftag f) a = f a     morphMap = Tagged P.fmap
+ Monad.hs view
@@ -0,0 +1,35 @@+module Monad where++import qualified Prelude as P+import Data.Constraint+import Data.Proxy+import Data.Tagged++import Category+import Functor+import NatTr++class EndoFunctorOf t c => Monad t (c :: o -> o -> *) | t -> c where+    nu :: NatTr c c (IdentityF c) t+    mu :: NatTr c c (Comp ('KProxy :: KProxy o) t t) t++data MonadMorph c t s where MonadMorph :: (Monad t c, Monad s c) => NatTr c c t s -> MonadMorph c t s++instance Category c => Category (MonadMorph c) where+    type Object (MonadMorph c) t = Monad t c+    id = MonadMorph id+    MonadMorph f . MonadMorph g = MonadMorph (f . g)+    observeObjects (MonadMorph _) = Dict++data ForgetM c where+    ForgetM :: Category c => ForgetM c++instance Category c => Functor (ForgetM c) ('KProxy :: KProxy (* -> *)) where+    type Domain (ForgetM c) = MonadMorph c+    type Codomain (ForgetM c) = NatTr c c+    type FMap (ForgetM c) (t :: *) = t+    morphMap = Tagged (\(MonadMorph t) -> t)++instance (P.Functor m, P.Monad m) => Monad (Ftag m) (->) where+    nu = NatTr (Tagged P.return)+    mu = NatTr (Tagged (P.>>= id))
+ Monad/Free.hs view
@@ -0,0 +1,50 @@+module Monad.Free where++import qualified Prelude as P+import Data.Constraint+import Data.Proxy+import Data.Tagged++import Category+import Functor+import Coproduct+import Monad+import NatTr+import NatTr.Coproduct++data Free f a where+    Free :: FMap f (Free f a) -> Free f a+    Pure :: EndoFunctorOf f (->) => a -> Free f a++freeT :: EndoFunctorOf f (->) => NatTr (->) (->) (f :.: Ftag (Free f)) (Ftag (Free f))+freeT = NatTr (Tagged Free)++pureT :: EndoFunctorOf f (->) => NatTr (->) (->) Id (Ftag (Free f))+pureT = NatTr (Tagged Pure)++unfreeT :: forall f. EndoFunctorOf f (->) => NatTr (->) (->) (Ftag (Free f)) ((f :.: Ftag (Free f)) :+: Id)+unfreeT = NatTr (Tagged t) where+    t :: forall a. Free f a -> FMap ((f :.: Ftag (Free f)) :+: Id) a+    t (Free f) = appNat inj1 f+    t (Pure a) = appNat inj2 a++instance EndoFunctorOf f (->) => P.Functor (Free f) where+    fmap t = go where+        go (Free f) = Free (proxy morphMap (Proxy :: Proxy f) go f)+        go (Pure a) = Pure (t a)++instance EndoFunctorOf f (->) => P.Monad (Free f) where+    f >>= t = go f where+        go (Free x) = Free (proxy morphMap (Proxy :: Proxy f) go x)+        go (Pure a) = t a+    return = Pure++data FreeM = FreeM++instance Functor FreeM ('KProxy :: KProxy (* -> *)) where+    type Domain FreeM = NatTr (->) (->)+    type Codomain FreeM = MonadMorph (->)+    type FMap FreeM f = Ftag (Free f)+    morphMap = Tagged (\t -> case observeObjects t of Dict -> f t) where+        f t = MonadMorph go where+            go = coproduct (freeT . compNat t go) pureT . unfreeT
Monoidal.hs view
@@ -7,10 +7,9 @@ import Category.Product import Functor -class (Category c, Functor (Mu c) ('KProxy :: KProxy ((k, k) -> k)), Domain (Mu c) ~ (c :><: c), Codomain (Mu c) ~ c, Object c (I c)) =>-        Monoidal (c :: k -> k -> *) where-    type Mu c-    type I c :: k+class (Category c, FunctorOf mu (c :><: c) c) => Monoidal (c :: o -> o -> *) mu | mu -> c where+    type I mu :: o -(<>) :: forall c a1 a2 b1 b2. Monoidal c => c a1 b1 -> c a2 b2 -> c (FMap (Mu c) '(a1, a2)) (FMap (Mu c) '(b1, b2))-f <> g = proxy morphMap (Proxy :: Proxy (Mu c)) (f :><: g)+(<>) :: forall (c :: o -> o -> *) mu a1 a2 b1 b2. Monoidal c mu => c a1 b1 -> c a2 b2 -> Tagged mu (c (FMap mu '(a1, a2)) (FMap mu '(b1, b2)))+f <> g = Tagged (proxy morphMap (Proxy :: Proxy mu) (f :><: g))+
+ NatTr.hs view
@@ -0,0 +1,124 @@+{-# LANGUAGE AllowAmbiguousTypes #-}++module NatTr where++import Data.Constraint hiding ((&&&))+import Data.Tagged+import Data.Proxy++import Category+import Category.Product+import Functor++data NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) (f :: *) (g :: *) where+    NatTr :: (Object (NatTr c1 c2) f, Object (NatTr c1 c2) g) =>+        (forall (a :: o1). Object c1 a => Tagged a (c2 (FMap f a :: o2) (FMap g a :: o2))) -> NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) f g++appNat :: forall c1 c2 f g a. Object c1 a => NatTr c1 c2 f g -> c2 (FMap f a) (FMap g a)+appNat (NatTr t) = proxy t (Proxy :: Proxy a)++instance (Category c1, Category c2) => Category (NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *)) where+    type Object (NatTr c1 c2) f = FunctorOf f c1 c2+    observeObjects (NatTr _) = Dict+    id :: forall f. Object (NatTr c1 c2) f => NatTr c1 c2 f f+    id = NatTr f where+        f :: forall a. Object c1 a => Tagged a (c2 (FMap f a) (FMap f a))+        f = Tagged (id \\ proxy objectMap (Proxy :: Proxy '(f, a)))+    (.) :: forall g h f. NatTr c1 c2 g h -> NatTr c1 c2 f g -> NatTr c1 c2 f h+    NatTr f . NatTr g = NatTr h where+        h :: forall a. Object c1 a => Tagged a (c2 (FMap f a) (FMap h a))+        h = Tagged (proxy f (Proxy :: Proxy a) . proxy g (Proxy :: Proxy a))++data CompFF c1 c2 c3  where CompFF :: (Category c1, Category c2, Category c3) => CompFF c1 c2 c3++instance (Category c1, Category c2, Category c3) =>+        Functor (CompFF (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) (c3 :: o3 -> o3 -> *)) ('KProxy :: KProxy ((*, *) -> *)) where+    type Domain (CompFF c1 c2 c3) = NatTr c2 c3 :><: NatTr c1 c2+    type Codomain (CompFF c1 c2 c3) = NatTr c1 c3+    type FMap (CompFF c1 c2 c3) '(f, g) = Comp ('KProxy :: KProxy o2) f g+    morphMap = Tagged (\(t1 :><: t2) -> compNat t1 t2)++compNat :: forall (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) (c3 :: o3 -> o3 -> *) f1 f2 g1 g2.+    NatTr c2 c3 f1 g1 -> NatTr c1 c2 f2 g2 -> NatTr c1 c3 (Comp ('KProxy :: KProxy o2) f1 f2) (Comp ('KProxy :: KProxy o2) g1 g2)+compNat (NatTr t1) (NatTr t2) = NatTr t3 where+    t3 :: forall (a :: o1). Object c1 a => Tagged a (c3 (FMap f1 (FMap f2 a :: o2) :: o3) (FMap g1 (FMap g2 a :: o2) :: o3))+    t3 = Tagged (m1 . m2) where+        m2 = proxy morphMap (Proxy :: Proxy f1) (proxy t2 (Proxy :: Proxy a))+        m1 = proxy t1 (Proxy :: Proxy (FMap g2 a)) \\ proxy objectMap (Proxy :: Proxy '(g2, a))++(<.>) :: (Functor f ('KProxy :: KProxy (o3 -> o4)), Functor g ('KProxy :: KProxy (o1 -> o2))) =>+    f -> g -> NatTr (Codomain g :: o2 -> o2 -> *) (Domain f :: o3 -> o3 -> *) h1 h2 ->+    NatTr (Domain g :: o1 -> o1 -> *) (Codomain f :: o4 -> o4 -> *)+        (Comp ('KProxy :: KProxy o3) f (Comp ('KProxy :: KProxy o2) h1 g))+        (Comp ('KProxy :: KProxy o3) f (Comp ('KProxy :: KProxy o2) h2 g))+f <.> g = compFL . compFR++compFL :: forall c1 c2 f h g. (Category c1, Functor h ('KProxy :: KProxy (o2 -> o3)), Domain h ~ c2) =>+    NatTr c1 (c2 :: o2 -> o2 -> *) f g -> NatTr c1 (Codomain h :: o3 -> o3 -> *) (Comp ('KProxy :: KProxy o2) h f) (Comp ('KProxy :: KProxy o2) h g)+compFL t | Dict <- observeObjects t = NatTr t' where+    t' :: forall a. Object c1 a => Tagged a (Codomain h (FMap h (FMap f a :: o2) :: o3) (FMap h (FMap g a :: o2)))+    t' = Tagged (proxy morphMap (Proxy :: Proxy (Comp ('KProxy :: KProxy o2) h (AppNat a c1 c2))) t)++compFR :: forall c2 c3 f h g. (Category c3, Functor h ('KProxy :: KProxy (o1 -> o2)), Codomain h ~ c2) =>+    NatTr (c2 :: o2 -> o2 -> *) c3 f g -> NatTr (Domain h :: o1 -> o1 -> *) c3 (Comp ('KProxy :: KProxy o2) f h) (Comp ('KProxy :: KProxy o2) g h)+compFR t | Dict <- observeObjects t = NatTr t' where+    t' :: forall (a :: o1). Object (Domain h) a => Tagged a (c3 (FMap f (FMap h a :: o2)) (FMap g (FMap h a :: o2)))+    t' = Tagged (proxy morphMap (Proxy :: Proxy (AppNat (FMap h a) c2 c3)) t \\ proxy objectMap (Proxy :: Proxy '(h, a)))++data AppNat a c1 c2 where AppNat :: (Category c1, Category c2, Object c1 a) => AppNat a c1 c2++instance (Category c1, Category c2, Object c1 a) => Functor (AppNat (a :: o1) (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *)) ('KProxy :: KProxy (* -> o2)) where+    type Domain (AppNat a c1 c2) = NatTr c1 c2+    type Codomain (AppNat a c1 c2) = c2+    type FMap (AppNat a c1 c2) f = (FMap f a :: o2)+    morphMap = Tagged (\(NatTr t) -> proxy t (Proxy :: Proxy a))++idL :: forall f. Functor f ('KProxy :: KProxy (o1 -> o2)) =>+    NatTr (Domain f :: o1 -> o1 -> *) (Codomain f :: o2 -> o2 -> *) (Comp ('KProxy :: KProxy o2) (IdentityF (Codomain f :: o2 -> o2 -> *)) f) f+idL = NatTr t where+    t :: forall (a :: o1). Object (Domain f) a => Tagged a (Codomain f (FMap f a :: o2) (FMap f a :: o2))+    t = Tagged (id \\ proxy objectMap (Proxy :: Proxy '(f, a)))++idLInv :: forall f. Functor f ('KProxy :: KProxy (o1 -> o2)) =>+    NatTr (Domain f :: o1 -> o1 -> *) (Codomain f :: o2 -> o2 -> *) f (Comp ('KProxy :: KProxy o2) (IdentityF (Codomain f :: o2 -> o2 -> *)) f)+idLInv = NatTr t where+    t :: forall (a :: o1). Object (Domain f) a => Tagged a (Codomain f (FMap f a :: o2) (FMap f a :: o2))+    t = Tagged (id \\ proxy objectMap (Proxy :: Proxy '(f, a)))++idR :: forall f. Functor f ('KProxy :: KProxy (o1 -> o2)) =>+    NatTr (Domain f :: o1 -> o1 -> *) (Codomain f :: o2 -> o2 -> *) (Comp ('KProxy :: KProxy o1) f (IdentityF (Domain f :: o1 -> o1 -> *))) f+idR = NatTr t where+    t :: forall (a :: o1). Object (Domain f) a => Tagged a (Codomain f (FMap f a :: o2) (FMap f a :: o2))+    t = Tagged (id \\ proxy objectMap (Proxy :: Proxy '(f, a)))++idRInv :: forall f. Functor f ('KProxy :: KProxy (o1 -> o2)) =>+    NatTr (Domain f :: o1 -> o1 -> *) (Codomain f :: o2 -> o2 -> *) f (Comp ('KProxy :: KProxy o1) f (IdentityF (Domain f :: o1 -> o1 -> *)))+idRInv = NatTr t where+    t :: forall (a :: o1). Object (Domain f) a => Tagged a (Codomain f (FMap f a :: o2) (FMap f a :: o2))+    t = Tagged (id \\ proxy objectMap (Proxy :: Proxy '(f, a)))++assocL :: forall f g h.+    (Functor f ('KProxy :: KProxy (o3 -> o4)), Functor g ('KProxy :: KProxy (o2 -> o3)), Functor h ('KProxy :: KProxy (o1 -> o2)),+    (Domain f :: o3 -> o3 -> *) ~ Codomain g, (Domain g :: o2 -> o2 -> *) ~ Codomain h) =>+        NatTr (Domain h :: o1 -> o1 -> *) (Codomain f :: o4 -> o4 -> *)+            (Comp ('KProxy :: KProxy o3) f (Comp ('KProxy :: KProxy o2) g h))+            (Comp ('KProxy :: KProxy o2) (Comp ('KProxy :: KProxy o3) f g) h)+assocL = NatTr t where+    t :: forall (a :: o1). Object (Domain h) a => Tagged a (Codomain f (FMap f (FMap g (FMap h a :: o2) :: o3) :: o4) (FMap f (FMap g (FMap h a :: o2) :: o3) :: o4))+    t = Tagged (id \\+                    proxy objectMap (Proxy :: Proxy '(f, (FMap g (FMap h a :: o2) :: o3))) .+                    proxy objectMap (Proxy :: Proxy '(g, (FMap h a :: o2))) .+                    proxy objectMap (Proxy :: Proxy '(h, a)))++assocR :: forall f g h.+    (Functor f ('KProxy :: KProxy (o3 -> o4)), Functor g ('KProxy :: KProxy (o2 -> o3)), Functor h ('KProxy :: KProxy (o1 -> o2)),+    (Domain f :: o3 -> o3 -> *) ~ Codomain g, (Domain g :: o2 -> o2 -> *) ~ Codomain h) =>+        NatTr (Domain h :: o1 -> o1 -> *) (Codomain f :: o4 -> o4 -> *)+            (Comp ('KProxy :: KProxy o2) (Comp ('KProxy :: KProxy o3) f g) h)+            (Comp ('KProxy :: KProxy o3) f (Comp ('KProxy :: KProxy o2) g h))+assocR = NatTr t where+    t :: forall (a :: o1). Object (Domain h) a => Tagged a (Codomain f (FMap f (FMap g (FMap h a :: o2) :: o3) :: o4) (FMap f (FMap g (FMap h a :: o2) :: o3) :: o4))+    t = Tagged (id \\+                    proxy objectMap (Proxy :: Proxy '(f, (FMap g (FMap h a :: o2) :: o3))) .+                    proxy objectMap (Proxy :: Proxy '(g, (FMap h a :: o2))) .+                    proxy objectMap (Proxy :: Proxy '(h, a)))
+ NatTr/Coproduct.hs view
@@ -0,0 +1,29 @@+module NatTr.Coproduct where++import Data.Constraint hiding ((&&&))+import Data.Tagged+import Data.Proxy++import Adjoint+import Category+import Category.Product+import Functor+import Functor.Product+import Product+import Coproduct+import NatTr++instance (Category c1, CoproductCategory c2) => Functor (CoproductF (NatTr c1 (c2 :: o2 -> o2 -> *))) ('KProxy :: KProxy ((*, *) -> *)) where+    type Domain (CoproductF (NatTr c1 c2)) = NatTr c1 c2 :><: NatTr c1 c2+    type Codomain (CoproductF (NatTr c1 c2)) = NatTr c1 c2+    type FMap (CoproductF (NatTr c1 c2)) '((f :: *), (g :: *)) = Comp ('KProxy :: KProxy (o2, o2)) (CoproductF c2) (f :&&&: g)+    morphMap = (Tagged (\t@(f :><: g) -> case observeObjects t of Dict -> coproduct (appNat inj1 . f) (appNat inj2 . g)))++instance (Category c1, CoproductCategory c2) =>+    Adjoint (NatTr c1 c2 :><: NatTr c1 c2) (NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *)) (CoproductF (NatTr c1 c2)) (Diag (NatTr c1 c2)) where+    leftAdjunct = NatTr (Tagged (\t -> (t . compFR inj1 . proj1FInv) :><: (t . compFR inj2 . proj2FInv)))+    rightAdjunct = NatTr (Tagged (\(t1 :><: t2) -> idL . compFR counit . assocL . compFL (diagInv . productNat t1 t2)))++instance (Category c1, CoproductCategory c2) => CoproductCategory (NatTr c1 c2)++type f :+: g = Coproduct (NatTr (->) (->)) f g
+ NatTr/Product.hs view
@@ -0,0 +1,29 @@+module NatTr.Product where++import qualified Prelude as P+import Data.Constraint hiding ((&&&))+import Data.Tagged+import Data.Proxy++import Category+import Category.Product+import Functor+import Functor.Product+import Product+import NatTr+import Adjoint++instance (Category c1, ProductCategory c2) => Functor (ProductF (NatTr c1 (c2 :: o2 -> o2 -> *))) ('KProxy :: KProxy ((*, *) -> *)) where+    type Domain (ProductF (NatTr c1 c2)) = NatTr c1 c2 :><: NatTr c1 c2+    type Codomain (ProductF (NatTr c1 c2)) = NatTr c1 c2+    type FMap (ProductF (NatTr c1 c2)) '((f :: *), (g :: *)) = Comp ('KProxy :: KProxy (o2, o2)) (ProductF c2) (f :&&&: g)+    morphMap = Tagged (\t@(f :><: g) -> case observeObjects t of Dict -> (f . appNat proj1) &&& (g . appNat proj2))++instance (Category c1, ProductCategory c2) =>+        Adjoint (NatTr c1 c2) (NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) :><: NatTr c1 c2) (Diag (NatTr c1 c2)) (ProductF (NatTr c1 c2)) where+    leftAdjunct = NatTr (Tagged (\(s :><: t) -> compFL (productNat s t . diag) . assocR . compFR unit . idLInv))+    rightAdjunct = NatTr (Tagged (\t -> (proj1F . compFR proj1 . t) :><: (proj2F . compFR proj2 . t)))++instance (Category c1, ProductCategory c2) => ProductCategory (NatTr c1 c2)++type f :*: g = Product (NatTr (->) (->)) f g
− NaturalTransformation.hs 
@@ -1,47 +0,0 @@-module NaturalTransformation where--import Data.Constraint-import Data.Tagged-import Data.Proxy--import Category-import Category.Product-import Functor-import Monoidal--data NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) (f :: *) (g :: *) where-    NatTr :: (Object (NatTr c1 c2) f, Object (NatTr c1 c2) g) =>-        (forall (a :: o1). Object c1 a => Tagged a (c2 (FMap f a :: o2) (FMap g a :: o2))) -> NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) f g--instance (Category c1, Category c2) => Category (NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *)) where-    type Object (NatTr c1 c2) f = (Functor f ('KProxy :: KProxy (o1 -> o2)), Domain f ~ c1, Codomain f ~ c2)-    observeObjects (NatTr _) = Dict-    id :: forall f. Object (NatTr c1 c2) f => NatTr c1 c2 f f-    id = NatTr f where-        f :: forall a. Object c1 a => Tagged a (c2 (FMap f a) (FMap f a))-        f = Tagged (id \\ proxy objectMap (Proxy :: Proxy '(f, a)))-    (.) :: forall g h f. NatTr c1 c2 g h -> NatTr c1 c2 f g -> NatTr c1 c2 f h-    NatTr f . NatTr g = NatTr h where-        h :: forall a. Object c1 a => Tagged a (c2 (FMap f a) (FMap h a))-        h = Tagged (proxy f (Proxy :: Proxy a) . proxy g (Proxy :: Proxy a))--data CompFF c1 c2 c3  where CompFF :: (Category c1, Category c2, Category c3) => CompFF c1 c2 c3--instance (Category c1, Category c2, Category c3) =>-        Functor (CompFF (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) (c3 :: o3 -> o3 -> *)) ('KProxy :: KProxy ((*, *) -> *)) where-    type Domain (CompFF c1 c2 c3) = NatTr c2 c3 :><: NatTr c1 c2-    type Codomain (CompFF c1 c2 c3) = NatTr c1 c3-    type FMap (CompFF c1 c2 c3) '(f, g) = Comp ('KProxy :: KProxy o2) f g-    morphMap = Tagged (\(t1 :><: t2) -> compNat t1 t2)--compNat :: forall (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) (c3 :: o3 -> o3 -> *) f1 f2 g1 g2.-    NatTr c2 c3 f1 g1 -> NatTr c1 c2 f2 g2 -> NatTr c1 c3 (Comp ('KProxy :: KProxy o2) f1 f2) (Comp ('KProxy :: KProxy o2) g1 g2)-compNat (NatTr t1) (NatTr t2) = NatTr t3 where-    t3 :: forall (a :: o1). Object c1 a => Tagged a (c3 (FMap f1 (FMap f2 a :: o2) :: o3) (FMap g1 (FMap g2 a :: o2) :: o3))-    t3 = Tagged (m1 . m2) where-        m2 = proxy morphMap (Proxy :: Proxy f1) (proxy t2 (Proxy :: Proxy a))-        m1 = proxy t1 (Proxy :: Proxy (FMap g2 a)) \\ proxy objectMap (Proxy :: Proxy '(g2, a))--instance Category c => Monoidal (NatTr c c) where-    type Mu (NatTr c c) = CompFF c c c-    type I (NatTr c c) = IdentityF c
Product.hs view
@@ -8,65 +8,52 @@ import Category import Category.Product import Functor+import Functor.Product+import NatTr+import Adjoint import Terminal-import TerminalMorphism+import Universal import Monoidal -class Category c => ProductCategory (c :: k -> k -> *) where-    type (><) (a :: k) (b :: k) :: k-    productObjectMap :: Tagged '(c, a, b) ((Object c a, Object c b) :- Object c (a >< b))-    univProduct :: forall (a :: k) (b :: k). Tagged '(c, a, b) ((Object c a, Object c b) :- TerminalMorphism (Diag c) (a >< b) '(a, b))+data ProductF (c :: o -> o -> *) where ProductF :: ProductCategory c => ProductF c+class Adjoint c (c :><: c) (Diag c) (ProductF c) => ProductCategory c+type Product c a b = FMap (ProductF c) '(a, b) -proj1 :: forall a b c. (ProductCategory c, Object c a, Object c b) => Tagged b (c (a >< b) a)-proj1 = Tagged p where-    p :><: _ = t-    t :: (c :><: c) '(a >< b, a >< b) '(a, b)-    t = proxy terminalMorphism (Proxy :: Proxy '(Diag c, a >< b)) \\ proxy univProduct (Proxy :: Proxy '(c, a, b))+proj1 :: forall (c :: o -> o -> *). ProductCategory c => NatTr (c :><: c) c (ProductF c) (Proj1 c c)+proj1 = idR . compFL counit . assocR . compFR retractProj1Inv . idLInv -proj2 :: forall a b c. (ProductCategory c, Object c a, Object c b) => Tagged a (c (a >< b) b)-proj2 = Tagged p where-    _ :><: p = t-    t :: (c :><: c) '(a >< b, a >< b) '(a, b)-    t = proxy terminalMorphism (Proxy :: Proxy '(Diag c, a >< b)) \\ proxy univProduct (Proxy :: Proxy '(c, a, b))+proj2 :: forall (c :: o -> o -> *). ProductCategory c => NatTr (c :><: c) c (ProductF c) (Proj2 c c)+proj2 = idR . compFL counit . assocR . compFR retractProj2Inv . idLInv -(&&&) :: forall c a b1 b2. ProductCategory c => c a b1 -> c a b2 -> c a (b1 >< b2)-f &&& g-    | Dict <- observeObjects f, Dict <- observeObjects g-        = proxy terminalFactorization (Proxy :: Proxy (Diag c)) (f :><: g) \\ proxy univProduct (Proxy :: Proxy '(c, b1, b2))+(&&&) :: forall c a b1 b2. ProductCategory c => c a b1 -> c a b2 -> c a (Product c b1 b2)+f &&& g | Dict <- observeObjects f = proxy phiL (Proxy :: Proxy '(Diag c, ProductF c)) (f :><: g) -(***) :: forall c a1 a2 b1 b2. ProductCategory c => c a1 b1 -> c a2 b2 -> c (a1 >< a2) (b1 >< b2)+(***) :: forall c a1 a2 b1 b2. ProductCategory c => c a1 b1 -> c a2 b2 -> c (Product c a1 a2) (Product c b1 b2) f *** g = proxy morphMap (Proxy :: Proxy (ProductF c)) (f :><: g) -data ProductF c where ProductF :: ProductCategory c => ProductF c+instance (ProductCategory c, Terminal c) => Monoidal c (ProductF c) where+    type I (ProductF c) = T c -instance ProductCategory (c :: k -> k -> *) => Functor (ProductF c) ('KProxy :: KProxy ((k, k) -> k)) where-    type Domain (ProductF c) = c :><: c-    type Codomain (ProductF c) = c-    type FMap (ProductF c) (a :: (k, k)) = L a >< R a-    morphMap :: forall (a :: (k, k)) (b :: (k, k)). Tagged (ProductF c)-        (Domain (ProductF c) a b -> Codomain (ProductF c) (FMap (ProductF c) a :: k) (FMap (ProductF c) b :: k))-    morphMap = Tagged m where-        m (f :><: g)-            | Dict <- observeObjects f, Dict <- observeObjects g = (f . (proxy proj1 (Proxy :: Proxy (R a)))) &&& (g . (proxy proj2 (Proxy :: Proxy (L a))))+instance Functor (ProductF (->)) ('KProxy :: KProxy ((*,*) -> *)) where+    type Domain (ProductF (->)) = (->) :><: (->)+    type Codomain (ProductF (->)) = (->)+    type FMap (ProductF (->)) '(a, b) = (a, b)+    morphMap = Tagged (\(f :><: g) -> (f . appNat proj1) &&& (g . appNat proj2)) -instance (ProductCategory c, Terminal c) => Monoidal c where-    type Mu c = ProductF c-    type I c = T c+instance Adjoint (->) ((->) :><: (->)) (Diag (->)) (ProductF (->)) where+    leftAdjunct = NatTr (Tagged (\(f :><: g) z -> (f z, g z)))+    rightAdjunct = NatTr (Tagged (\f -> (P.fst . f) :><: (P.snd . f))) -instance TerminalMorphism (Diag (->)) (a, b) '(a, b) where-    terminalMorphism = Tagged (P.fst :><: P.snd)-    terminalFactorization  = Tagged (\(f :><: g) z -> (f z, g z))+instance ProductCategory (->) -instance ProductCategory (->) where-    type (><) a b = (a, b)-    productObjectMap = Tagged (Sub Dict)-    univProduct = Tagged (Sub Dict)+instance Functor (ProductF (:-)) ('KProxy :: KProxy ((Constraint, Constraint) -> Constraint)) where+    type Domain (ProductF (:-)) = (:-) :><: (:-)+    type Codomain (ProductF (:-)) = (:-)+    type FMap (ProductF (:-)) '((a :: Constraint), (b :: Constraint)) = ((a, b) :: Constraint)+    morphMap = Tagged (\(f :><: g) -> (f . appNat proj1) &&& (g . appNat proj2)) -instance TerminalMorphism (Diag (:-)) ((a :: Constraint), b) '(a, b) where-    terminalMorphism = Tagged (Sub Dict :><: Sub Dict)-    terminalFactorization = Tagged (\(f :><: g) -> Sub (Dict \\ f \\ g))+instance Adjoint (:-) ((:-) :><: (:-)) (Diag (:-)) (ProductF (:-)) where+    leftAdjunct = NatTr (Tagged (\(f :><: g) -> Sub (Dict \\ f \\ g)))+    rightAdjunct = NatTr (Tagged (\f -> (Sub (Dict \\ f) :><: Sub (Dict \\ f)))) -instance ProductCategory (:-) where-    type (><) a b = ((a, b) :: Constraint)-    productObjectMap = Tagged (Sub Dict)-    univProduct = Tagged (Sub Dict)+instance ProductCategory (:-)
− TerminalMorphism.hs 
@@ -1,12 +0,0 @@-module TerminalMorphism where--import Data.Tagged-import Data.Proxy--import Category-import Functor--class (Functor f ('KProxy :: KProxy (o1 -> o2)), Object (Domain f) a, Object (Codomain f) x) =>-        TerminalMorphism f (a :: o1) (x :: o2) where-    terminalMorphism :: Tagged '(f, a) (Codomain f (FMap f a) x)-    terminalFactorization :: Object (Domain f) y => Tagged f (Codomain f (FMap f y) x -> Domain f y a)
+ Universal.hs view
@@ -0,0 +1,17 @@+module Universal where++import Data.Tagged+import Data.Proxy++import Category+import Functor++class (Functor f ('KProxy :: KProxy (o1 -> o2)), Object (Domain f) a, Object (Codomain f) x) =>+        InitialMorphism f (a :: o1) (x :: o2) where+    initialMorphism :: Tagged '(f, a) (Codomain f x (FMap f a))+    initialFactorization :: Object (Domain f) b => Tagged f (Codomain f x (FMap f b) -> Domain f a b)++class (Functor f ('KProxy :: KProxy (o1 -> o2)), Object (Domain f) a, Object (Codomain f) x) =>+        TerminalMorphism f (a :: o1) (x :: o2) where+    terminalMorphism :: Tagged '(f, a) (Codomain f (FMap f a) x)+    terminalFactorization :: Object (Domain f) b => Tagged f (Codomain f (FMap f b) x -> Domain f b a)
extended-categories.cabal view
@@ -1,5 +1,5 @@ name:                extended-categories-version:             0.1.0+version:             0.2.0 synopsis:       Extended Categories description:    An implementation of category theory which makes use of GHC's enriched kind system. homepage:            github.com/ian-mi/extended-categories@@ -21,10 +21,10 @@ source-repository this         type: git         location: git@github.com:ian-mi/extended-categories.git-        tag: 0.1.0+        tag: 0.2.0  library-  exposed-modules:     Category, Category.Product, Functor, Product, Terminal, TerminalMorphism, NaturalTransformation, Monoidal+  exposed-modules:     Category, Category.Product, Functor, Universal, Product, Coproduct, Terminal, NatTr, NatTr.Product, NatTr.Coproduct, Adjoint, Monoidal, Monad, Monad.Free   -- other-modules:          default-extensions:    PolyKinds, DataKinds, TypeFamilies, ConstraintKinds, InstanceSigs, ScopedTypeVariables, MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, FlexibleInstances, UndecidableInstances, TypeOperators, GADTs, NoImplicitPrelude, RankNTypes   build-depends:       base >=4.7 && <4.8, constraints >=0.3 && <0.5, tagged >=0.7 && <0.8, ghc-prim >=0.3 && <0.4