data-category 0.3.1.1 → 0.4

raw patch · 16 files changed

+463/−393 lines, 16 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/Category/Adjunction.hs +16/−49
• Data/Category/Boolean.hs +1/−1
• Data/Category/CartesianClosed.hs +7/−6
• Data/Category/Coproduct.hs +1/−1
• Data/Category/Dialg.hs +30/−3
• Data/Category/Discrete.hs +9/−14
• Data/Category/Functor.hs +103/−42
• Data/Category/Kleisli.hs +17/−20
• Data/Category/Limit.hs +73/−133
• Data/Category/Monoid.hs +6/−6
• Data/Category/Monoidal.hs +20/−14
• Data/Category/NaturalTransformation.hs +55/−55
• Data/Category/Product.hs +0/−48
• Data/Category/RepresentableFunctor.hs +74/−0
• Data/Category/Yoneda.hs +48/−0
• data-category.cabal +3/−1

@@ -18,25 +18,17 @@   , leftAdjunct   , rightAdjunct   +  -- * Adjunctions as a category+  , AdjArrow(..)+     -- * Adjunctions from universal morphisms   , initialPropAdjunction   , terminalPropAdjunction   -  -- * Adjunctions to universal morphisms+  -- * Universal morphisms from adjunctions   , adjunctionInitialProp   , adjunctionTerminalProp   -  -- * Adjunctions as a category-  , AdjArrow(..)-  -  -- * (Co)limitfunctor adjunction-  , limitAdj-  , colimitAdj-  -  -- * (Co)monad of an adjunction-  , adjunctionMonad-  , adjunctionComonad-     -- * Examples   , contAdj   @@ -48,8 +40,7 @@ import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation-import Data.Category.Limit-import qualified Data.Category.Monoidal as M+import Data.Category.RepresentableFunctor  data Adjunction c d f g = (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)   => Adjunction@@ -73,31 +64,25 @@  -- Each pair (FY, unit_Y) is an initial morphism from Y to G. adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)-adjunctionInitialProp adj@(Adjunction f _ un _) y = InitialUniversal (f % y) (un ! y) (rightAdjunct adj)+adjunctionInitialProp adj@(Adjunction f g un _) y = initialUniversal g (f % y) (un ! y) (rightAdjunct adj)  -- Each pair (GX, counit_X) is a terminal morphism from F to X. adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)-adjunctionTerminalProp adj@(Adjunction _ g _ coun) x = TerminalUniversal (g % x) (coun ! x) (leftAdjunct adj)+adjunctionTerminalProp adj@(Adjunction f g _ coun) x = terminalUniversal f (g % x) (coun ! x) (leftAdjunct adj)    initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)   => f -> g -> (forall y. Obj d y -> InitialUniversal y g (f :% y)) -> Adjunction c d f g-initialPropAdjunction f g univ = mkAdjunction f g un coun-  where-    coun :: forall a. Obj c a -> c (f :% (g :% a)) a-    coun a = initialFactorizer (univ (g % a)) a (g % a)-    un   :: forall a. Obj d a -> d a (g :% (f :% a))-    un   a = initialMorphism (univ a)+initialPropAdjunction f g univ = mkAdjunction f g +  (universalElement . univ)+  (\a -> represent (univ (g % a)) a (g % a))     terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)   => f -> g -> (forall x. Obj c x -> TerminalUniversal x f (g :% x)) -> Adjunction c d f g-terminalPropAdjunction f g univ = mkAdjunction f g un coun-  where-    un   :: forall a. Obj d a -> d a (g :% (f :% a))-    un   a = terminalFactorizer (univ (f % a)) a (f % a)-    coun :: forall a. Obj c a -> c (f :% (g :% a)) a-    coun a = terminalMorphism (univ a)+terminalPropAdjunction f g univ = mkAdjunction f g +  (\a -> unOp $ represent (univ (f % a)) (Op a) (f % a)) +  (universalElement . univ)       data AdjArrow c d where@@ -110,27 +95,9 @@   tgt (AdjArrow (Adjunction _ _ _ _)) = AdjArrow $ mkAdjunction Id Id id id      AdjArrow (Adjunction f g u c) . AdjArrow (Adjunction f' g' u' c') = AdjArrow $ -    mkAdjunction (f' :.: f) (g :.: g') (\i -> ((Wrap g f % u') ! i) . (u ! i)) (\i -> (c' ! i) . ((Wrap f' g' % c) ! i))----- | The limit functor is right adjoint to the diagonal functor.-limitAdj :: forall j (~>). HasLimits j (~>) -  => LimitFunctor j (~>) -  -> Adjunction (Nat j (~>)) (~>) (Diag j (~>)) (LimitFunctor j (~>))-limitAdj LimitFunctor = terminalPropAdjunction Diag LimitFunctor (\f @ Nat{} -> limitUniv f)---- | The colimit functor is left adjoint to the diagonal functor.-colimitAdj :: forall j (~>). HasColimits j (~>) -  => ColimitFunctor j (~>) -  -> Adjunction (~>) (Nat j (~>)) (ColimitFunctor j (~>)) (Diag j (~>))-colimitAdj ColimitFunctor = initialPropAdjunction ColimitFunctor Diag (\f @ Nat{} -> colimitUniv f)---adjunctionMonad :: Adjunction c d f g -> M.Monad (g :.: f)-adjunctionMonad (Adjunction f g un coun) = M.mkMonad (g :.: f) (un !) ((Wrap g f % coun) !)--adjunctionComonad :: Adjunction c d f g -> M.Comonad (f :.: g)-adjunctionComonad (Adjunction f g un coun) = M.mkComonad (f :.: g) (coun !) ((Wrap f g % un) !)+    Adjunction (f' :.: f) (g :.: g') +      (compAssoc (g :.: g') f' f . Precompose f % (compAssocInv g g' f' . Postcompose g % u' . idPrecompInv g) . u)+      (c' . Precompose g' % (idPrecomp f' . Postcompose f' % c . compAssoc f' f g) . compAssocInv (f' :.: f) g g')   

@@ -172,7 +172,7 @@  -- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@. data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)-type instance Dom (NatAsFunctor f g) = (Dom f) :**: Boolean+type instance Dom (NatAsFunctor f g) = Dom f :**: Boolean type instance Cod (NatAsFunctor f g) = Cod f type instance NatAsFunctor f g :% (a, Fls) = f :% a type instance NatAsFunctor f g :% (a, Tru) = g :% a

@@ -19,7 +19,7 @@ import Data.Category.Product import Data.Category.Limit import Data.Category.Adjunction-import qualified Data.Category.Monoidal as M+import Data.Category.Monoidal as M   type family Exponential (~>) y z :: *@@ -74,21 +74,23 @@   (CatA f) ^^^ (CatA h) = CatA (Wrap f h)  +type Presheaves (~>) = Nat (Op (~>)) (->)+ data PShExponential ((~>) :: * -> * -> *) p q = PShExponential type instance Dom (PShExponential (~>) p q) = Op (~>) type instance Cod (PShExponential (~>) p q) = (->)-type instance PShExponential (~>) p q :% a = Presheaves (~>) ((YonedaEmbedding (~>) :% a) :*: p) q+type instance PShExponential (~>) p q :% a = Presheaves (~>) (((~>) :-*: a) :*: p) q instance (Category (~>), Dom p ~ Op (~>), Dom q ~ Op (~>), Cod p ~ (->), Cod q ~ (->), Functor p, Functor q)   => Functor (PShExponential (~>) p q) where-  PShExponential % Op f = \(Nat (_ :*: p) q n) -> Nat (Hom_X (src f) :*: p) q $ \i (i2a, pi) -> n i (f . i2a, pi)+  PShExponential % Op f = \(Nat (_ :*: p) q n) -> Nat (hom_X (src f) :*: p) q $ \i (i2a, pi) -> n i (f . i2a, pi)  type instance Exponential (Presheaves (~>)) y z = PShExponential (~>) y z  instance Category (~>) => CartesianClosed (Presheaves (~>)) where      apply (Nat y _ _) (Nat z _ _) = Nat (PShExponential :*: y) z $ \(Op i) (n, yi) -> (n ! Op i) (i, yi)-  tuple (Nat y _ _) (Nat z _ _) = Nat z PShExponential $ \(Op i) zi -> (Nat (Hom_X i) z $ \_ j2i -> (z % Op j2i) zi) *** natId y-  zn@Nat{} ^^^ yn@Nat{} = Nat PShExponential PShExponential $ \(Op i) n -> zn . n . (natId (Hom_X i) *** yn)+  tuple (Nat y _ _) (Nat z _ _) = Nat z PShExponential $ \(Op i) zi -> (Nat (hom_X i) z $ \_ j2i -> (z % Op j2i) zi) *** natId y+  zn@Nat{} ^^^ yn@Nat{} = Nat PShExponential PShExponential $ \(Op i) n -> zn . n . (natId (hom_X i) *** yn)       data ProductWith (~>) y = ProductWith (Obj (~>) y)@@ -113,7 +115,6 @@  uncurry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> x ~> (ExponentialWith (~>) y :% z) -> (ProductWith (~>) y :% x) ~> z uncurry _ y z = rightAdjunct (curryAdj y) z-  type State (~>) s a = ExponentialWith (~>) s :% ProductWith (~>) s :% a 

@@ -24,7 +24,7 @@   I1 :: c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)   I2 :: c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2) --- | The product category of category @c1@ and @c2@.+-- | The coproduct category of category @c1@ and @c2@. instance (Category c1, Category c2) => Category (c1 :++: c2) where      src (I1 a)      = I1 (src a)

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts, ViewPatterns #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts, ViewPatterns, ScopedTypeVariables, UndecidableInstances #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Dialg@@ -13,13 +13,16 @@ ----------------------------------------------------------------------------- module Data.Category.Dialg where -import Prelude hiding ((.), Functor)+import Prelude (($), id) import qualified Prelude  import Data.Category import Data.Category.Functor+import Data.Category.NaturalTransformation import Data.Category.Limit import Data.Category.Product+import Data.Category.Monoidal+import qualified Data.Category.Adjunction as A   -- | Objects of Dialg(F,G) are (F,G)-dialgebras.@@ -117,4 +120,28 @@   initialObject = dialgId $ Dialgebra id (Z :**: S)      initialize (dialgebra -> d@(Dialgebra _ (z :**: s))) = DialgA (dialgebra initialObject) d $ primRec z s-    ++++data EMAdjF m = EMAdjF (Monad m)+type instance Dom (EMAdjF m) = Dom m+type instance Cod (EMAdjF m) = Alg m+type instance EMAdjF m :% a = m :% a+instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (EMAdjF m) where+  EMAdjF m % f = DialgA (alg (src f)) (alg (tgt f)) $ monadFunctor m % f+    where+      alg :: Obj (~>) x -> Algebra m (m :% x)+      alg x = Dialgebra (monadFunctor m % x) (multiply m ! x)++data EMAdjG m = EMAdjG+type instance Dom (EMAdjG m) = Alg m+type instance Cod (EMAdjG m) = Dom m+type instance EMAdjG m :% a = a+instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (EMAdjG m) where+  EMAdjG % DialgA _ _ f = f++eilenbergMooreAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) +  => Monad m -> A.Adjunction (Alg m) (~>) (EMAdjF m) (EMAdjG m)+eilenbergMooreAdj m = A.mkAdjunction (EMAdjF m) EMAdjG+  (\x -> unit m ! x)+  (\(DialgA (Dialgebra _ h) _ _) -> DialgA (Dialgebra (src h) (monadFunctor m % h)) (Dialgebra (tgt h) h) h)

@@ -19,9 +19,10 @@   , Void   , Unit   , Pair+  , magicZ      -- * Functors-  , Next(..)+  , Succ(..)   , DiscreteDiagram(..)        -- * Natural Transformations@@ -80,19 +81,13 @@ type Pair = Discrete (S (S Z))  -type family PredDiscrete (c :: * -> * -> *) :: * -> * -> *-type instance PredDiscrete (Discrete (S n)) = Discrete n--data Next :: * -> * where-  Next :: (Functor f, Dom f ~ Discrete (S n)) => f -> Next f-  -type instance Dom (Next f) = PredDiscrete (Dom f)-type instance Cod (Next f) = Cod f-type instance Next f :% a = f :% S a--instance (Functor f, Category (PredDiscrete (Dom f))) => Functor (Next f) where-  Next f % Z     = f % S Z-  Next f % (S a) = f % S (S a)+data Succ n = Succ+type instance Dom (Succ n) = Discrete n+type instance Cod (Succ n) = Discrete (S n)+type instance Succ n :% a = S a+instance (Category (Discrete n)) => Functor (Succ n) where+  Succ % Z     = S Z+  Succ % (S a) = S (S a)   infixr 7 :::

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, UndecidableInstances, GADTs, RankNTypes #-}+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Functor@@ -25,21 +25,31 @@   , Id(..)   , (:.:)(..)   , Const(..), ConstF-  , (:*-:)(..)-  , (:-*:)(..)   , Opposite(..)   , EndoHask(..)   -  -- * Universal properties-  , InitialUniversal(..)-  , TerminalUniversal(..)-+  -- *** Related to the product category+  , Proj1(..)+  , Proj2(..)+  , (:***:)(..)+  , DiagProd(..)+  , Tuple1(..)+  , Tuple2(..)+  +  -- *** Hom functors+  , Hom(..)+  , (:*-:)+  , homX_+  , (:-*:)+  , hom_X+   ) where   -import Prelude hiding (id, (.), Functor)+import Prelude hiding ((.), Functor) import qualified Prelude    import Data.Category+import Data.Category.Product  infixr 9 % infixr 9 :%@@ -112,31 +122,7 @@  type ConstF f = Const (Dom f) (Cod f) -  --- | The covariant functor Hom(X,--)-data (:*-:) :: * -> (* -> * -> *) -> * where-  HomX_ :: Category (~>) => Obj (~>) x -> x :*-: (~>)-  -type instance Dom (x :*-: (~>)) = (~>)-type instance Cod (x :*-: (~>)) = (->)-type instance (x :*-: (~>)) :% a = x ~> a -instance Category (~>) => Functor (x :*-: (~>)) where -  HomX_ _ % f = (f .)----- | The contravariant functor Hom(--,X)-data (:-*:) :: (* -> * -> *) -> * -> * where-  Hom_X :: Category (~>) => Obj (~>) x -> (~>) :-*: x--type instance Dom ((~>) :-*: x) = Op (~>)-type instance Cod ((~>) :-*: x) = (->)-type instance ((~>) :-*: x) :% a = a ~> x--instance Category (~>) => Functor ((~>) :-*: x) where -  Hom_X _ % Op f = (. f)-- -- | The dual of a functor data Opposite f where   Opposite :: Functor f => f -> Opposite f@@ -161,14 +147,89 @@   EndoHask % f = fmap f  --- | An initial universal property, a universal morphism from x to u.-data InitialUniversal  x u a = InitialUniversal-  { iuObject :: Obj (Dom u) a-  , initialMorphism :: Cod u x (u :% a)-  , initialFactorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y }+-- | 'Proj1' is a bifunctor that projects out the first component of a product.+data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1++type instance Dom (Proj1 c1 c2) = c1 :**: c2+type instance Cod (Proj1 c1 c2) = c1+type instance Proj1 c1 c2 :% (a1, a2) = a1++instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where +  Proj1 % (f1 :**: _) = f1+++-- | 'Proj2' is a bifunctor that projects out the second component of a product.+data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj2++type instance Dom (Proj2 c1 c2) = c1 :**: c2+type instance Cod (Proj2 c1 c2) = c2+type instance Proj2 c1 c2 :% (a1, a2) = a2++instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where +  Proj2 % (_ :**: f2) = f2+++-- | @f1 :***: f2@ is the product of the functors @f1@ and @f2@.+data f1 :***: f2 = f1 :***: f2++type instance Dom (f1 :***: f2) = Dom f1 :**: Dom f2+type instance Cod (f1 :***: f2) = Cod f1 :**: Cod f2+type instance (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)++instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where +  (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)   --- | A terminal universal property, a universal morphism from u to x.-data TerminalUniversal x u a = TerminalUniversal -  { tuObject :: Obj (Dom u) a-  , terminalMorphism :: Cod u (u :% a) x-  , terminalFactorizer :: forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a }+  +-- | 'DiagProd' is the diagonal functor for products.+data DiagProd ((~>) :: * -> * -> *) = DiagProd++type instance Dom (DiagProd (~>)) = (~>)+type instance Cod (DiagProd (~>)) = (~>) :**: (~>)+type instance DiagProd (~>) :% a = (a, a)++instance Category (~>) => Functor (DiagProd (~>)) where +  DiagProd % f = f :**: f+++-- | 'Tuple1' tuples with a fixed object on the left.+data Tuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple1 (Obj c1 a)++type instance Dom (Tuple1 c1 c2 a1) = c2+type instance Cod (Tuple1 c1 c2 a1) = c1 :**: c2+type instance Tuple1 c1 c2 a1 :% a2 = (a1, a2)++instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1) where+  Tuple1 a % f = a :**: f+++-- | 'Tuple2' tuples with a fixed object on the right.+data Tuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple2 (Obj c2 a)++type instance Dom (Tuple2 c1 c2 a2) = c1+type instance Cod (Tuple2 c1 c2 a2) = c1 :**: c2+type instance Tuple2 c1 c2 a2 :% a1 = (a1, a2)++instance (Category c1, Category c2) => Functor (Tuple2 c1 c2 a2) where+  Tuple2 a % f = f :**: a+++-- | The Hom functor, Hom(–,–), a bifunctor contravariant in its first argument and covariant in its second argument.+data Hom ((~>) :: * -> * -> *) = Hom  ++type instance Dom (Hom (~>)) = Op (~>) :**: (~>)+type instance Cod (Hom (~>)) = (->)+type instance (Hom (~>)) :% (a1, a2) = a1 ~> a2++instance Category (~>) => Functor (Hom (~>)) where +  Hom % (Op f1 :**: f2) = \g -> f2 . g . f1+++type x :*-: (~>) = Hom (~>) :.: Tuple1 (Op (~>)) (~>) x+-- | The covariant functor Hom(X,–)+homX_ :: Category (~>) => Obj (~>) x -> x :*-: (~>)+homX_ x = Hom :.: Tuple1 (Op x)++type (~>) :-*: x = Hom (~>) :.: Tuple2 (Op (~>)) (~>) x+-- | The contravariant functor Hom(–,X)+hom_X :: Category (~>) => Obj (~>) x -> (~>) :-*: x+hom_X x = Hom :.: Tuple2 x

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleInstances, FlexibleContexts, RankNTypes, ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleInstances, FlexibleContexts, RankNTypes, ScopedTypeVariables, UndecidableInstances  #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Kleisli@@ -23,14 +23,13 @@ import qualified Data.Category.Adjunction as A  -data Kleisli ((~>) :: * -> * -> *) m a b where-  Kleisli :: Monad m -> Obj (~>) b -> a ~> (m :% b) -> Kleisli (~>) m a b+data Kleisli m a b where+  Kleisli :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Monad m -> Obj (~>) b -> a ~> (m :% b) -> Kleisli m a b -kleisliId :: (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) -  => Monad m -> Obj (~>) a -> Kleisli (~>) m a a+kleisliId :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Monad m -> Obj (~>) a -> Kleisli m a a kleisliId m a = Kleisli m a $ unit m ! a -instance (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Category (Kleisli (~>) m) where+instance Category (Kleisli m) where      src (Kleisli m _ f) = kleisliId m (src f)   tgt (Kleisli m b _) = kleisliId m b@@ -39,24 +38,22 @@   -data KleisliAdjF ((~>) :: * -> * -> *) m where-  KleisliAdjF :: Monad m -> KleisliAdjF (~>) m-type instance Dom (KleisliAdjF (~>) m) = (~>)-type instance Cod (KleisliAdjF (~>) m) = Kleisli (~>) m-type instance KleisliAdjF (~>) m :% a = a-instance (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (KleisliAdjF (~>) m) where+data KleisliAdjF m = KleisliAdjF (Monad m)+type instance Dom (KleisliAdjF m) = Dom m+type instance Cod (KleisliAdjF m) = Kleisli m+type instance KleisliAdjF m :% a = a+instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (KleisliAdjF m) where   KleisliAdjF m % f = Kleisli m (tgt f) $ (unit m ! tgt f) . f    -data KleisliAdjG ((~>) :: * -> * -> *) m where-  KleisliAdjG :: Monad m -> KleisliAdjG (~>) m-type instance Dom (KleisliAdjG (~>) m) = Kleisli (~>) m-type instance Cod (KleisliAdjG (~>) m) = (~>)-type instance KleisliAdjG (~>) m :% a = m :% a-instance (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (KleisliAdjG (~>) m) where+data KleisliAdjG m = KleisliAdjG (Monad m)+type instance Dom (KleisliAdjG m) = Kleisli m+type instance Cod (KleisliAdjG m) = Dom m+type instance KleisliAdjG m :% a = m :% a+instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (KleisliAdjG m) where   KleisliAdjG m % Kleisli _ b f = (multiply m ! b) . (monadFunctor m % f) -kleisliAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>), Category (~>)) -  => Monad m -> A.Adjunction (Kleisli (~>) m) (~>) (KleisliAdjF (~>) m) (KleisliAdjG (~>) m)+kleisliAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) +  => Monad m -> A.Adjunction (Kleisli m) (~>) (KleisliAdjF m) (KleisliAdjG m) kleisliAdj m = A.mkAdjunction (KleisliAdjF m) (KleisliAdjG m)   (\x -> unit m ! x)   (\(Kleisli _ x _) -> Kleisli m x $ monadFunctor m % x)

@@ -36,26 +36,16 @@   -- * Limits   , LimitFam   , Limit-  , LimitUniversal-  , limitUniversal-  , limit-  , limitFactorizer+  , HasLimits(..)+  , LimitFunctor(..)+  , limitAdj      -- * Colimits   , ColimitFam   , Colimit-  , ColimitUniversal-  , colimitUniversal-  , colimit-  , colimitFactorizer-  -  -- * Limits of a certain type-  , HasLimits(..)   , HasColimits(..)-  -  -- ** As a functor-  , LimitFunctor(..)   , ColimitFunctor(..)+  , colimitAdj      -- ** Limits of type Void   , HasTerminalObject(..)@@ -72,21 +62,20 @@   , CoproductFunctor(..)   , (:+:)(..)   -  -- ** Limits of type Hask-  , ForAll(..)-  , endoHaskLimit-  , Exists(..)-  , endoHaskColimit+  -- -- ** Limits of type Hask+  -- , ForAll(..)+  -- , Exists(..)    ) where  import Prelude hiding ((.), Functor, product)-import qualified Prelude (Functor) import qualified Control.Arrow as A ((&&&), (***), (|||), (+++))  import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation+import Data.Category.Adjunction+ import Data.Category.Product import Data.Category.Coproduct import Data.Category.Discrete@@ -135,99 +124,57 @@  type Limit f = LimitFam (Dom f) (Cod f) f --- | A limit of @f@ is a universal morphism from the diagonal functor to @f@.-type LimitUniversal f = TerminalUniversal f (DiagF f) (Limit f)---- | @limitUniversal@ is a helper function to create the universal property from the limit and the limit factorizer.-limitUniversal :: (Cod f ~ (~>)) -  => Cone f (Limit f)-  -> (forall n. Cone f n -> n ~> Limit f)-  -> LimitUniversal f-limitUniversal l lf = TerminalUniversal-  { tuObject           = coneVertex l-  , terminalMorphism   = l-  , terminalFactorizer = const lf-  }---- | A limit of the diagram @f@ is a cone of @f@.-limit :: LimitUniversal f -> Cone f (Limit f)-limit = terminalMorphism---- | For any other cone of @f@ with vertex @n@ there exists a unique morphism from @n@ to the limit of @f@.-limitFactorizer :: (Cod f ~ (~>)) => LimitUniversal f -> (forall n. Cone f n -> n ~> Limit f)-limitFactorizer lu c = terminalFactorizer lu (coneVertex c) c------ | Colimits in a category @(~>)@ by means of a diagram of type @j@, which is a functor from @j@ to @(~>)@.-type family ColimitFam j (~>) f :: *--type Colimit f = ColimitFam (Dom f) (Cod f) f---- | A colimit of @f@ is a universal morphism from @f@ to the diagonal functor.-type ColimitUniversal f = InitialUniversal f (DiagF f) (Colimit f)---- | @colimitUniversal@ is a helper function to create the universal property from the colimit and the colimit factorizer.-colimitUniversal :: (Cod f ~ (~>)) -  => Cocone f (Colimit f)-  -> (forall n. Cocone f n -> Colimit f ~> n)-  -> ColimitUniversal f-colimitUniversal l lf = InitialUniversal-  { iuObject          = coconeVertex l-  , initialMorphism   = l-  , initialFactorizer = const lf-  }---- | A colimit of the diagram @f@ is a co-cone of @f@.-colimit :: ColimitUniversal f -> Cocone f (Colimit f)-colimit = initialMorphism---- | For any other co-cone of @f@ with vertex @n@ there exists a unique morphism from the colimit of @f@ to @n@.-colimitFactorizer :: (Cod f ~ (~>)) => ColimitUniversal f -> (forall n. Cocone f n -> Colimit f ~> n)-colimitFactorizer cu c = initialFactorizer cu (coconeVertex c) c--- -- | An instance of @HasLimits j (~>)@ says that @(~>)@ has all limits of type @j@. class (Category j, Category (~>)) => HasLimits j (~>) where-  limitUniv :: Obj (Nat j (~>)) f -> LimitUniversal f+  limit           :: Obj (Nat j (~>)) f -> Cone f (Limit f)+  limitFactorizer :: Obj (Nat j (~>)) f -> (forall n. Cone f n -> n ~> Limit f)  -- | If every diagram of type @j@ has a limit in @(~>)@ there exists a limit functor. -- --   Applied to a natural transformation it is a generalisation of @(***)@: -- --   @l@ '***' @r =@ 'LimitFunctor' '%' 'arrowPair' @l r@-data LimitFunctor :: (* -> * -> *) -> (* -> * -> *) -> * where-  LimitFunctor :: HasLimits j (~>) => LimitFunctor j (~>)-+data LimitFunctor (j :: * -> * -> *) ((~>)  :: * -> * -> *) = LimitFunctor type instance Dom (LimitFunctor j (~>)) = Nat j (~>) type instance Cod (LimitFunctor j (~>)) = (~>) type instance LimitFunctor j (~>) :% f = LimitFam j (~>) f+instance HasLimits j (~>) => Functor (LimitFunctor j (~>)) where+  LimitFunctor % n @ Nat{}  = limitFactorizer (tgt n) (n . limit (src n)) -instance (Category j, Category (~>)) => Functor (LimitFunctor j (~>)) where-  LimitFunctor % n @ Nat{}  = limitFactorizer (limitUniv (tgt n)) (n . limit (limitUniv (src n)))+-- | The limit functor is right adjoint to the diagonal functor.+limitAdj :: HasLimits j (~>) => Adjunction (Nat j (~>)) (~>) (Diag j (~>)) (LimitFunctor j (~>))+limitAdj = mkAdjunction diag LimitFunctor (\a -> limitFactorizer (diag % a) (diag % a)) (\f @ Nat{} -> limit f)+  where diag = Diag -- Forces the type of all Diags to be the same.   +-- | Colimits in a category @(~>)@ by means of a diagram of type @j@, which is a functor from @j@ to @(~>)@.+type family ColimitFam j (~>) f :: *++type Colimit f = ColimitFam (Dom f) (Cod f) f+ -- | An instance of @HasColimits j (~>)@ says that @(~>)@ has all colimits of type @j@. class (Category j, Category (~>)) => HasColimits j (~>) where-  colimitUniv :: Obj (Nat j (~>)) f -> ColimitUniversal f+  colimit           :: Obj (Nat j (~>)) f -> Cocone f (Colimit f)+  colimitFactorizer :: Obj (Nat j (~>)) f -> (forall n. Cocone f n -> Colimit f ~> n)  -- | If every diagram of type @j@ has a colimit in @(~>)@ there exists a colimit functor. -- --   Applied to a natural transformation it is a generalisation of @(+++)@: -- --   @l@ '+++' @r =@ 'ColimitFunctor' '%' 'arrowPair' @l r@-data ColimitFunctor :: (* -> * -> *) -> (* -> * -> *) -> * where-  ColimitFunctor :: HasColimits j (~>) => ColimitFunctor j (~>)-  +data ColimitFunctor (j :: * -> * -> *) ((~>)  :: * -> * -> *) = ColimitFunctor type instance Dom (ColimitFunctor j (~>)) = Nat j (~>) type instance Cod (ColimitFunctor j (~>)) = (~>) type instance ColimitFunctor j (~>) :% f = ColimitFam j (~>) f--instance (Category j, Category (~>)) => Functor (ColimitFunctor j (~>)) where-  ColimitFunctor % n @ Nat{}  = colimitFactorizer (colimitUniv (src n)) (colimit (colimitUniv (tgt n)) . n)+instance HasColimits j (~>) => Functor (ColimitFunctor j (~>)) where+  ColimitFunctor % n @ Nat{}  = colimitFactorizer (src n) (colimit (tgt n) . n) +-- | The colimit functor is left adjoint to the diagonal functor.+colimitAdj :: HasColimits j (~>) => Adjunction (~>) (Nat j (~>)) (ColimitFunctor j (~>)) (Diag j (~>))+colimitAdj = mkAdjunction ColimitFunctor diag (\f @ Nat{} -> colimit f) (\a -> colimitFactorizer (diag % a) (diag % a)) +  where diag = Diag -- Forces the type of all Diags to be the same.+     -- | A terminal object is the limit of the functor from /0/ to (~>).@@ -244,9 +191,8 @@  instance (HasTerminalObject (~>)) => HasLimits Void (~>) where   -  limitUniv (Nat f _ _) = limitUniversal-    (voidNat (Const terminalObject) f)-    (terminate . coneVertex)+  limit (Nat f _ _) = voidNat (Const terminalObject) f+  limitFactorizer Nat{} = terminate . coneVertex   -- | @()@ is the terminal object in @Hask@.@@ -301,9 +247,8 @@  instance HasInitialObject (~>) => HasColimits Void (~>) where   -  colimitUniv (Nat f _ _) = colimitUniversal-    (voidNat f (Const initialObject))-    (initialize . coconeVertex)+  colimit (Nat f _ _) = voidNat f (Const initialObject)+  colimitFactorizer Nat{} = initialize . coconeVertex   data Zero@@ -358,30 +303,27 @@   (&&&) :: (a ~> x) -> (a ~> y) -> (a ~> BinaryProduct (~>) x y)    (***) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryProduct (~>) a1 a2 ~> BinaryProduct (~>) b1 b2)-  l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r)) where-+  l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r)) -type instance LimitFam (Discrete (S n)) (~>) f = BinaryProduct (~>) (f :% Z) (LimitFam (Discrete n) (~>) (Next f))+type instance LimitFam (Discrete (S n)) (~>) f = BinaryProduct (~>) (f :% Z) (LimitFam (Discrete n) (~>) (f :.: Succ n))  instance (HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) => HasLimits (Discrete (S n)) (~>) where   -  limitUniv (Nat l _ _) = limitUniv' l+  limit = limit'     where-      limitUniv' :: forall f. (Functor f, Dom f ~ Discrete (S n), Cod f ~ (~>), HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) -                 => f -> LimitUniversal f-      limitUniv' f = limitUniversal-        (Nat (Const $ x *** y) f (\z -> unCom $ h z))-        (\c -> c ! Z &&& limitFactorizer luNext (Nat (Const $ coneVertex c) (Next f) $ \n -> c ! S n))+      limit' :: forall f. Obj (Nat (Discrete (S n)) (~>)) f -> Cone f (Limit f)+      limit' l@Nat{} = Nat (Const $ x *** y) (srcF l) (\z -> unCom $ h z)         where-          x = f % Z+          x = l ! Z           y = coneVertex limNext-          limNext = limit luNext-          luNext = limitUniv (natId (Next f))+          limNext = limit (l `o` natId Succ)           h :: Obj (Discrete (S n)) z -> Com (ConstF f (LimitFam (Discrete (S n)) (~>) f)) f z           h Z     = Com $               proj1 x y           h (S n) = Com $ limNext ! n . proj2 x y +  limitFactorizer l@Nat{} c = c ! Z &&& limitFactorizer (l `o` natId Succ) ((c `o` natId Succ) . constPostcompInv (srcF c) Succ) + type instance BinaryProduct (->) x y = (x, y)  instance HasBinaryProducts (->) where@@ -453,28 +395,26 @@   (|||) :: (x ~> a) -> (y ~> a) -> (BinaryCoproduct (~>) x y ~> a)        (+++) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryCoproduct (~>) a1 a2 ~> BinaryCoproduct (~>) b1 b2)-  l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r) where+  l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r)      -type instance ColimitFam (Discrete (S n)) (~>) f = BinaryCoproduct (~>) (f :% Z) (ColimitFam (Discrete n) (~>) (Next f))+type instance ColimitFam (Discrete (S n)) (~>) f = BinaryCoproduct (~>) (f :% Z) (ColimitFam (Discrete n) (~>) (f :.: Succ n))  instance (HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) => HasColimits (Discrete (S n)) (~>) where   -  colimitUniv (Nat l _ _) = colimitUniv' l+  colimit = colimit'     where-      colimitUniv' :: forall f. (Functor f, Dom f ~ Discrete (S n), Cod f ~ (~>), HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) -                   => f -> ColimitUniversal f-      colimitUniv' f = colimitUniversal-        (Nat f (Const $ x +++ y) (\z -> unCom $ h z))-        (\c -> c ! Z ||| colimitFactorizer cluNext (Nat (Next f) (Const $ coconeVertex c) $ \n -> c ! S n))+      colimit' :: forall f. Obj (Nat (Discrete (S n)) (~>)) f -> Cocone f (Colimit f)+      colimit' l@Nat{} = Nat (srcF l) (Const $ x +++ y) (\z -> unCom $ h z)         where-          x = f % Z+          x = l ! Z           y = coconeVertex colNext-          colNext = colimit cluNext-          cluNext = colimitUniv (natId (Next f))+          colNext = colimit (l `o` natId Succ)           h :: Obj (Discrete (S n)) z -> Com f (ConstF f (ColimitFam (Discrete (S n)) (~>) f)) z           h Z     = Com $ inj1 x y           h (S n) = Com $ inj2 x y . colNext ! n+  +  colimitFactorizer l@Nat{} c = c ! Z ||| colimitFactorizer (l `o` natId Succ) (constPostcomp (tgtF c) Succ . (c `o` natId Succ))   type instance BinaryCoproduct (->) x y = Either x y@@ -536,21 +476,21 @@   Nat f1 f2 f +++ Nat g1 g2 g = Nat (f1 :+: g1) (f2 :+: g2) $ \z -> f z +++ g z  -newtype ForAll f = ForAll { unForAll :: forall a. f a }--type instance LimitFam (->) (->) (EndoHask f) = ForAll f--endoHaskLimit :: Prelude.Functor f => LimitUniversal (EndoHask f)-endoHaskLimit = limitUniversal-  (Nat (Const id) EndoHask $ \_ -> unForAll)-  (\c n -> ForAll ((c ! id) n)) -- ForAll . (c ! id)---data Exists f = forall a. Exists (f a)--type instance ColimitFam (->) (->) (EndoHask f) = Exists f--endoHaskColimit :: Prelude.Functor f => ColimitUniversal (EndoHask f)-endoHaskColimit = colimitUniversal-  (Nat EndoHask (Const id) $ \_ -> Exists)-  (\c (Exists fa) -> (c ! id) fa) -- (c ! id) . unExists+-- newtype ForAll f = ForAll { unForAll :: forall a. f :% a }+-- +-- type instance LimitFam (->) (->) f = ForAll f+-- +-- instance HasLimits (->) (->) where+--   +--   limit (Nat f _ _) = Nat (Const id) f $ \_ -> unForAll+--   limitFactorizer Nat{} c n = ForAll $ (c ! id) n -- ForAll . (c ! id)+-- +-- +-- data Exists f = forall a. Exists (f :% a)+-- +-- type instance ColimitFam (->) (->) f = Exists f+-- +-- instance HasColimits (->) (->) where+--   +--   colimit (Nat f _ _) = Nat f (Const id) $ \_ -> Exists+--   colimitFactorizer Nat{} c (Exists fa) = (c ! id) fa -- (c ! id) . unExists

@@ -19,8 +19,8 @@ import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation-import Data.Category.Adjunction (Adjunction, mkAdjunction, adjunctionMonad, adjunctionComonad, leftAdjunct, rightAdjunct)-import Data.Category.Monoidal+import Data.Category.Adjunction+import Data.Category.Monoidal as M  -- | The arrows are the values of the monoid. data MonoidA m a b where@@ -71,13 +71,13 @@ foldMap = unMonoidMorphism . rightAdjunct freeMonoidAdj (MonoidMorphism id)  listMonadReturn :: a -> [a]-listMonadReturn = unit (adjunctionMonad freeMonoidAdj) ! id+listMonadReturn = M.unit (adjunctionMonad freeMonoidAdj) ! id  listMonadJoin :: [[a]] -> [a]-listMonadJoin = multiply (adjunctionMonad freeMonoidAdj) ! id+listMonadJoin = M.multiply (adjunctionMonad freeMonoidAdj) ! id  listComonadExtract :: Monoid m => [m] -> m-listComonadExtract = let MonoidMorphism f = counit (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f+listComonadExtract = let MonoidMorphism f = M.counit (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f  listComonadDuplicate :: Monoid m => [m] -> [[m]]-listComonadDuplicate = let MonoidMorphism f = comultiply (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f+listComonadDuplicate = let MonoidMorphism f = M.comultiply (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f

@@ -18,9 +18,9 @@ import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation-import Data.Category.Product+import Data.Category.Adjunction (Adjunction(Adjunction)) import Data.Category.Limit-+import Data.Category.Product  class Functor f => HasUnit f where   @@ -47,13 +47,13 @@  class HasUnit f => TensorProduct f where   -  leftUnitor     :: Cod f ~ (~>) => f -> Obj (Cod f) a -> (f :% (Unit f, a)) ~> a-  leftUnitorInv  :: Cod f ~ (~>) => f -> Obj (Cod f) a -> a ~> (f :% (Unit f, a))-  rightUnitor    :: Cod f ~ (~>) => f -> Obj (Cod f) a -> (f :% (a, Unit f)) ~> a-  rightUnitorInv :: Cod f ~ (~>) => f -> Obj (Cod f) a -> a ~> (f :% (a, Unit f))+  leftUnitor     :: Cod f ~ (~>) => f -> Obj (~>) a -> (f :% (Unit f, a)) ~> a+  leftUnitorInv  :: Cod f ~ (~>) => f -> Obj (~>) a -> a ~> (f :% (Unit f, a))+  rightUnitor    :: Cod f ~ (~>) => f -> Obj (~>) a -> (f :% (a, Unit f)) ~> a+  rightUnitorInv :: Cod f ~ (~>) => f -> Obj (~>) a -> a ~> (f :% (a, Unit f))   -  associator     :: Cod f ~ (~>) => f -> Obj (Cod f) a -> Obj (Cod f) b -> Obj (Cod f) c -> (f :% (f :% (a, b), c)) ~> (f :% (a, f :% (b, c)))-  associatorInv  :: Cod f ~ (~>) => f -> Obj (Cod f) a -> Obj (Cod f) b -> Obj (Cod f) c -> (f :% (a, f :% (b, c))) ~> (f :% (f :% (a, b), c))+  associator     :: Cod f ~ (~>) => f -> Obj (~>) a -> Obj (~>) b -> Obj (~>) c -> (f :% (f :% (a, b), c)) ~> (f :% (a, f :% (b, c)))+  associatorInv  :: Cod f ~ (~>) => f -> Obj (~>) a -> Obj (~>) b -> Obj (~>) c -> (f :% (a, f :% (b, c))) ~> (f :% (f :% (a, b), c))   instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => TensorProduct (ProductFunctor (~>)) where@@ -78,13 +78,13 @@    instance Category (~>) => TensorProduct (FunctorCompose (~>)) where   -  leftUnitor     _ (Nat g _ _) = Nat (Id :.: g) g $ \i -> g % i-  leftUnitorInv  _ (Nat g _ _) = Nat g (Id :.: g) $ \i -> g % i-  rightUnitor    _ (Nat g _ _) = Nat (g :.: Id) g $ \i -> g % i-  rightUnitorInv _ (Nat g _ _) = Nat g (g :.: Id) $ \i -> g % i+  leftUnitor     _ (Nat g _ _) = idPostcomp g+  leftUnitorInv  _ (Nat g _ _) = idPostcompInv g+  rightUnitor    _ (Nat g _ _) = idPrecomp g+  rightUnitorInv _ (Nat g _ _) = idPrecompInv g -  associator    _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = Nat ((f :.: g) :.: h) (f :.: (g :.: h)) $ \i -> f % g % h % i-  associatorInv _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = Nat (f :.: (g :.: h)) ((f :.: g) :.: h) $ \i -> f % g % h % i+  associator    _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = compAssoc f g h+  associatorInv _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = compAssocInv f g h   @@ -147,3 +147,9 @@   , comultiply = Nat f (f :.: f) dupl   } ++adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f)+adjunctionMonad (Adjunction f g un coun) = mkMonad (g :.: f) (un !) ((Wrap g f % coun) !)++adjunctionComonad :: Adjunction c d f g -> Comonad (f :.: g)+adjunctionComonad (Adjunction f g un coun) = mkComonad (f :.: g) (coun !) ((Wrap f g % un) !)

@@ -18,10 +18,24 @@   , (!)   , o   , natId+  , srcF+  , tgtF    -- * Functor category   , Nat(..)   , Endo+  +  -- * Functor isomorphisms+  , compAssoc+  , compAssocInv+  , idPrecomp+  , idPrecompInv+  , idPostcomp+  , idPostcompInv+  , constPrecomp+  , constPrecompInv+  , constPostcomp+  , constPostcompInv        -- * Related functors   , FunctorCompose(..)@@ -29,19 +43,9 @@   , Postcompose(..)   , Wrap(..)   -  -- ** Presheaves-  , Presheaves-  , Representable(..)-  -  -- ** Yoneda-  , YonedaEmbedding(..)-  , Yoneda(..)-  , fromYoneda-  , toYoneda-   ) where   -import Prelude hiding ((.), id, Functor)+import Prelude hiding ((.), Functor)  import Data.Category import Data.Category.Functor@@ -81,7 +85,12 @@ natId :: Functor f => f -> Nat (Dom f) (Cod f) f f natId f = Nat f f $ \i -> f % i +srcF :: Nat c d f g -> f+srcF (Nat f _ _) = f +tgtF :: Nat c d f g -> g+tgtF (Nat _ g _) = g+ -- | Functor category D^C. -- Objects of D^C are functors from C to D. -- Arrows of D^C are natural transformations.@@ -93,6 +102,41 @@   Nat _ h ngh . Nat f _ nfg = Nat f h $ \i -> ngh i . nfg i  +compAssoc :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) +          => f -> g -> h -> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))+compAssoc f g h = Nat ((f :.: g) :.: h) (f :.: (g :.: h)) $ \i -> f % g % h % i++compAssocInv :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) +             => f -> g -> h -> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)+compAssocInv f g h = Nat (f :.: (g :.: h)) ((f :.: g) :.: h) $ \i -> f % g % h % i++idPrecomp :: Functor f => f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f+idPrecomp f = Nat (f :.: Id) f (f %)++idPrecompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))+idPrecompInv f = Nat f (f :.: Id) (f %)++idPostcomp :: Functor f => f -> Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f+idPostcomp f = Nat (Id :.: f) f (f %)++idPostcompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (Id (Cod f) :.: f)+idPostcompInv f = Nat f (Id :.: f) (f %)+++constPrecomp :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (f :.: Const c1 (Dom f) x) (Const c1 (Cod f) (f :% x))+constPrecomp (Const x) f = let fx = f % x in Nat (f :.: Const x) (Const fx) $ const fx++constPrecompInv :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (Const c1 (Cod f) (f :% x)) (f :.: Const c1 (Dom f) x)+constPrecompInv (Const x) f = let fx = f % x in Nat (Const fx) (f :.: Const x) $ const fx++constPostcomp :: Functor f => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 x)+constPostcomp (Const x) f = Nat (Const x :.: f) (Const x) $ const x++constPostcompInv :: Functor f => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Dom f) c2 x) (Const (Cod f) c2 x :.: f)+constPostcompInv (Const x) f = Nat (Const x) (Const x :.: f) $ const x+++ -- | The category of endofunctors. type Endo (~>) = Nat (~>) (~>) @@ -144,47 +188,3 @@  instance (Functor f, Functor h) => Functor (Wrap f h) where   Wrap f h % n = natId f `o` n `o` natId h---type Presheaves (~>) = Nat (Op (~>)) (->)---- | A functor F: Op(C) -> Set is representable if it is naturally isomorphic to the contravariant hom-functor.-class Functor f => Representable f where-  type RepresentingObject f :: *-  represent   :: (Dom f ~ Op c) => f -> (c :-*: RepresentingObject f) :~> f-  unrepresent :: (Dom f ~ Op c) => f -> f :~> (c :-*: RepresentingObject f)--instance Category (~>) => Representable ((~>) :-*: x) where-  type RepresentingObject ((~>) :-*: x) = x-  represent   f = natId f-  unrepresent f = natId f----- | The Yoneda embedding functor.-data YonedaEmbedding :: (* -> * -> *) -> * where-  YonedaEmbedding :: Category (~>) => YonedaEmbedding (~>)-  -type instance Dom (YonedaEmbedding (~>)) = (~>)-type instance Cod (YonedaEmbedding (~>)) = Nat (Op (~>)) (->)-type instance YonedaEmbedding (~>) :% a = (~>) :-*: a--instance Category (~>) => Functor (YonedaEmbedding (~>)) where-  YonedaEmbedding % f = Nat (Hom_X $ src f) (Hom_X $ tgt f) $ \_ -> (f .)---data Yoneda f = Yoneda-type instance Dom (Yoneda f) = Dom f-type instance Cod (Yoneda f) = (->)-type instance Yoneda f :% a = Nat (Dom f) (->) (a :*-: Dom f) f-instance Functor f => Functor (Yoneda f) where-  Yoneda % ab = \(Nat _ f n) -> Nat (HomX_ $ tgt ab) f $ \z bz -> n z (bz . ab)-      -  -fromYoneda :: (Functor f, Cod f ~ (->)) => f -> Nat (Dom f) (->) (Yoneda f) f-fromYoneda f = Nat Yoneda f $ \a n -> (n ! a) a--toYoneda :: (Functor f, Cod f ~ (->)) => f -> Nat (Dom f) (->) f (Yoneda f)-toYoneda f = Nat f Yoneda $ \a fa -> Nat (HomX_ a) f $ \_ h -> (f % h) fa---- Contravariant Yoneda:--- type instance Yoneda f :% a = Nat (Op (Dom f)) (->) (Dom f :-*: a) f

@@ -14,7 +14,6 @@ import Prelude ()  import Data.Category-import Data.Category.Functor   data (:**:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where@@ -27,50 +26,3 @@   tgt (a1 :**: a2)            = tgt a1 :**: tgt a2      (a1 :**: a2) . (b1 :**: b2) = (a1 . b1) :**: (a2 . b2)---  -  -    -data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1-type instance Dom (Proj1 c1 c2) = c1 :**: c2-type instance Cod (Proj1 c1 c2) = c1-type instance Proj1 c1 c2 :% (a1, a2) = a1-instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where -  Proj1 % (f1 :**: _) = f1--data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj2-type instance Dom (Proj2 c1 c2) = c1 :**: c2-type instance Cod (Proj2 c1 c2) = c2-type instance Proj2 c1 c2 :% (a1, a2) = a2-instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where -  Proj2 % (_ :**: f2) = f2--data f1 :***: f2 = f1 :***: f2-type instance Dom (f1 :***: f2) = Dom f1 :**: Dom f2-type instance Cod (f1 :***: f2) = Cod f1 :**: Cod f2-type instance (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)-instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where -  (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)-  -data DiagProd ((~>) :: * -> * -> *) = DiagProd-type instance Dom (DiagProd (~>)) = (~>)-type instance Cod (DiagProd (~>)) = (~>) :**: (~>)-type instance DiagProd (~>) :% a = (a, a)-instance Category (~>) => Functor (DiagProd (~>)) where -  DiagProd % f = f :**: f--data Tuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple1 (Obj c1 a)-type instance Dom (Tuple1 c1 c2 a1) = c2-type instance Cod (Tuple1 c1 c2 a1) = c1 :**: c2-type instance Tuple1 c1 c2 a1 :% a2 = (a1, a2)-instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1) where-  Tuple1 a % f = a :**: f--data Tuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple2 (Obj c2 a)-type instance Dom (Tuple2 c1 c2 a2) = c1-type instance Cod (Tuple2 c1 c2 a2) = c1 :**: c2-type instance Tuple2 c1 c2 a2 :% a1 = (a1, a2)-instance (Category c1, Category c2) => Functor (Tuple2 c1 c2 a2) where-  Tuple2 a % f = f :**: a-

@@ -0,0 +1,74 @@+{-# LANGUAGE TypeOperators, TypeFamilies, RankNTypes #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.RepresentableFunctor+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.RepresentableFunctor where++import Prelude (($), id)++import Data.Category+import Data.Category.Functor+++data Representable f repObj = Representable+  { representedFunctor :: f+  , representingObject :: Obj (Dom f) repObj+  , represent          :: (Dom f ~ (~>), Cod f ~ (->)) => Obj (~>) z -> f :% z -> repObj ~> z+  , universalElement   :: (Dom f ~ (~>), Cod f ~ (->)) => f :% repObj+  }++unrepresent :: (Functor f, Dom f ~ (~>), Cod f ~ (->)) => Representable f repObj -> repObj ~> z -> f :% z+unrepresent rep h = representedFunctor rep % h $ universalElement rep++covariantHomRepr :: Category (~>) => Obj (~>) x -> Representable (x :*-: (~>)) x+covariantHomRepr x = Representable+  { representedFunctor = homX_ x+  , representingObject = x+  , represent          = \_ -> id+  , universalElement   = x+  }++contravariantHomRepr :: Category (~>) => Obj (~>) x -> Representable ((~>) :-*: x) x+contravariantHomRepr x = Representable+  { representedFunctor = hom_X x+  , representingObject = Op x+  , represent          = \_ h -> Op h+  , universalElement   = x+  }++type InitialUniversal x u a = Representable ((x :*-: Cod u) :.: u) a+-- | An initial universal property, a universal morphism from x to u.+initialUniversal :: 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 obj mor factorizer = Representable+  { representedFunctor = homX_ (src mor) :.: u+  , representingObject = obj+  , represent          = factorizer+  , universalElement   = mor+  }+  +type TerminalUniversal x u a = Representable ((Cod u :-*: x) :.: Opposite u) a+-- | A terminal universal property, a universal morphism from u to x.+terminalUniversal :: 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 obj mor factorizer = Representable+  { representedFunctor = hom_X (tgt mor) :.: Opposite u+  , representingObject = Op obj+  , represent          = \(Op y) f -> Op (factorizer y f)+  , universalElement   = mor+  }

@@ -0,0 +1,48 @@+{-# LANGUAGE TypeOperators, TypeFamilies #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Yoneda+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Yoneda where++import Prelude (($))++import Data.Category+import Data.Category.Functor+import Data.Category.NaturalTransformation+import Data.Category.CartesianClosed++-- The Yoneda emedding is just the Hom functor in curried form:+-- curry (CatA Id) (CatA Id) (CatA Id) (CatA Hom)+-- leftAdjunct (curryAdj (CatA Id)) (CatA Id) (CatA Hom)+-- (ExponentialWith (CatA Id) % (CatA Hom)) . (tuple (CatA Id) (CatA Id))+-- CatA (Wrap Hom Id) . CatA CatTuple+-- CatA (Postcompose Hom :.: CatTuple)++-- | The Yoneda embedding functor.+yonedaEmbedding :: Category (~>) => Postcompose (Hom (~>)) (~>) :.: CatTuple (~>) (Op (~>))+yonedaEmbedding = Postcompose Hom :.: CatTuple+++data Yoneda f = Yoneda+type instance Dom (Yoneda f) = Dom f+type instance Cod (Yoneda f) = (->)+type instance Yoneda f :% a = Nat (Dom f) (->) (a :*-: Dom f) f+instance Functor f => Functor (Yoneda f) where+  Yoneda % ab = \n -> n . yonedaEmbedding % Op ab+      +  +fromYoneda :: (Functor f, Cod f ~ (->)) => f -> Yoneda f :~> f+fromYoneda f = Nat Yoneda f $ \a n -> (n ! a) a++toYoneda :: (Functor f, Cod f ~ (->)) => f -> f :~> Yoneda f+toYoneda f = Nat f Yoneda $ \a fa -> Nat (homX_ a) f $ \_ h -> (f % h) fa++-- Contravariant Yoneda:+-- type instance Yoneda f :% a = Nat (Op (Dom f)) (->) (Dom f :-*: a) f

@@ -1,5 +1,5 @@ name:                data-category-version:             0.3.1.1+version:             0.4 synopsis:            Restricted categories  description:         Data-category is a collection of categories, and some categorical constructions on them.@@ -31,6 +31,7 @@     Data.Category,     Data.Category.Functor,     Data.Category.NaturalTransformation,+    Data.Category.RepresentableFunctor,     Data.Category.Adjunction,     Data.Category.Limit,     Data.Category.Monoidal,@@ -38,6 +39,7 @@     Data.Category.Product,     Data.Category.Coproduct,     Data.Category.Discrete,+    Data.Category.Yoneda,     Data.Category.Monoid,     Data.Category.Boolean,     Data.Category.Omega,