data-category 0.10 → 0.11

raw patch · 29 files changed

+1268/−481 lines, 29 filesdep +basedep +ghc-primPVP ok

version bump matches the API change (PVP)

Dependencies added: base, ghc-prim

API changes (from Hackage documentation)

Files

• Data/Category.hs +17/−8
• Data/Category/Adjunction.hs +4/−4
• Data/Category/Boolean.hs +5/−3
• Data/Category/CartesianClosed.hs +12/−9
• Data/Category/Comma.hs +43/−6
• Data/Category/Coproduct.hs +24/−22
• Data/Category/Cube.hs +4/−2
• Data/Category/Dialg.hs +2/−2
• Data/Category/Enriched.hs +11/−289
• Data/Category/Enriched/Functor.hs +187/−0
• Data/Category/Enriched/Limit.hs +111/−0
• Data/Category/Enriched/Poset3.hs +84/−0
• Data/Category/Enriched/Yoneda.hs +56/−0
• Data/Category/Fin.hs +139/−0
• Data/Category/Fix.hs +4/−2
• Data/Category/Functor.hs +19/−46
• Data/Category/KanExtension.hs +6/−4
• Data/Category/Limit.hs +74/−19
• Data/Category/Monoidal.hs +62/−3
• Data/Category/NNO.hs +16/−14
• Data/Category/NaturalTransformation.hs +77/−10
• Data/Category/Preorder.hs +106/−0
• Data/Category/Product.hs +5/−3
• Data/Category/RepresentableFunctor.hs +8/−8
• Data/Category/Simplex.hs +27/−16
• Data/Category/Void.hs +3/−1
• Data/Category/WeightedLimit.hs +142/−0
• Data/Category/Yoneda.hs +7/−7
• data-category.cabal +13/−3

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, PolyKinds, NoImplicitPrelude #-}+{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, PolyKinds, LinearTypes, FlexibleInstances, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category@@ -18,10 +18,15 @@   -- * Opposite category   , Op(..) +  -- * `(->)`/Hask+  , obj+ ) where -infixr 8 .+import GHC.Exts+import Data.Kind (Type) +infixr 8 .  -- | Whenever objects are required at value level, they are represented by their identity arrows. type Obj k a = k a a@@ -35,12 +40,16 @@   (.) :: k b c -> k a b -> k a c  --- | The category with Haskell types as objects and Haskell functions as arrows.-instance Category (->) where+obj :: Obj (FUN m) a+obj x = x -  src _ = \x -> x-  tgt _ = \x -> x+-- | For @m ~ Many@: The category with Haskell types as objects and Haskell functions as arrows, i.e. @(->)@.+-- For @m ~ One@: The category with Haskell types as objects and Haskell linear functions as arrows, i.e. @(%1->)@.+instance Category (FUN m) where +  src _ = obj+  tgt _ = obj+   f . g = \x -> f (g x)  @@ -56,5 +65,5 @@   -- | @Kind k@ is the kind of the objects of the category @k@.-type family Kind (k :: o -> o -> *) :: * where-  Kind (k :: o -> o -> *) = o+type family Kind (k :: o -> o -> Type) :: Type where+  Kind (k :: o -> o -> Type) = o

@@ -104,8 +104,8 @@ -- | The category with categories as objects and adjunctions as arrows. instance Category AdjArrow where -  src (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj-  tgt (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj+  src (AdjArrow Adjunction{}) = AdjArrow idAdj+  tgt (AdjArrow Adjunction{}) = AdjArrow idAdj    AdjArrow x . AdjArrow y = AdjArrow (composeAdj x y) @@ -127,7 +127,7 @@  contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r) contAdj = mkAdjunction-  (Opposite (Hom_X (\x -> x)) :.: OpOpInv)-  (Hom_X (\x -> x))+  (Opposite (Hom_X obj) :.: OpOpInv)+  (Hom_X obj)   (\_ -> \(Op f) -> \b a -> f a b)   (\_ -> \f -> Op (\b a -> f a b))

@@ -14,6 +14,8 @@ ----------------------------------------------------------------------------- module Data.Category.Boolean where +import Data.Kind (Type)+ import Data.Category import Data.Category.Limit import Data.Category.Monoidal@@ -160,7 +162,7 @@ falseProductComonoid = ComonoidObject F2T Fls  -data Arrow k a b = Arrow (k a b)+newtype Arrow k a b = Arrow (k a b) -- | Any functor from the Boolean category points to an arrow in its target category. instance Category k => Functor (Arrow k a b) where   type Dom (Arrow k a b) = Boolean@@ -191,7 +193,7 @@ type TgtFunctor = ColimitFunctor Boolean  -data Terminator (k :: * -> * -> *) = Terminator+data Terminator (k :: Type -> Type -> Type) = Terminator -- | @Terminator k@ is the functor that sends an object to its terminating arrow. instance HasTerminalObject k => Functor (Terminator k) where   type Dom (Terminator k) = k@@ -206,7 +208,7 @@   (\_ n -> n ! Fls)  -data Initializer (k :: * -> * -> *) = Initializer+data Initializer (k :: Type -> Type -> Type) = Initializer -- | @Initializer k@ is the functor that sends an object to its initializing arrow. instance HasInitialObject k => Functor (Initializer k) where   type Dom (Initializer k) = k

@@ -10,6 +10,7 @@   UndecidableInstances,   TypeSynonymInstances,   FlexibleInstances,+  TupleSections,   NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- |@@ -22,6 +23,8 @@ ----------------------------------------------------------------------------- module Data.Category.CartesianClosed where +import Data.Kind (Type)+ import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -42,7 +45,7 @@   (^^^) :: k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)  -data ExpFunctor (k :: * -> * -> *) = ExpFunctor+data ExpFunctor (k :: Type -> Type -> Type) = ExpFunctor -- | The exponential as a bifunctor. instance CartesianClosed k => Functor (ExpFunctor k) where   type Dom (ExpFunctor k) = Op k :**: k@@ -61,7 +64,7 @@   type Exponential (->) y z = y -> z    apply _ _ (f, y) = f y-  tuple _ _ z      = \y -> (z, y)+  tuple _ _ z      = (z,)   f ^^^ h          = \g -> f . g . h  @@ -94,7 +97,7 @@   type Exponential (Presheaves k) y z = PShExponential k y z    apply yn@(Nat y _ _) zn@(Nat z _ _) = Nat (PshExponential yn zn :*: y) z (\(Op i) (n, yi) -> (n ! Op i) (i, yi))-  tuple yn zn@(Nat z _ _) = Nat z (PshExponential yn (zn *** yn)) (\(Op i) zi -> (Nat (Hom_X i) z (\_ j2i -> (z % Op j2i) zi) *** yn))+  tuple yn zn@(Nat z _ _) = Nat z (PshExponential yn (zn *** yn)) (\(Op i) zi -> Nat (Hom_X i) z (\_ j2i -> (z % Op j2i) zi) *** yn)   zn ^^^ yn = Nat (PshExponential (tgt yn) (src zn)) (PshExponential (src yn) (tgt zn)) (\(Op i) n -> zn . n . (natId (Hom_X i) *** yn))  @@ -109,26 +112,26 @@  -- | From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions, --   generalized to any cartesian closed category.-curry :: (CartesianClosed k, Kind k ~ *) => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z)+curry :: (CartesianClosed k, Kind k ~ Type) => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z) curry x y _ = leftAdjunct (curryAdj y) x -uncurry :: (CartesianClosed k, Kind k ~ *) => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z+uncurry :: (CartesianClosed k, Kind k ~ Type) => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z uncurry _ y z = rightAdjunct (curryAdj y) z  -- | From every adjunction we get a monad, in this case the State monad. type State k s a = Exponential k s (BinaryProduct k a s) -stateMonadReturn :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k a (State k s a)+stateMonadReturn :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k a (State k s a) stateMonadReturn s a = M.unit (adjunctionMonad (curryAdj s)) ! a -stateMonadJoin :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a)+stateMonadJoin :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a) stateMonadJoin s a = M.multiply (adjunctionMonad (curryAdj s)) ! a  -- ! From every adjunction we also get a comonad, the Context comonad in this case. type Context k s a = BinaryProduct k (Exponential k s a) s -contextComonadExtract :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (Context k s a) a+contextComonadExtract :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k (Context k s a) a contextComonadExtract s a = M.counit (adjunctionComonad (curryAdj s)) ! a -contextComonadDuplicate :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a))+contextComonadDuplicate :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a)) contextComonadDuplicate s a = M.comultiply (adjunctionComonad (curryAdj s)) ! a

@@ -12,17 +12,20 @@ ----------------------------------------------------------------------------- module Data.Category.Comma where +import Data.Kind (Type)+ import Data.Category+import Data.Category.Adjunction import Data.Category.Functor import Data.Category.Limit import Data.Category.RepresentableFunctor  -data CommaO :: * -> * -> * -> * where+data CommaO :: Type -> Type -> Type -> Type where   CommaO :: (Cod t ~ k, Cod s ~ k)     => Obj (Dom t) a -> k (t :% a) (s :% b) -> Obj (Dom s) b -> CommaO t s (a, b) -data (:/\:) :: * -> * -> * -> * -> * where+data (:/\:) :: Type -> Type -> Type -> Type -> Type where   CommaA ::     CommaO t s (a, b) ->     Dom t a a' ->@@ -48,9 +51,7 @@ type (c `ObjectsUnder` a) = Id c `ObjectsFUnder` a type (c `ObjectsOver`  a) = Id c `ObjectsFOver`  a -type Arrows c = Id c :/\: Id c - initialUniversalComma :: forall u x c a a_                        . (Functor u, c ~ (u `ObjectsFUnder` x), HasInitialObject c, (a_, a) ~ InitialObject c)                       => u -> InitialUniversal x u a@@ -59,7 +60,7 @@     initialUniversal u a mor factorizer       where         factorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y-        factorizer y arr = case (init (commaId (CommaO y arr y))) of CommaA _ _ f _ -> f+        factorizer y arr = case init (commaId (CommaO y arr y)) of CommaA _ _ f _ -> f           where             init :: Obj c (y, y) -> c (a_, a) (y, y)             init = initialize@@ -72,7 +73,43 @@     terminalUniversal u a mor factorizer       where         factorizer :: forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a-        factorizer y arr = case (term (commaId (CommaO y arr y))) of CommaA _ f _ _ -> f+        factorizer y arr = case term (commaId (CommaO y arr y)) of CommaA _ f _ _ -> f           where             term :: Obj c (y, y) -> c (y, y) (a, a_)             term = terminate+++type Arrows k = Id k :/\: Id k++data IdArrow (k :: Type -> Type -> Type) = IdArrow+instance Category k => Functor (IdArrow k) where+  type Dom (IdArrow k) = k+  type Cod (IdArrow k) = Arrows k+  type IdArrow k :% a = (a, a)+  IdArrow % f = CommaA+    (CommaO (src f) (src f) (src f))+    f+    f+    (CommaO (tgt f) (tgt f) (tgt f))++data Src (k :: Type -> Type -> Type) = Src+instance Category k => Functor (Src k) where+  type Dom (Src k) = Arrows k+  type Cod (Src k) = k+  type Src k :% (a, b) = a+  Src % (CommaA _ aa' _ _) = aa'++data Tgt (k :: Type -> Type -> Type) = Tgt+instance Category k => Functor (Tgt k) where+  type Dom (Tgt k) = Arrows k+  type Cod (Tgt k) = k+  type Tgt k :% (a, b) = b+  Tgt % (CommaA _ _ bb' _) = bb'++-- | Taking the target of an arrow is left adjoint to taking the identity of an object+tgtIdAdj :: Category k => Adjunction k (Arrows k) (Tgt k) (IdArrow k)+tgtIdAdj = mkAdjunctionUnits Tgt IdArrow (\(CommaA o@(CommaO _ ab b) _ _ _) -> CommaA o ab b (CommaO b b b)) (\o -> o)++-- | Taking the source of an arrow is right adjoint to taking the identity of an object+idSrcAdj :: Category k => Adjunction (Arrows k) k (IdArrow k) (Src k)+idSrcAdj = mkAdjunctionUnits IdArrow Src (\o -> o) (\(CommaA o@(CommaO a ab _) _ _ _) -> CommaA (CommaO a a a) a ab o)

@@ -10,6 +10,8 @@ ----------------------------------------------------------------------------- module Data.Category.Coproduct where +import Data.Kind (Type)+ import Data.Category import Data.Category.Functor @@ -21,13 +23,13 @@ data I1 a data I2 a -data (:++:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where+data (:++:) :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where   I1 :: c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)   I2 :: c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)  -- | The coproduct category of categories @c1@ and @c2@. instance (Category c1, Category c2) => Category (c1 :++: c2) where-  +   src (I1 a)      = I1 (src a)   src (I2 a)      = I2 (src a)   tgt (I1 a)      = I1 (tgt a)@@ -36,10 +38,10 @@   (I1 a) . (I1 b) = I1 (a . b)   (I2 a) . (I2 b) = I2 (a . b) -  -  -    -data Inj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj1++++data Inj1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Inj1 -- | 'Inj1' is a functor which injects into the left category. instance (Category c1, Category c2) => Functor (Inj1 c1 c2) where   type Dom (Inj1 c1 c2) = c1@@ -47,7 +49,7 @@   type Inj1 c1 c2 :% a = I1 a   Inj1 % f = I1 f -data Inj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj2+data Inj2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Inj2 -- | 'Inj2' is a functor which injects into the right category. instance (Category c1, Category c2) => Functor (Inj2 c1 c2) where   type Dom (Inj2 c1 c2) = c2@@ -64,8 +66,8 @@   type (f1 :+++: f2) :% (I2 a) = I2 (f2 :% a)   (g :+++: _) % I1 f = I1 (g % f)   (_ :+++: g) % I2 f = I2 (g % f)-  -data CodiagCoprod (k :: * -> * -> *) = CodiagCoprod++data CodiagCoprod (k :: Type -> Type -> Type) = CodiagCoprod -- | 'CodiagCoprod' is the codiagonal functor for coproducts. instance Category k => Functor (CodiagCoprod k) where   type Dom (CodiagCoprod k) = k :++: k@@ -75,7 +77,7 @@   CodiagCoprod % I1 f = f   CodiagCoprod % I2 f = f -data Cotuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple1 (Obj c1 a)+newtype Cotuple1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) a = Cotuple1 (Obj c1 a) -- | 'Cotuple1' projects out to the left category, replacing a value from the right category with a fixed object. instance (Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1) where   type Dom (Cotuple1 c1 c2 a1) = c1 :++: c2@@ -85,7 +87,7 @@   Cotuple1 _ % I1 f = f   Cotuple1 a % I2 _ = a -data Cotuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple2 (Obj c2 a)+newtype Cotuple2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) a = Cotuple2 (Obj c2 a) -- | 'Cotuple2' projects out to the right category, replacing a value from the left category with a fixed object. instance (Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2) where   type Dom (Cotuple2 c1 c2 a2) = c1 :++: c2@@ -96,13 +98,13 @@   Cotuple2 _ % I2 f = 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)-  +data Cograph c d f :: Type -> Type -> Type where+  I1A :: c a1 b1 -> Cograph c d f (I1 a1) (I1 b1)+  I2A :: d a2 b2 -> Cograph c d f (I2 a2) (I2 b2)+  I12 :: Obj c a -> Obj d b -> f -> f :% (a, b) -> Cograph c d f (I1 a) (I2 b)+ -- | The cograph of the profunctor @f@.-instance (Functor f, Dom f ~ (Op c :**: d), Cod f ~ (->), Category c, Category d) => Category (Cograph f) where+instance ProfunctorOf c d f => Category (Cograph c d f) where    src (I1A a)       = I1A (src a)   src (I2A a)       = I2A (src a)@@ -117,19 +119,19 @@   (I2A a) . (I2A b) = I2A (a . b)  -- | The directed coproduct category of categories @c1@ and @c2@.-newtype (c1 :>>: c2) a b = DC (Cograph (Const (Op c1 :**: c2) (->) ()) a b) deriving Category+newtype (c1 :>>: c2) a b = DC (Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b) deriving Category  -data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)+newtype NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)  -- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@. instance (Functor f, Functor g, Dom f ~ Dom g, Cod f ~ Cod g) => Functor (NatAsFunctor f g) where-  -  type Dom (NatAsFunctor f g) = Dom f :**: Cograph (Hom Unit)++  type Dom (NatAsFunctor f g) = Dom f :**: Cograph Unit Unit (Hom Unit)   type Cod (NatAsFunctor f g) = Cod f   type NatAsFunctor f g :% (a, I1 ()) = f :% a   type NatAsFunctor f g :% (a, I2 ()) = g :% a-  +   NatAsFunctor (Nat f _ _) % (a :**: I1A Unit) = f % a   NatAsFunctor (Nat _ g _) % (a :**: I2A Unit) = g % a   NatAsFunctor n           % (a :**: I12 Unit Unit Hom Unit) = n ! a

@@ -12,6 +12,8 @@ ----------------------------------------------------------------------------- module Data.Category.Cube where +import Data.Kind (Type)+ import Data.Category import Data.Category.Product import Data.Category.Functor@@ -25,7 +27,7 @@  data Sign = M | P -data Cube :: * -> * -> * where+data Cube :: Type -> Type -> Type where   Z :: Cube Z Z   S :: Cube x y -> Cube (S x) (S y)   Y :: Sign -> Cube x y -> Cube x (S y) -- face maps@@ -64,7 +66,7 @@  data Sign0 = SM | S0 | SP -data ACube :: * -> * where+data ACube :: Type -> Type where   Nil :: ACube Z   Cons :: Sign0 -> ACube n -> ACube (S n) 

@@ -79,13 +79,13 @@    type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) = NatNum -  initialObject = dialgId (Dialgebra (\x -> x) (Z :**: S))+  initialObject = dialgId (Dialgebra obj (Z :**: S))    initialize (dialgebra -> d@(Dialgebra _ (z :**: s))) = DialgA (dialgebra initialObject) d (primRec z s)   -data FreeAlg m = FreeAlg (Monad m)+newtype FreeAlg m = FreeAlg (Monad m) -- | @FreeAlg@ M takes @x@ to the free algebra @(M x, mu_x)@ of the monad @M@. instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (FreeAlg m) where   type Dom (FreeAlg m) = Dom m

@@ -5,10 +5,12 @@   , RankNTypes   , PatternSynonyms   , FlexibleContexts+  , FlexibleInstances   , NoImplicitPrelude   , UndecidableInstances   , ScopedTypeVariables   , ConstraintKinds+  , MultiParamTypeClasses   #-} ----------------------------------------------------------------------------- -- |@@ -21,21 +23,21 @@ ----------------------------------------------------------------------------- module Data.Category.Enriched where +import Data.Kind (Type)+ import Data.Category (Category(..), Obj, Op(..)) import Data.Category.Product import Data.Category.Functor (Functor(..), Hom(..))-import Data.Category.Limit hiding (HasLimits)-import Data.Category.CartesianClosed-import Data.Category.Boolean-+import Data.Category.Limit (HasBinaryProducts(..), HasTerminalObject(..))+import Data.Category.CartesianClosed (CartesianClosed(..), ExpFunctor(..), curry, uncurry)  -- | An enriched category-class CartesianClosed (V k) => ECategory (k :: * -> * -> *) where+class CartesianClosed (V k) => ECategory (k :: Type -> Type -> Type) where   -- | The category V which k is enriched in-  type V k :: * -> * -> *+  type V k :: Type -> Type -> Type    -- | The hom object in V from a to b-  type k $ ab :: *+  type k $ ab :: Type   hom :: Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))    id :: Obj k a -> Arr k a a@@ -67,7 +69,7 @@   comp (EOp a) (EOp b) (EOp c) = comp c b a . (proj2 (hom c b) (hom b a) &&& proj1 (hom c b) (hom b a))  -data (:<>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where+data (:<>:) :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where   (:<>:) :: (V k1 ~ V k2) => Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)  -- | The enriched product category of enriched categories @c1@ and @c2@.@@ -114,285 +116,5 @@   type V (InHask k) = (->)   type InHask k $ (a, b) = k a b   hom (InHask a) (InHask b) = Hom % (Op a :**: b)-  id (InHask f) () = f -- meh+  id (InHask f) () = f   comp _ _ _ (f, g) = f . g----- | Enriched functors.-class (ECategory (EDom ftag), ECategory (ECod ftag), V (EDom ftag) ~ V (ECod ftag)) => EFunctor ftag where--  -- | The domain, or source category, of the functor.-  type EDom ftag :: * -> * -> *-  -- | The codomain, or target category, of the functor.-  type ECod ftag :: * -> * -> *--  -- | @:%%@ maps objects at the type level-  type ftag :%% a :: *--  -- | @%%@ maps object at the value level-  (%%) :: ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)--  -- | `map` maps arrows.-  map :: (EDom ftag ~ k) => ftag -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))--type EFunctorOf a b t = (EFunctor t, EDom t ~ a, ECod t ~ b)---data Id (k :: * -> * -> *) = Id--- | The identity functor on k-instance ECategory k => EFunctor (Id k) where-  type EDom (Id k) = k-  type ECod (Id k) = k-  type Id k :%% a = a-  Id %% a = a-  map Id = hom--data (g :.: h) where-  (:.:) :: (EFunctor g, EFunctor h, ECod h ~ EDom g) => g -> h -> g :.: h--- | The composition of two functors.-instance (ECategory (ECod g), ECategory (EDom h), V (EDom h) ~ V (ECod g), ECod h ~ EDom g) => EFunctor (g :.: h) where-  type EDom (g :.: h) = EDom h-  type ECod (g :.: h) = ECod g-  type (g :.: h) :%% a = g :%% (h :%% a)-  (g :.: h) %% a = g %% (h %% a)-  map (g :.: h) a b = map g (h %% a) (h %% b) . map h a b--data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where-  Const :: Obj c2 x -> Const c1 c2 x--- | The constant functor.-instance (ECategory c1, ECategory c2, V c1 ~ V c2) => EFunctor (Const c1 c2 x) where-  type EDom (Const c1 c2 x) = c1-  type ECod (Const c1 c2 x) = c2-  type Const c1 c2 x :%% a = x-  Const x %% _ = x-  map (Const x) a b = id x . terminate (hom a b)--data Opposite f where-  Opposite :: EFunctor f => f -> Opposite f--- | The dual of a functor-instance (EFunctor f) => EFunctor (Opposite f) where-  type EDom (Opposite f) = EOp (EDom f)-  type ECod (Opposite f) = EOp (ECod f)-  type Opposite f :%% a = f :%% a-  Opposite f %% EOp a = EOp (f %% a)-  map (Opposite f) (EOp a) (EOp b) = map f b a--data f1 :<*>: f2 = f1 :<*>: f2--- | @f1 :<*>: f2@ is the product of the functors @f1@ and @f2@.-instance (EFunctor f1, EFunctor f2, V (ECod f1) ~ V (ECod f2)) => EFunctor (f1 :<*>: f2) where-  type EDom (f1 :<*>: f2) = EDom f1 :<>: EDom f2-  type ECod (f1 :<*>: f2) = ECod f1 :<>: ECod f2-  type (f1 :<*>: f2) :%% (a1, a2) = (f1 :%% a1, f2 :%% a2)-  (f1 :<*>: f2) %% (a1 :<>: a2) = (f1 %% a1) :<>: (f2 %% a2)-  map (f1 :<*>: f2) (a1 :<>: a2) (b1 :<>: b2) = map f1 a1 b1 *** map f2 a2 b2--data DiagProd (k :: * -> * -> *) = DiagProd--- | 'DiagProd' is the diagonal functor for products.-instance ECategory k => EFunctor (DiagProd k) where-  type EDom (DiagProd k) = k-  type ECod (DiagProd k) = k :<>: k-  type DiagProd k :%% a = (a, a)-  DiagProd %% a = a :<>: a-  map DiagProd a b = hom a b &&& hom a b--newtype UnderlyingF f = UnderlyingF f--- | The underlying functor of an enriched functor @f@-instance EFunctor f => Functor (UnderlyingF f) where-  type Dom (UnderlyingF f) = Underlying (EDom f)-  type Cod (UnderlyingF f) = Underlying (ECod f)-  type UnderlyingF f :% a = f :%% a-  UnderlyingF f % Underlying a ab b = Underlying (f %% a) (map f a b . ab) (f %% b)---data EHom (k :: * -> * -> *) = EHom-instance ECategory k => EFunctor (EHom k) where-  type EDom (EHom k) = EOp k :<>: k-  type ECod (EHom k) = Self (V k)-  type EHom k :%% (a, b) = k $ (a, b)-  EHom %% (EOp a :<>: b) = Self (hom a b)-  map EHom (EOp a1 :<>: a2) (EOp b1 :<>: b2) = curry (ba *** ab) a b (comp b1 a1 b2 . (comp a1 a2 b2 . (proj2 ba ab *** a) &&& proj1 ba ab . proj1 (ba *** ab) a))-    where-      a = hom a1 a2-      b = hom b1 b2-      ba = hom b1 a1-      ab = hom a2 b2----- | Enriched natural transformations.-data ENat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where-  ENat :: (EFunctorOf c d f, EFunctorOf c d g)-    => f -> g -> (forall z. Obj c z -> Arr d (f :%% z) (g :%% z)) -> ENat c d f g------ | The enriched functor @k(x, -)@-data EHomX_ k x = EHomX_ (Obj k x)-instance ECategory k => EFunctor (EHomX_ k x) where-  type EDom (EHomX_ k x) = k-  type ECod (EHomX_ k x) = Self (V k)-  type EHomX_ k x :%% y = k $ (x, y)-  EHomX_ x %% y = Self (hom x y)-  map (EHomX_ x) a b = curry (hom a b) (hom x a) (hom x b) (comp x a b)---- | The enriched functor @k(-, x)@-data EHom_X k x = EHom_X (Obj (EOp k) x)-instance ECategory k => EFunctor (EHom_X k x) where-  type EDom (EHom_X k x) = EOp k-  type ECod (EHom_X k x) = Self (V k)-  type EHom_X k x :%% y = k $ (y, x)-  EHom_X x %% y = Self (hom x y)-  map (EHom_X x) a b = curry (hom a b) (hom x a) (hom x b) (comp x a b)----type VProfunctor k l t = EFunctorOf (EOp k :<>: l) (Self (V k)) t--class CartesianClosed v => HasEnds v where-  type End (v :: * -> * -> *) t :: *-  end :: (VProfunctor k k t, V k ~ v) => t -> Obj v (End v t)-  endCounit :: (VProfunctor k k t, V k ~ v) => t -> Obj k a -> v (End v t) (t :%% (a, a))-  endFactorizer :: (VProfunctor k k t, V k ~ v) => t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)---newtype HaskEnd t = HaskEnd { getHaskEnd :: forall k a. VProfunctor k k t => t -> Obj k a -> t :%% (a, a) }-instance HasEnds (->) where-  type End (->) t = HaskEnd t-  end _ e = e-  endCounit t a (HaskEnd e) = e t a-  endFactorizer _ e x = HaskEnd (\_ a -> e a x)---data FunCat a b t s where-  FArr :: (EFunctorOf a b t, EFunctorOf a b s) => t -> s -> FunCat a b t s--type t :->>: s = EHom (ECod t) :.: (Opposite t :<*>: s)-(->>) :: (EFunctor t, EFunctor s, ECod t ~ ECod s, V (ECod t) ~ V (ECod s)) => t -> s -> t :->>: s-t ->> s = EHom :.: (Opposite t :<*>: s)--- | The enriched functor category @[a, b]@-instance (HasEnds (V a), V a ~ V b) => ECategory (FunCat a b) where-  type V (FunCat a b) = V a-  type FunCat a b $ (t, s) = End (V a) (t :->>: s)-  hom (FArr t _) (FArr s _) = end (t ->> s)-  id (FArr t _) = endFactorizer (t ->> t) (\a -> id (t %% a))-  comp (FArr t _) (FArr s _) (FArr r _) = endFactorizer (t ->> r)-    (\a -> comp (t %% a) (s %% a) (r %% a) . (endCounit (s ->> r) a *** endCounit (t ->> s) a))---data EndFunctor (k :: * -> * -> *) = EndFunctor-instance (HasEnds (V k), ECategory k) => EFunctor (EndFunctor k) where-  type EDom (EndFunctor k) = FunCat (EOp k :<>: k) (Self (V k))-  type ECod (EndFunctor k) = Self (V k)-  type EndFunctor k :%% t = End (V k) t-  EndFunctor %% (FArr t _) = Self (end t)-  map EndFunctor (FArr f _) (FArr g _) = curry (end (f ->> g)) (end f) (end g) (endFactorizer g (\a ->-    let aa = EOp a :<>: a in apply (getSelf (f %% aa)) (getSelf (g %% aa)) . (endCounit (f ->> g) aa *** endCounit f a)))----- d :: j -> k, w :: j -> Self (V k)-type family WeigtedLimit (k :: * -> * -> *) w d :: *-type Lim w d = WeigtedLimit (ECod d) w d--class HasEnds (V k) => HasLimits k where-  limitObj :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k (Lim w d)-  limit    :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHomX_ k e :.: d))) (k $ (e, Lim w d))-  limitInv :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k e -> V k (k $ (e, Lim w d)) (End (V k) (w :->>: (EHomX_ k e :.: d)))---- d :: j -> k, w :: EOp j -> Self (V k)-type family WeigtedColimit (k :: * -> * -> *) w d :: *-type Colim w d = WeigtedColimit (ECod d) w d--class HasEnds (V k) => HasColimits k where-  colimitObj :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k (Colim w d)-  colimit    :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHom_X k e :.: Opposite d))) (k $ (Colim w d, e))-  colimitInv :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (k $ (Colim w d, e)) (End (V k) (w :->>: (EHom_X k e :.: Opposite d)))---type instance WeigtedLimit (Self v) w d = End v (w :->>: d)-instance HasEnds v => HasLimits (Self v) where-  limitObj w d = Self (end (w ->> d))-  limit w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in curry (end wed) e (end (w ->> d))-    (endFactorizer (w ->> d) (\a -> let { Self wa = w %% a; Self da = d %% a } in apply e (da ^^^ wa) . (flip wa e da . endCounit wed a *** e)))-  limitInv w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in endFactorizer wed-    (\a -> let { Self wa = w %% a; Self da = d %% a } in flip e wa da . (endCounit (w ->> d) a ^^^ e))----yoneda    :: forall f k x. (HasEnds (V k), EFunctorOf k (Self (V k)) f) => f -> Obj k x -> V k (End (V k) (EHomX_ k x :->>: f)) (f :%% x)-yoneda f x = apply (hom x x) (getSelf (f %% x)) . (endCounit (EHomX_ x ->> f) x &&& id x . terminate (end (EHomX_ x ->> f)))--yonedaInv :: forall f k x. (HasEnds (V k), EFunctorOf k (Self (V k)) f) => f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f))-yonedaInv f x = endFactorizer (EHomX_ x ->> f) h-  where-    h :: Obj k a -> V k (f :%% x) (Exponential (V k) (k $ (x, a)) (f :%% a))-    h a = curry fx xa fa (apply fx fa . (map f x a . proj2 fx xa &&& proj1 fx xa))-      where-        xa = hom x a-        Self fx = f %% x-        Self fa = f %% a--data Y (k :: * -> * -> *) = Y--- | Yoneda embedding-instance (ECategory k, HasEnds (V k)) => EFunctor (Y k) where-  type EDom (Y k) = EOp k-  type ECod (Y k) = FunCat k (Self (V k))-  type Y k :%% x = EHomX_ k x-  Y %% EOp x = FArr (EHomX_ x) (EHomX_ x)-  map Y (EOp a) (EOp b) = yonedaInv (EHomX_ b) a---data One-data Two-data Three-data PosetTest a b where-  One :: PosetTest One One-  Two :: PosetTest Two Two-  Three :: PosetTest Three Three--type family Poset3 a b where-  Poset3 Two One = Fls-  Poset3 Three One = Fls-  Poset3 Three Two = Fls-  Poset3 a b = Tru-instance ECategory PosetTest where-  type V PosetTest = Boolean-  type PosetTest $ (a, b) = Poset3 a b-  hom One One = Tru-  hom One Two = Tru-  hom One Three = Tru-  hom Two One = Fls-  hom Two Two = Tru-  hom Two Three = Tru-  hom Three One = Fls-  hom Three Two = Fls-  hom Three Three = Tru--  id One = Tru-  id Two = Tru-  id Three = Tru-  comp One One One = Tru-  comp One One Two = Tru-  comp One One Three = Tru-  comp One Two One = F2T-  comp One Two Two = Tru-  comp One Two Three = Tru-  comp One Three One = F2T-  comp One Three Two = F2T-  comp One Three Three = Tru-  comp Two One One = Fls-  comp Two One Two = F2T-  comp Two One Three = F2T-  comp Two Two One = Fls-  comp Two Two Two = Tru-  comp Two Two Three = Tru-  comp Two Three One = Fls-  comp Two Three Two = F2T-  comp Two Three Three = Tru-  comp Three One One = Fls-  comp Three One Two = Fls-  comp Three One Three = F2T-  comp Three Two One = Fls-  comp Three Two Two = Fls-  comp Three Two Three = F2T-  comp Three Three One = Fls-  comp Three Three Two = Fls-  comp Three Three Three = Tru

@@ -0,0 +1,187 @@+{-# LANGUAGE+    TypeOperators+  , TypeFamilies+  , GADTs+  , RankNTypes+  , PatternSynonyms+  , FlexibleContexts+  , FlexibleInstances+  , NoImplicitPrelude+  , UndecidableInstances+  , ScopedTypeVariables+  , ConstraintKinds+  , MultiParamTypeClasses+  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Enriched.Functor+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Enriched.Functor where++import Data.Kind (Type)++import Data.Category (Category(..), Obj)+import Data.Category.Functor (Functor(..))+import Data.Category.Limit (HasBinaryProducts(..), HasTerminalObject(..))+import Data.Category.CartesianClosed+import Data.Category.Enriched++-- | Enriched functors.+class (ECategory (EDom ftag), ECategory (ECod ftag), V (EDom ftag) ~ V (ECod ftag)) => EFunctor ftag where++  -- | The domain, or source category, of the functor.+  type EDom ftag :: Type -> Type -> Type+  -- | The codomain, or target category, of the functor.+  type ECod ftag :: Type -> Type -> Type++  -- | @:%%@ maps objects at the type level+  type ftag :%% a :: Type++  -- | @%%@ maps object at the value level+  (%%) :: ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)++  -- | `map` maps arrows.+  map :: (EDom ftag ~ k) => ftag -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))++type EFunctorOf a b t = (EFunctor t, EDom t ~ a, ECod t ~ b)+++data Id (k :: Type -> Type -> Type) = Id+-- | The identity functor on k+instance ECategory k => EFunctor (Id k) where+  type EDom (Id k) = k+  type ECod (Id k) = k+  type Id k :%% a = a+  Id %% a = a+  map Id = hom++data (g :.: h) where+  (:.:) :: (EFunctor g, EFunctor h, ECod h ~ EDom g) => g -> h -> g :.: h+-- | The composition of two functors.+instance (ECategory (ECod g), ECategory (EDom h), V (EDom h) ~ V (ECod g), ECod h ~ EDom g) => EFunctor (g :.: h) where+  type EDom (g :.: h) = EDom h+  type ECod (g :.: h) = ECod g+  type (g :.: h) :%% a = g :%% (h :%% a)+  (g :.: h) %% a = g %% (h %% a)+  map (g :.: h) a b = map g (h %% a) (h %% b) . map h a b++data Const (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) x where+  Const :: Obj c2 x -> Const c1 c2 x+-- | The constant functor.+instance (ECategory c1, ECategory c2, V c1 ~ V c2) => EFunctor (Const c1 c2 x) where+  type EDom (Const c1 c2 x) = c1+  type ECod (Const c1 c2 x) = c2+  type Const c1 c2 x :%% a = x+  Const x %% _ = x+  map (Const x) a b = id x . terminate (hom a b)++data Opposite f where+  Opposite :: EFunctor f => f -> Opposite f+-- | The dual of a functor+instance (EFunctor f) => EFunctor (Opposite f) where+  type EDom (Opposite f) = EOp (EDom f)+  type ECod (Opposite f) = EOp (ECod f)+  type Opposite f :%% a = f :%% a+  Opposite f %% EOp a = EOp (f %% a)+  map (Opposite f) (EOp a) (EOp b) = map f b a++data f1 :<*>: f2 = f1 :<*>: f2+-- | @f1 :<*>: f2@ is the product of the functors @f1@ and @f2@.+instance (EFunctor f1, EFunctor f2, V (ECod f1) ~ V (ECod f2)) => EFunctor (f1 :<*>: f2) where+  type EDom (f1 :<*>: f2) = EDom f1 :<>: EDom f2+  type ECod (f1 :<*>: f2) = ECod f1 :<>: ECod f2+  type (f1 :<*>: f2) :%% (a1, a2) = (f1 :%% a1, f2 :%% a2)+  (f1 :<*>: f2) %% (a1 :<>: a2) = (f1 %% a1) :<>: (f2 %% a2)+  map (f1 :<*>: f2) (a1 :<>: a2) (b1 :<>: b2) = map f1 a1 b1 *** map f2 a2 b2++data DiagProd (k :: Type -> Type -> Type) = DiagProd+-- | 'DiagProd' is the diagonal functor for products.+instance ECategory k => EFunctor (DiagProd k) where+  type EDom (DiagProd k) = k+  type ECod (DiagProd k) = k :<>: k+  type DiagProd k :%% a = (a, a)+  DiagProd %% a = a :<>: a+  map DiagProd a b = hom a b &&& hom a b++newtype UnderlyingF f = UnderlyingF f+-- | The underlying functor of an enriched functor @f@+instance EFunctor f => Functor (UnderlyingF f) where+  type Dom (UnderlyingF f) = Underlying (EDom f)+  type Cod (UnderlyingF f) = Underlying (ECod f)+  type UnderlyingF f :% a = f :%% a+  UnderlyingF f % Underlying a ab b = Underlying (f %% a) (map f a b . ab) (f %% b)++newtype InHaskF f = InHaskF f+-- | A regular functor is a functor enriched in Hask.+instance Functor f => EFunctor (InHaskF f) where+  type EDom (InHaskF f) = InHask (Dom f)+  type ECod (InHaskF f) = InHask (Cod f)+  type InHaskF f :%% a = f :% a+  InHaskF f %% InHask a = InHask (f % a)+  map (InHaskF f) _ _ = \g -> f % g++newtype InHaskToHask f = InHaskToHask f+instance (Functor f, Cod f ~ (->)) => EFunctor (InHaskToHask f) where+  type EDom (InHaskToHask f) = InHask (Dom f)+  type ECod (InHaskToHask f) = Self (->)+  type InHaskToHask f :%% a = f :% a+  InHaskToHask f %% InHask a = Self (f % a)+  map (InHaskToHask f) _ _ = \g -> f % g++newtype UnderlyingHask (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) f = UnderlyingHask f+-- | The underlying functor of an enriched functor @f@ enriched in Hask.+instance (EFunctor f, EDom f ~ InHask c, ECod f ~ InHask d, Category c, Category d) => Functor (UnderlyingHask c d f) where+  type Dom (UnderlyingHask c d f) = c+  type Cod (UnderlyingHask c d f) = d+  type UnderlyingHask c d f :% a = f :%% a+  UnderlyingHask f % g = map f (InHask (src g)) (InHask (tgt g)) g++data EHom (k :: Type -> Type -> Type) = EHom+instance ECategory k => EFunctor (EHom k) where+  type EDom (EHom k) = EOp k :<>: k+  type ECod (EHom k) = Self (V k)+  type EHom k :%% (a, b) = k $ (a, b)+  EHom %% (EOp a :<>: b) = Self (hom a b)+  map EHom (EOp a1 :<>: a2) (EOp b1 :<>: b2) = curry (ba *** ab) a b (comp b1 a1 b2 . (comp a1 a2 b2 . (proj2 ba ab *** a) &&& proj1 ba ab . proj1 (ba *** ab) a))+    where+      a = hom a1 a2+      b = hom b1 b2+      ba = hom b1 a1+      ab = hom a2 b2++-- | The enriched functor @k(x, -)@+data EHomX_ k x = EHomX_ (Obj k x)+instance ECategory k => EFunctor (EHomX_ k x) where+  type EDom (EHomX_ k x) = k+  type ECod (EHomX_ k x) = Self (V k)+  type EHomX_ k x :%% y = k $ (x, y)+  EHomX_ x %% y = Self (hom x y)+  map (EHomX_ x) a b = curry (hom a b) (hom x a) (hom x b) (comp x a b)++-- | The enriched functor @k(-, x)@+data EHom_X k x = EHom_X (Obj (EOp k) x)+instance ECategory k => EFunctor (EHom_X k x) where+  type EDom (EHom_X k x) = EOp k+  type ECod (EHom_X k x) = Self (V k)+  type EHom_X k x :%% y = k $ (y, x)+  EHom_X x %% y = Self (hom x y)+  map (EHom_X x) a b = curry (hom a b) (hom x a) (hom x b) (comp x a b)+++-- | A V-enrichment on a functor @F: V -> V@ is the same thing as tensorial strength @(a, f b) -> f (a, b)@.+strength :: EFunctorOf (Self v) (Self v) f => f -> Obj v a -> Obj v b -> v (BinaryProduct v a (f :%% b)) (f :%% (BinaryProduct v a b))+strength f a b = uncurry a fb fab (map f (Self b) (Self (a *** b)) . tuple b a)+  where+    Self fb = f %% Self b+    Self fab = f %% Self (a *** b)+++-- | Enriched natural transformations.+data ENat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where+  ENat :: (EFunctorOf c d f, EFunctorOf c d g)+    => f -> g -> (forall z. Obj c z -> Arr d (f :%% z) (g :%% z)) -> ENat c d f g

@@ -0,0 +1,111 @@+{-# LANGUAGE+    TypeOperators+  , TypeFamilies+  , GADTs+  , RankNTypes+  , PatternSynonyms+  , FlexibleContexts+  , FlexibleInstances+  , NoImplicitPrelude+  , UndecidableInstances+  , ScopedTypeVariables+  , ConstraintKinds+  , MultiParamTypeClasses+  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Enriched.Limit+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Enriched.Limit where++import Data.Kind (Type)++import Data.Category (Category(..), Obj)+import Data.Category.Functor (Functor(..))+import Data.Category.Limit (HasBinaryProducts(..))+import Data.Category.CartesianClosed (CartesianClosed(..), curry, flip)+import qualified Data.Category.WeightedLimit as Hask+import Data.Category.Enriched+import Data.Category.Enriched.Functor++type VProfunctor k l t = EFunctorOf (EOp k :<>: l) (Self (V k)) t++class CartesianClosed v => HasEnds v where+  type End (v :: Type -> Type -> Type) t :: Type+  end :: (VProfunctor k k t, V k ~ v) => t -> Obj v (End v t)+  endCounit :: (VProfunctor k k t, V k ~ v) => t -> Obj k a -> v (End v t) (t :%% (a, a))+  endFactorizer :: (VProfunctor k k t, V k ~ v) => t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)+++newtype HaskEnd t = HaskEnd { getHaskEnd :: forall k a. VProfunctor k k t => t -> Obj k a -> t :%% (a, a) }+instance HasEnds (->) where+  type End (->) t = HaskEnd t+  end _ e = e+  endCounit t a (HaskEnd e) = e t a+  endFactorizer _ e x = HaskEnd (\_ a -> e a x)+++data FunCat a b t s where+  FArr :: (EFunctorOf a b t, EFunctorOf a b s) => t -> s -> FunCat a b t s++type t :->>: s = EHom (ECod t) :.: (Opposite t :<*>: s)+(->>) :: (EFunctor t, EFunctor s, ECod t ~ ECod s, V (ECod t) ~ V (ECod s)) => t -> s -> t :->>: s+t ->> s = EHom :.: (Opposite t :<*>: s)+-- | The enriched functor category @[a, b]@+instance (HasEnds (V a), CartesianClosed (V a), V a ~ V b) => ECategory (FunCat a b) where+  type V (FunCat a b) = V a+  type FunCat a b $ (t, s) = End (V a) (t :->>: s)+  hom (FArr t _) (FArr s _) = end (t ->> s)+  id (FArr t _) = endFactorizer (t ->> t) (\a -> id (t %% a))+  comp (FArr t _) (FArr s _) (FArr r _) = endFactorizer (t ->> r)+    (\a -> comp (t %% a) (s %% a) (r %% a) . (endCounit (s ->> r) a *** endCounit (t ->> s) a))+++data EndFunctor (k :: Type -> Type -> Type) = EndFunctor+instance (HasEnds (V k), ECategory k) => EFunctor (EndFunctor k) where+  type EDom (EndFunctor k) = FunCat (EOp k :<>: k) (Self (V k))+  type ECod (EndFunctor k) = Self (V k)+  type EndFunctor k :%% t = End (V k) t+  EndFunctor %% (FArr t _) = Self (end t)+  map EndFunctor (FArr f _) (FArr g _) = curry (end (f ->> g)) (end f) (end g) (endFactorizer g (\a ->+    let aa = EOp a :<>: a in apply (getSelf (f %% aa)) (getSelf (g %% aa)) . (endCounit (f ->> g) aa *** endCounit f a)))+++-- d :: j -> k, w :: j -> Self (V k)+type family WeigtedLimit (k :: Type -> Type -> Type) w d :: Type+type Lim w d = WeigtedLimit (ECod d) w d++class (HasEnds (V k), EFunctor w, ECod w ~ Self (V k)) => HasLimits k w where+  limitObj :: EFunctorOf (EDom w) k d => w -> d -> Obj k (Lim w d)+  limit    :: EFunctorOf (EDom w) k d => w -> d -> Obj k e -> V k (k $ (e, Lim w d)) (End (V k) (w :->>: (EHomX_ k e :.: d)))+  limitInv :: EFunctorOf (EDom w) k d => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHomX_ k e :.: d))) (k $ (e, Lim w d))++-- d :: j -> k, w :: EOp j -> Self (V k)+type family WeigtedColimit (k :: Type -> Type -> Type) w d :: Type+type Colim w d = WeigtedColimit (ECod d) w d++class (HasEnds (V k), EFunctor w, ECod w ~ Self (V k)) => HasColimits k w where+  colimitObj :: (EFunctorOf j k d, EOp j ~ EDom w) => w -> d -> Obj k (Colim w d)+  colimit    :: (EFunctorOf j k d, EOp j ~ EDom w) => w -> d -> Obj k e -> V k (k $ (Colim w d, e)) (End (V k) (w :->>: (EHom_X k e :.: Opposite d)))+  colimitInv :: (EFunctorOf j k d, EOp j ~ EDom w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHom_X k e :.: Opposite d))) (k $ (Colim w d, e))+++type instance WeigtedLimit (Self v) w d = End v (w :->>: d)+instance (HasEnds v, EFunctor w, ECod w ~ Self v) => HasLimits (Self v) w where+  limitObj w d = Self (end (w ->> d))+  limit    w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in endFactorizer wed+    (\a -> let { Self wa = w %% a; Self da = d %% a } in flip e wa da . (endCounit (w ->> d) a ^^^ e))+  limitInv w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in curry (end wed) e (end (w ->> d))+    (endFactorizer (w ->> d) (\a -> let { Self wa = w %% a; Self da = d %% a } in apply e (da ^^^ wa) . (flip wa e da . endCounit wed a *** e)))++type instance WeigtedLimit (InHask k) (InHaskToHask w) d = Hask.WeightedLimit k w (UnderlyingHask (Dom w) k d)+instance Hask.HasWLimits k w => HasLimits (InHask k) (InHaskToHask w) where+  limitObj (InHaskToHask w) d = InHask (Hask.limitObj w (UnderlyingHask d))+  limit    (InHaskToHask w) d _ el = HaskEnd (\_ (InHask a) wa -> Hask.limit w (UnderlyingHask d) a wa . el)+  limitInv (InHaskToHask w) d (InHask e) (HaskEnd n) =+    Hask.limitFactorizer w (UnderlyingHask d) e (n (InHaskToHask w ->> (EHomX_ (InHask e) :.: d)) . InHask)

@@ -0,0 +1,84 @@+{-# LANGUAGE+    TypeOperators+  , TypeFamilies+  , GADTs+  , RankNTypes+  , PatternSynonyms+  , FlexibleContexts+  , FlexibleInstances+  , NoImplicitPrelude+  , UndecidableInstances+  , ScopedTypeVariables+  , ConstraintKinds+  , MultiParamTypeClasses+  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Enriched.Poset3+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Enriched.Poset3 where++import Data.Category.Boolean+import Data.Category.Enriched++data One+data Two+data Three+data PosetTest a b where+  One :: PosetTest One One+  Two :: PosetTest Two Two+  Three :: PosetTest Three Three++type family Poset3 a b where+  Poset3 Two One = Fls+  Poset3 Three One = Fls+  Poset3 Three Two = Fls+  Poset3 a b = Tru+instance ECategory PosetTest where+  type V PosetTest = Boolean+  type PosetTest $ (a, b) = Poset3 a b+  hom One One = Tru+  hom One Two = Tru+  hom One Three = Tru+  hom Two One = Fls+  hom Two Two = Tru+  hom Two Three = Tru+  hom Three One = Fls+  hom Three Two = Fls+  hom Three Three = Tru++  id One = Tru+  id Two = Tru+  id Three = Tru+  comp One One One = Tru+  comp One One Two = Tru+  comp One One Three = Tru+  comp One Two One = F2T+  comp One Two Two = Tru+  comp One Two Three = Tru+  comp One Three One = F2T+  comp One Three Two = F2T+  comp One Three Three = Tru+  comp Two One One = Fls+  comp Two One Two = F2T+  comp Two One Three = F2T+  comp Two Two One = Fls+  comp Two Two Two = Tru+  comp Two Two Three = Tru+  comp Two Three One = Fls+  comp Two Three Two = F2T+  comp Two Three Three = Tru+  comp Three One One = Fls+  comp Three One Two = Fls+  comp Three One Three = F2T+  comp Three Two One = Fls+  comp Three Two Two = Fls+  comp Three Two Three = F2T+  comp Three Three One = Fls+  comp Three Three Two = Fls+  comp Three Three Three = Tru

@@ -0,0 +1,56 @@+{-# LANGUAGE+    TypeOperators+  , TypeFamilies+  , GADTs+  , RankNTypes+  , PatternSynonyms+  , FlexibleContexts+  , FlexibleInstances+  , NoImplicitPrelude+  , UndecidableInstances+  , ScopedTypeVariables+  , ConstraintKinds+  , MultiParamTypeClasses+  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Enriched.Yoneda+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Enriched.Yoneda where++import Data.Kind (Type)++import Data.Category (Category(..), Obj)+import Data.Category.CartesianClosed (CartesianClosed(..), curry)+import Data.Category.Limit (HasBinaryProducts(..), HasTerminalObject(..))+import Data.Category.Enriched+import Data.Category.Enriched.Functor+import Data.Category.Enriched.Limit+++yoneda    :: forall f k x. (HasEnds (V k), EFunctorOf k (Self (V k)) f) => f -> Obj k x -> V k (End (V k) (EHomX_ k x :->>: f)) (f :%% x)+yoneda f x = apply (hom x x) (getSelf (f %% x)) . (endCounit (EHomX_ x ->> f) x &&& id x . terminate (end (EHomX_ x ->> f)))++yonedaInv :: forall f k x. (HasEnds (V k), EFunctor f, EDom f ~ k, ECod f ~ Self (V k)) => f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f))+yonedaInv f x = endFactorizer (EHomX_ x ->> f) h+  where+    h :: Obj k a -> V k (f :%% x) (Exponential (V k) (k $ (x, a)) (f :%% a))+    h a = curry fx xa fa (apply fx fa . (map f x a . proj2 fx xa &&& proj1 fx xa))+      where+        xa = hom x a+        Self fx = f %% x+        Self fa = f %% a++data Y (k :: Type -> Type -> Type) = Y+-- | Yoneda embedding+instance (ECategory k, HasEnds (V k)) => EFunctor (Y k) where+  type EDom (Y k) = EOp k+  type ECod (Y k) = FunCat k (Self (V k))+  type Y k :%% x = EHomX_ k x+  Y %% EOp x = FArr (EHomX_ x) (EHomX_ x)+  map Y (EOp a) (EOp b) = yonedaInv (EHomX_ b) a

@@ -0,0 +1,139 @@+{-# LANGUAGE TypeFamilies, GADTs, PolyKinds, DataKinds, FlexibleInstances, FlexibleContexts, UndecidableInstances, NoImplicitPrelude #-}+{-# LANGUAGE EmptyCase, TypeApplications, ScopedTypeVariables, TypeOperators #-}+module Data.Category.Fin where++import Data.Category+import Data.Category.Limit+import Data.Category.CartesianClosed++data Nat = Z | S Nat++data Fin n where+  FZ :: Fin ('S n)+  FS :: Fin n -> Fin ('S n)++data LTE (n :: Nat) (a :: Fin n) (b :: Fin n) where+  ZEQ :: LTE ('S m) 'FZ 'FZ+  ZLT :: LTE ('S m) 'FZ  b -> LTE ('S ('S m))  'FZ    ('FS b)+  SLT :: LTE ('S m)  a   b -> LTE ('S ('S m)) ('FS a) ('FS b)++instance Category (LTE n) where+  src ZEQ = ZEQ+  src (ZLT _) = ZEQ+  src (SLT a) = SLT (src a)+  tgt ZEQ = ZEQ+  tgt (ZLT a) = SLT (tgt a)+  tgt (SLT a) = SLT (tgt a)+  ZEQ . a = a+  a . ZEQ = a+  SLT a . ZLT b = ZLT (a . b)+  SLT a . SLT b = SLT (a . b)++instance HasInitialObject (LTE ('S n)) where+  type InitialObject (LTE ('S n)) = 'FZ+  initialObject = ZEQ+  initialize ZEQ = ZEQ+  initialize (SLT a) = ZLT (initialize a)++instance HasTerminalObject (LTE ('S 'Z)) where+  type TerminalObject (LTE ('S 'Z)) = 'FZ+  terminalObject = ZEQ+  terminate ZEQ = ZEQ++instance HasTerminalObject (LTE ('S n)) => HasTerminalObject (LTE ('S ('S n))) where+  type TerminalObject (LTE ('S ('S n))) = 'FS (TerminalObject (LTE ('S n)))+  terminalObject = SLT terminalObject+  terminate ZEQ = ZLT (terminate ZEQ)+  terminate (SLT a) = SLT (terminate a)++instance HasBinaryCoproducts (LTE ('S 'Z)) where+  type BinaryCoproduct (LTE ('S 'Z)) 'FZ 'FZ = 'FZ+  inj1 ZEQ ZEQ = ZEQ+  inj2 ZEQ ZEQ = ZEQ+  ZEQ ||| ZEQ = ZEQ++instance HasBinaryCoproducts (LTE ('S n)) => HasBinaryCoproducts (LTE ('S ('S n))) where+  type BinaryCoproduct (LTE ('S ('S n))) 'FZ 'FZ = 'FZ+  type BinaryCoproduct (LTE ('S ('S n))) 'FZ ('FS b) = 'FS (BinaryCoproduct (LTE ('S n)) 'FZ b)+  type BinaryCoproduct (LTE ('S ('S n))) ('FS a) 'FZ = 'FS (BinaryCoproduct (LTE ('S n)) a 'FZ)+  type BinaryCoproduct (LTE ('S ('S n))) ('FS a) ('FS b) = 'FS (BinaryCoproduct (LTE ('S n)) a b)+  inj1 ZEQ ZEQ = ZEQ+  inj1 ZEQ (SLT a) = ZLT (inj1 ZEQ a)+  inj1 (SLT a) ZEQ = SLT (inj1 a ZEQ)+  inj1 (SLT a) (SLT b) = SLT (inj1 a b)+  inj2 ZEQ ZEQ = ZEQ+  inj2 ZEQ (SLT a) = SLT (inj2 ZEQ a)+  inj2 (SLT a) ZEQ = ZLT (inj2 a ZEQ)+  inj2 (SLT a) (SLT b) = SLT (inj2 a b)+  ZEQ ||| ZEQ = ZEQ+  ZLT a ||| ZLT b = ZLT (case a ||| b of { ZEQ -> ZEQ; ZLT n -> ZLT n })+  ZLT a ||| SLT b = SLT (a ||| b)+  SLT a ||| ZLT b = SLT (a ||| b)+  SLT a ||| SLT b = SLT (a ||| b)++instance HasBinaryProducts (LTE ('S 'Z)) where+  type BinaryProduct (LTE ('S 'Z)) 'FZ 'FZ = 'FZ+  proj1 ZEQ ZEQ = ZEQ+  proj2 ZEQ ZEQ = ZEQ+  ZEQ &&& ZEQ = ZEQ++instance HasBinaryProducts (LTE ('S n)) => HasBinaryProducts (LTE ('S ('S n))) where+  type BinaryProduct (LTE ('S ('S n))) 'FZ 'FZ = 'FZ+  type BinaryProduct (LTE ('S ('S n))) 'FZ ('FS b) = 'FZ+  type BinaryProduct (LTE ('S ('S n))) ('FS a) 'FZ = 'FZ+  type BinaryProduct (LTE ('S ('S n))) ('FS a) ('FS b) = 'FS (BinaryProduct (LTE ('S n)) a b)+  proj1 ZEQ ZEQ = ZEQ+  proj1 ZEQ (SLT _) = ZEQ+  proj1 (SLT a) ZEQ = ZLT (case proj1 a ZEQ of { ZEQ -> ZEQ; ZLT n -> ZLT n })+  proj1 (SLT a) (SLT b) = SLT (proj1 a b)+  proj2 ZEQ ZEQ = ZEQ+  proj2 ZEQ (SLT a) = ZLT (case proj2 ZEQ a of { ZEQ -> ZEQ; ZLT n -> ZLT n })+  proj2 (SLT _) ZEQ = ZEQ+  proj2 (SLT a) (SLT b) = SLT (proj2 a b)+  ZEQ &&& ZEQ = ZEQ+  ZEQ &&& ZLT _ = ZEQ+  ZLT _ &&& ZEQ = ZEQ+  ZLT a &&& ZLT b = ZLT (a &&& b)+  SLT a &&& SLT b = SLT (a &&& b)++data Proof a n where+  Proof :: (BinaryProduct (LTE ('S n)) 'FZ a ~ 'FZ, BinaryProduct (LTE ('S n)) a 'FZ ~ 'FZ) => Proof a n+proof :: Obj (LTE ('S n)) a -> Proof a n+proof = proof -- trust me++instance CartesianClosed (LTE ('S 'Z)) where+  type Exponential (LTE ('S 'Z)) 'FZ 'FZ = 'FZ+  apply ZEQ ZEQ = ZEQ+  tuple ZEQ ZEQ = ZEQ+  ZEQ ^^^ ZEQ = ZEQ++-- b -> c = max(a: min(a, b) <= c)+-- → 0 1 2 3+--  +-------+-- 0|3 3 3 3+-- 1|0 3 3 3+-- 2|0 1 3 3+-- 3|0 1 2 3+instance CartesianClosed (LTE ('S n)) => CartesianClosed (LTE ('S ('S n))) where+  type Exponential (LTE ('S ('S n))) 'FZ 'FZ = 'FS (Exponential (LTE ('S n)) 'FZ 'FZ)+  type Exponential (LTE ('S ('S n))) 'FZ ('FS b) = 'FS (Exponential (LTE ('S n)) 'FZ b)+  type Exponential (LTE ('S ('S n))) ('FS a) 'FZ = 'FZ+  type Exponential (LTE ('S ('S n))) ('FS a) ('FS b) = 'FS (Exponential (LTE ('S n)) a b)+  apply ZEQ ZEQ = ZEQ+  apply ZEQ (SLT a) = ZLT (case apply ZEQ a of { ZEQ -> ZEQ; ZLT n -> ZLT n })+  apply (SLT _) ZEQ = ZEQ+  apply (SLT a) (SLT b) = SLT (apply a b)+  tuple ZEQ ZEQ = case proof (ZEQ @n) of Proof -> ZLT (tuple ZEQ ZEQ)+  tuple ZEQ (SLT a) = case proof (src a) of Proof -> SLT (tuple ZEQ a)+  tuple (SLT _) ZEQ = ZEQ+  tuple (SLT a) (SLT b) = SLT (tuple a b)+  ZEQ ^^^ ZEQ = SLT (ZEQ ^^^ ZEQ)+  ZEQ ^^^ ZLT a = ZLT (initialize (tgt (ZEQ ^^^ a)))+  ZEQ ^^^ SLT _ = ZEQ+  ZLT a ^^^ ZEQ = SLT (a ^^^ ZEQ)+  ZLT a ^^^ ZLT b = ZLT (initialize (tgt (a ^^^ b)))+  ZLT a ^^^ SLT b = ZLT (initialize (tgt (a ^^^ b)))+  SLT a ^^^ ZEQ = SLT (a ^^^ ZEQ)+  SLT a ^^^ ZLT b = SLT (a ^^^ b)+  SLT a ^^^ SLT b = SLT (a ^^^ b)+

@@ -10,6 +10,8 @@ ----------------------------------------------------------------------------- module Data.Category.Fix where +import Data.Kind (Type)+ import Data.Category import Data.Category.Functor import Data.Category.Limit@@ -58,7 +60,7 @@   tuple (Fix a) (Fix b) = Fix (tuple a b)   Fix a ^^^ Fix b = Fix (a ^^^ b) -data Wrap (f :: * -> * -> *) = Wrap+data Wrap (f :: Type -> Type -> Type) = Wrap -- | The `Wrap` functor wraps `Fix` around @f (Fix f)@. instance Category (f (Fix f)) => Functor (Wrap (Fix f)) where   type Dom (Wrap (Fix f)) = f (Fix f)@@ -66,7 +68,7 @@   type Wrap (Fix f) :% a = a   Wrap % f = Fix f -data Unwrap (f :: * -> * -> *) = Unwrap+data Unwrap (f :: Type -> Type -> Type) = Unwrap -- | The `Unwrap` functor unwraps @Fix f@ to @f (Fix f)@. instance Category (f (Fix f)) => Functor (Unwrap (Fix f)) where   type Dom (Unwrap (Fix f)) = Fix f

@@ -34,7 +34,6 @@   , Id(..)   , (:.:)(..)   , Const(..), ConstF-  , Opposite(..)   , OpOp(..)   , OpOpInv(..)   , Any(..)@@ -52,12 +51,14 @@   , Hom(..)   , (:*-:), pattern HomX_   , (:-*:), pattern Hom_X-  , HomF, pattern HomF-  , Star, pattern Star-  , Costar, pattern Costar +  -- *** Profunctors+  , ProfunctorOf+ ) where +import Data.Kind (Type)+ import Data.Category import Data.Category.Product @@ -70,12 +71,12 @@ class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where    -- | The domain, or source category, of the functor.-  type Dom ftag :: * -> * -> *+  type Dom ftag :: Type -> Type -> Type   -- | The codomain, or target category, of the functor.-  type Cod ftag :: * -> * -> *+  type Cod ftag :: Type -> Type -> Type    -- | @:%@ maps objects.-  type ftag :% a :: *+  type ftag :% a :: Type    -- | @%@ maps arrows.   (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)@@ -84,7 +85,7 @@   -- | Functors are arrows in the category Cat.-data Cat :: (* -> * -> *) -> (* -> * -> *) -> * where+data Cat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type where   CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (Dom ftag) (Cod ftag)  @@ -98,7 +99,7 @@   -data Id (k :: * -> * -> *) = Id+data Id (k :: Type -> Type -> Type) = Id  -- | The identity functor on k instance Category k => Functor (Id k) where@@ -122,7 +123,7 @@   -data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where+data Const (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) x where   Const :: Obj c2 x -> Const c1 c2 x  -- | The constant functor.@@ -137,19 +138,8 @@ type ConstF f = Const (Dom f) (Cod f)  -data Opposite f where-  Opposite :: Functor f => f -> Opposite f --- | The dual of a functor-instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f) where-  type Dom (Opposite f) = Op (Dom f)-  type Cod (Opposite f) = Op (Cod f)-  type Opposite f :% a = f :% a--  Opposite f % Op a = Op (f % a)---data OpOp (k :: * -> * -> *) = OpOp+data OpOp (k :: Type -> Type -> Type) = OpOp  -- | The @Op (Op x) = x@ functor. instance Category k => Functor (OpOp k) where@@ -160,7 +150,7 @@   OpOp % Op (Op f) = f  -data OpOpInv (k :: * -> * -> *) = OpOpInv+data OpOpInv (k :: Type -> Type -> Type) = OpOpInv  -- | The @x = Op (Op x)@ functor. instance Category k => Functor (OpOpInv k) where@@ -175,7 +165,7 @@ newtype Any f = Any f deriving Functor  -data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1+data Proj1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Proj1  -- | 'Proj1' is a bifunctor that projects out the first component of a product. instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where@@ -186,7 +176,7 @@   Proj1 % (f1 :**: _) = f1  -data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj2+data Proj2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Proj2  -- | 'Proj2' is a bifunctor that projects out the second component of a product. instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where@@ -208,7 +198,7 @@   (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)  -data DiagProd (k :: * -> * -> *) = DiagProd+data DiagProd (k :: Type -> Type -> Type) = DiagProd  -- | 'DiagProd' is the diagonal functor for products. instance Category k => Functor (DiagProd k) where@@ -220,18 +210,11 @@   type Tuple1 c1 c2 a = (Const c2 c1 a :***: Id c2) :.: DiagProd c2- -- | 'Tuple1' tuples with a fixed object on the left. pattern Tuple1 :: (Category c1, Category c2) => Obj c1 a -> Tuple1 c1 c2 a pattern Tuple1 a = (Const a :***: Id) :.: DiagProd --- type Tuple2 c1 c2 a = (Id c1 :***: Const c1 c2 a) :.: DiagProd c1------ -- | 'Tuple2' tuples with a fixed object on the right.--- tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a--- tuple2 a = (Id :***: Const a) :.: DiagProd--type Swap (c1 :: * -> * -> *) (c2 :: * -> * -> *) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2)+type Swap (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2) -- | 'swap' swaps the 2 categories of the product of categories. pattern Swap :: (Category c1, Category c2) => Swap c1 c2 pattern Swap = (Proj2 :***: Proj1) :.: DiagProd@@ -243,7 +226,7 @@   -data Hom (k :: * -> * -> *) = Hom+data Hom (k :: Type -> Type -> Type) = Hom  -- | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument. instance Category k => Functor (Hom k) where@@ -265,14 +248,4 @@ pattern Hom_X x = Hom :.: Tuple2 x  -type HomF f g = Hom (Cod f) :.: (Opposite f :***: g)-pattern HomF :: (Functor f, Functor g, Cod f ~ Cod g) => f -> g -> HomF f g-pattern HomF f g = Hom :.: (Opposite f :***: g)--type Star f = HomF (Id (Cod f)) f-pattern Star :: Functor f => f -> Star f-pattern Star f = HomF Id f--type Costar f = HomF f (Id (Cod f))-pattern Costar :: Functor f => f -> Costar f-pattern Costar f = HomF f Id+type ProfunctorOf c d t = (FunctorOf (Op c :**: d) (->) t, Category c, Category d)

@@ -19,6 +19,8 @@ ----------------------------------------------------------------------------- module Data.Category.KanExtension where +import Data.Kind (Type)+ import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -30,7 +32,7 @@ -- | An instance of @HasRightKan p k@ says there are right Kan extensions for all functors with codomain @k@. class (Functor p, Category k) => HasRightKan p k where   -- | The right Kan extension of a functor @p@ for functors @f@ with codomain @k@.-  type RanFam p k (f :: *) :: *+  type RanFam p k (f :: Type) :: Type   -- | 'ran' gives the defining natural transformation of the right Kan extension of @f@ along @p@.   ran           :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k (RanFam p k f :.: p) f   -- | 'ranFactorizer' shows that this extension is universal.@@ -44,7 +46,7 @@ ranF' :: Nat (Dom p) k (RanFam p k f :.: p) f -> Obj (Nat (Cod p) k) (RanFam p k f) ranF' (Nat (r :.: _) _ _) = natId r -data RanFunctor (p :: *) (k :: * -> * -> *) = RanFunctor p+newtype RanFunctor (p :: Type) (k :: Type -> Type -> Type) = RanFunctor p instance HasRightKan p k => Functor (RanFunctor p k) where   type Dom (RanFunctor p k) = Nat (Dom p) k   type Cod (RanFunctor p k) = Nat (Cod p) k@@ -60,7 +62,7 @@ -- | An instance of @HasLeftKan p k@ says there are left Kan extensions for all functors with codomain @k@. class (Functor p, Category k) => HasLeftKan p k where   -- | The left Kan extension of a functor @p@ for functors @f@ with codomain @k@.-  type LanFam (p :: *) (k :: * -> * -> *) (f :: *) :: *+  type LanFam (p :: Type) (k :: Type -> Type -> Type) (f :: Type) :: Type   -- | 'lan' gives the defining natural transformation of the left Kan extension of @f@ along @p@.   lan           :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k f (LanFam p k f :.: p)   -- | 'lanFactorizer' shows that this extension is universal.@@ -74,7 +76,7 @@ lanF' :: Nat (Dom p) k f (LanFam p k f :.: p) -> Obj (Nat (Cod p) k) (LanFam p k f) lanF' (Nat _ (r :.: _) _) = natId r -data LanFunctor (p :: *) (k :: * -> * -> *) = LanFunctor p+newtype LanFunctor (p :: Type) (k :: Type -> Type -> Type) = LanFunctor p instance HasLeftKan p k => Functor (LanFunctor p k) where   type Dom (LanFunctor p k) = Nat (Dom p) k   type Cod (LanFunctor p k) = Nat (Cod p) k

@@ -4,6 +4,10 @@   GADTs,   PolyKinds,   DataKinds,+  LinearTypes,+  LambdaCase,+  EmptyCase,+  BlockArguments,   MultiParamTypeClasses,   RankNTypes,   ScopedTypeVariables,@@ -65,13 +69,20 @@   , ProductFunctor(..)   , (:*:)(..)   , prodAdj+  , type (&)(..)   , HasBinaryCoproducts(..)   , CoproductFunctor(..)   , (:+:)(..)   , coprodAdj+  , Either(..)  ) where +import Data.Kind (Type)+import GHC.Exts (FUN)+import GHC.Types (Multiplicity(One))+import Prelude (Either(..))+ import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -88,7 +99,7 @@ infixl 2 |||  -data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where+data Diag :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type where   Diag :: Diag j k  -- | The diagonal functor from (index-) category J to k.@@ -123,7 +134,7 @@ -- | An instance of @HasLimits j k@ says that @k@ has all limits of type @j@. class (Category j, Category k) => HasLimits j k where   -- | Limits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.-  type LimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *+  type LimitFam (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) (f :: Type) :: Type   -- | 'limit' returns the limiting cone for a functor @f@.   limit           :: Obj (Nat j k) f -> Cone j k f (LimitFam j k f)   -- | 'limitFactorizer' shows that the limiting cone is universal – i.e. any other cone of @f@ factors through it@@ -132,7 +143,7 @@  type Limit f = LimitFam (Dom f) (Cod f) f -data LimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = LimitFunctor+data LimitFunctor (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) = LimitFunctor -- | If every diagram of type @j@ has a limit in @k@ there exists a limit functor. --   It can be seen as a generalisation of @(***)@. instance HasLimits j k => Functor (LimitFunctor j k) where@@ -182,7 +193,7 @@ -- | An instance of @HasColimits j k@ says that @k@ has all colimits of type @j@. class (Category j, Category k) => HasColimits j k where   -- | Colimits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.-  type ColimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *+  type ColimitFam (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) (f :: Type) :: Type   -- | 'colimit' returns the limiting co-cone for a functor @f@.   colimit           :: Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)   -- | 'colimitFactorizer' shows that the limiting co-cone is universal – i.e. any other co-cone of @f@ factors through it@@ -191,7 +202,7 @@  type Colimit f = ColimitFam (Dom f) (Cod f) f -data ColimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = ColimitFunctor+data ColimitFunctor (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) = ColimitFunctor -- | If every diagram of type @j@ has a colimit in @k@ there exists a colimit functor. --   It can be seen as a generalisation of @(+++)@. instance HasColimits j k => Functor (ColimitFunctor j k) where@@ -248,10 +259,20 @@ instance HasTerminalObject (->) where   type TerminalObject (->) = () -  terminalObject = \x -> x+  terminalObject = obj    terminate _ _ = () +data Top where+  Top :: a %1 -> Top+-- | The terminal object in the category of linear types is `Top`.+instance HasTerminalObject (FUN 'One) where+  type TerminalObject (FUN 'One) = Top++  terminalObject = obj++  terminate _ = Top+ -- | @Unit@ is the terminal category. instance HasTerminalObject Cat where   type TerminalObject Cat = Unit@@ -311,14 +332,16 @@   data Zero+absurd :: FUN m Zero a+absurd = \case  -- | Any empty data type is an initial object in @Hask@.-instance HasInitialObject (->) where-  type InitialObject (->) = Zero+instance HasInitialObject (FUN m) where+  type InitialObject (FUN m) = Zero -  initialObject = \x -> x+  initialObject = obj -  initialize = initialize+  initialize _ = absurd  -- | The empty category is the initial object in @Cat@. instance HasInitialObject Cat where@@ -409,6 +432,25 @@   f &&& g = \x -> (f x, g x)   f *** g = \(x, y) -> (f x, g y) ++newtype x & y = AddConj (forall r. Either (x %1-> r) (y %1-> r) %1-> r)++-- | The product in the category of linear types is a & b, where you have access to a and b, but not both at the same time.+instance HasBinaryProducts (FUN 'One) where+  type BinaryProduct (FUN 'One) x y = x & y++  proj1 _ _ = \(AddConj f) -> f (Left obj)+  proj2 _ _ = \(AddConj f) -> f (Right obj)++  f &&& g = \x -> AddConj \case+    Left h -> h (f x)+    Right h -> h (g x)+  f *** g = \(AddConj h) -> AddConj \case+    Left l -> h (Left (\x -> l (f x)))+    Right r -> h (Right (\x -> r (g x)))+++ -- | The product of categories ':**:' is the binary product in 'Cat'. instance HasBinaryProducts Cat where   type BinaryProduct Cat c1 c2 = c1 :**: c2@@ -456,13 +498,13 @@   proj2 (DC (I2A a)) (DC (I2A b)) = DC (I2A (proj2 a b))    DC (I1A a) &&& DC (I1A b) = DC (I1A (a &&& b))-  DC (I1A a) &&& DC (I12 _ _ _ _) = DC (I1A a)-  DC (I12 _ _ _ _) &&& DC (I1A b) = DC (I1A b)+  DC (I1A a) &&& DC I12{} = DC (I1A a)+  DC I12{} &&& DC (I1A b) = DC (I1A b)   DC (I2A a) &&& DC (I2A b) = DC (I2A (a &&& b))   DC (I12 a b1 _ _) &&& DC (I12 _ b2 _ _) = DC (I12 a (b1 *** b2) (Const (\() -> ())) ())  -data ProductFunctor (k :: * -> * -> *) = ProductFunctor+data ProductFunctor (k :: Type -> Type -> Type) = ProductFunctor -- | Binary product as a bifunctor. instance HasBinaryProducts k => Functor (ProductFunctor k) where   type Dom (ProductFunctor k) = k :**: k@@ -534,6 +576,19 @@     colimitFactorizer (constPostcompOut (c `o` natId Inj2))  +instance HasBinaryCoproducts (FUN m) where+  type BinaryCoproduct (FUN m) a b = Either a b++  inj1 _ _ = Left+  inj2 _ _ = Right++  f ||| g = \case+    Left a -> f a+    Right b -> g b+  f +++ g = \case+    Left a -> Left (f a)+    Right b -> Right (g b)+ -- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'. instance HasBinaryCoproducts Cat where   type BinaryCoproduct Cat c1 c2 = c1 :++: c2@@ -581,13 +636,13 @@   inj2 (DC (I2A a)) (DC (I2A b)) = DC (I2A (inj2 a b))    DC (I1A a) ||| DC (I1A b) = DC (I1A (a ||| b))-  DC (I2A a) ||| DC (I12 _ _ _ _) = DC (I2A a)-  DC (I12 _ _ _ _) ||| DC (I2A b) = DC (I2A b)+  DC (I2A a) ||| DC I12{} = DC (I2A a)+  DC I12{} ||| DC (I2A b) = DC (I2A b)   DC (I2A a) ||| DC (I2A b) = DC (I2A (a ||| b))   DC (I12 a1 b _ _) ||| DC (I12 a2 _ _ _) = DC (I12 (a1 +++ a2) b (Const (\() -> ())) ())  -data CoproductFunctor (k :: * -> * -> *) = CoproductFunctor+data CoproductFunctor (k :: Type -> Type -> Type) = CoproductFunctor -- | Binary coproduct as a bifunctor. instance HasBinaryCoproducts k => Functor (CoproductFunctor k) where   type Dom (CoproductFunctor k) = k :**: k@@ -679,16 +734,16 @@   colimitFactorizer n = n ! terminalObject  -data ForAll f = ForAll (forall a. Obj (->) a -> f :% a)+newtype ForAll f = ForAll (forall a. Obj (->) a -> f :% a)  instance HasLimits (->) (->) where   type LimitFam (->) (->) f = ForAll f-  limit (Nat f _ _) = Nat (Const (\x -> x)) f (\a (ForAll g) -> g a)+  limit (Nat f _ _) = Nat (Const obj) f (\a (ForAll g) -> g a)   limitFactorizer n = \z -> ForAll (\a -> (n ! a) z)  data Exists f = forall a. Exists (Obj (->) a) (f :% a)  instance HasColimits (->) (->) where   type ColimitFam (->) (->) f = Exists f-  colimit (Nat f _ _) = Nat f (Const (\x -> x)) Exists+  colimit (Nat f _ _) = Nat f (Const obj) Exists   colimitFactorizer n = \(Exists a fa) -> (n ! a) fa

@@ -2,9 +2,12 @@     TypeOperators   , TypeFamilies   , GADTs+  , PolyKinds+  , DataKinds   , Rank2Types   , ViewPatterns   , TypeSynonymInstances+  , FlexibleContexts   , FlexibleInstances   , UndecidableInstances   , NoImplicitPrelude@@ -26,13 +29,17 @@ import Data.Category.Adjunction import Data.Category.Limit import Data.Category.Product+import Data.Category.KanExtension +import GHC.Exts (FUN)+import GHC.Types (Multiplicity(One)) + -- | A monoidal category is a category with some kind of tensor product. --   A tensor product is a bifunctor, with a unit object. class (Functor f, Dom f ~ (Cod f :**: Cod f)) => TensorProduct f where -  type Unit f :: *+  type Unit f :: Kind (Cod f)   unitObject :: f -> Obj (Cod f) (Unit f)    leftUnitor     :: Cod f ~ k => f -> Obj k a -> k (f :% (Unit f, a)) a@@ -96,11 +103,63 @@   associator    _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = compAssoc f g h   associatorInv _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = compAssocInv f g h +data LinearTensor = LinearTensor+instance Functor LinearTensor where+  type Dom LinearTensor = FUN 'One :**: FUN 'One+  type Cod LinearTensor = FUN 'One+  type LinearTensor :% (a, b) = (a, b) +  LinearTensor % (f :**: g) = \(a, b) -> (f a, g b)++instance TensorProduct LinearTensor where+  type Unit LinearTensor = ()+  unitObject _ = obj++  leftUnitor     _ _ = \((), a) -> a+  leftUnitorInv  _ _ = \a -> ((), a)+  rightUnitor    _ _ = \(a, ()) -> a+  rightUnitorInv _ _ = \a -> (a, ())+  associator    _ _ _ _ = \((a, b), c) -> (a, (b, c))+  associatorInv _ _ _ _ = \(a, (b, c)) -> ((a, b), c)++instance SymmetricTensorProduct LinearTensor where+  swap _ _ _ = \(a, b) -> (b, a)+++-- | Day convolution+data Day t = Day t+instance TensorProduct t => Functor (Day t) where+  type Dom (Day t) = Nat (Cod t) (->) :**: Nat (Cod t) (->)+  type Cod (Day t) = Nat (Cod t) (->)+  type Day t :% (f, g) = LanHaskF t (ProductFunctor (->) :.: (f :***: g))+  Day _ % (nf :**: ng) =+    Nat LanHaskF LanHaskF (\_ (LanHask x@(x1 :**: x2) tx fgx) -> LanHask x tx ((nf ! x1 *** ng ! x2) fgx))++instance TensorProduct t => TensorProduct (Day t) where+  type Unit (Day t) = Curry1 (Op (Cod t)) (Cod t) (Hom (Cod t)) :% Unit t+  unitObject (Day t) = Curry1 Hom % Op (unitObject t)+  leftUnitor (Day t) (NatId a) =+    Nat LanHaskF a (\_ (LanHask (_ :**: c2) tcz (uc1, ac2)) -> (a % (tcz . t % (uc1 :**: c2) . leftUnitorInv t c2)) ac2)+  leftUnitorInv (Day t) (NatId a) =+    Nat a LanHaskF (\z az -> LanHask (unitObject t :**: z) (leftUnitor t z) (unitObject t, az))+  rightUnitor (Day t) (NatId a) =+    Nat LanHaskF a (\_ (LanHask (c1 :**: _) tcz (ac1, uc2)) -> (a % (tcz . t % (c1 :**: uc2) . rightUnitorInv t c1)) ac1)+  rightUnitorInv (Day t) (NatId a) =+    Nat a LanHaskF (\z az -> LanHask (z :**: unitObject t) (rightUnitor t z) (az, unitObject t))+  associator (Day t) _ _ _ =+    Nat LanHaskF LanHaskF (\_ (LanHask (_e :**: d) eda (LanHask (b :**: c) bce (fb, gc), hd)) ->+      let cd = c :**: d; tcd = t % cd+      in LanHask (b :**: tcd) (eda . t % (bce :**: d) . associatorInv t b c d) (fb, LanHask cd tcd (gc, hd)))+  associatorInv (Day t) _ _ _ =+    Nat LanHaskF LanHaskF (\_ (LanHask (b :**: _c) bca (fb, LanHask (d :**: e) dec (gd, he))) ->+      let bd = b :**: d; tbd = t % bd+      in LanHask (tbd :**: e) (bca . t % (b :**: dec) . associator t b d e) (LanHask bd tbd (fb, gd), he))++ -- | @MonoidObject f a@ defines a monoid @a@ in a monoidal category with tensor product @f@. data MonoidObject f a = MonoidObject-  { unit     :: Cod f (Unit f)        a-  , multiply :: Cod f ((f :% (a, a))) a+  { unit     :: Cod f (Unit f)      a+  , multiply :: Cod f (f :% (a, a)) a   }  trivialMonoid :: TensorProduct f => f -> MonoidObject f (Unit f)

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, UndecidableInstances, NoImplicitPrelude #-}+{-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Peano@@ -10,6 +10,8 @@ ----------------------------------------------------------------------------- module Data.Category.NNO where +import Data.Kind (Type)+ import Data.Category.Functor import Data.Category.Limit import Data.Category.Unit@@ -18,24 +20,24 @@   class HasTerminalObject k => HasNaturalNumberObject k where-  -  type NaturalNumberObject k :: *-  ++  type NaturalNumberObject k :: Type+   zero :: k (TerminalObject k) (NaturalNumberObject k)   succ :: k (NaturalNumberObject k) (NaturalNumberObject k)-  +   primRec :: k (TerminalObject k) a -> k a a -> k (NaturalNumberObject k) a-  -  ++ data NatNum = Z | S NatNum  instance HasNaturalNumberObject (->) where-  +   type NaturalNumberObject (->) = NatNum-  +   zero = \() -> Z   succ = S-  +   primRec z _  Z    = z ()   primRec z s (S n) = s (primRec z s n) @@ -43,14 +45,14 @@ -- type Nat = Fix ((:++:) Unit)  -- instance HasNaturalNumberObject Cat where-  + --   type NaturalNumberObject Cat = CatW Nat-  + --   zero = CatA (Const (Fix (I1 Unit))) --   succ = CatA (Wrap :.: Inj2)-  + --   primRec (CatA z) (CatA s) = CatA (PrimRec z s)-  + -- data PrimRec z s = PrimRec z s -- instance (Functor z, Functor s, Dom z ~ Unit, Cod z ~ Dom s, Dom s ~ Cod s) => Functor (PrimRec z s) where --   type Dom (PrimRec z s) = Nat

@@ -16,6 +16,7 @@   , (!)   , o   , natId+  , pattern NatId   , srcF   , tgtF @@ -42,12 +43,22 @@   , EndoFunctorCompose   , Precompose, pattern Precompose   , Postcompose, pattern Postcompose+  , Curry1, pattern Curry1+  , Curry2, pattern Curry2   , Wrap(..)   , Apply(..)   , Tuple(..)+  , Opp(..), Opposite, pattern Opposite+  , HomF, pattern HomF+  , Star, pattern Star+  , Costar, pattern Costar+  , (:*%:), pattern HomXF+  , (:%*:), pattern HomFX  ) where +import Data.Kind (Type)+ import Data.Category import Data.Category.Functor import Data.Category.Product@@ -59,7 +70,7 @@  -- | Natural transformations are built up of components, -- one for each object @z@ in the domain category of @f@ and @g@.-data Nat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where+data Nat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where   Nat :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g)     => f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g @@ -80,11 +91,12 @@  -- | The identity natural transformation of a functor. natId :: Functor f => f -> Nat (Dom f) (Cod f) f f-natId f = Nat f f (\i -> f % i)+natId f = Nat f f (f %) -pattern NatId :: Functor f => f -> Nat (Dom f) (Cod f) f f-pattern NatId f <- Nat f _ _ where -  NatId f = Nat f f (\i -> f % i)+pattern NatId :: () => (Functor f, c ~ Dom f, d ~ Cod f) => f -> Nat c d f f+pattern NatId f <- Nat f _ _ where+  NatId f = Nat f f (f %)+{-# COMPLETE NatId #-}  srcF :: Nat c d f g -> f srcF (Nat f _ _) = f@@ -137,7 +149,7 @@ constPostcompOut (Nat f (Const x :.: _) n) = Nat f (Const x) n  -data FunctorCompose (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) = FunctorCompose+data FunctorCompose (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) (e :: Type -> Type -> Type) = FunctorCompose  -- | Composition of functors is a functor. instance (Category c, Category d, Category e) => Functor (FunctorCompose c d e) where@@ -157,6 +169,7 @@  type Profunctors c d = Nat (Op d :**: c) (->) + -- | @Precompose f e@ is the functor such that @Precompose f e :% g = g :.: f@, --   for functors @g@ that compose with @f@ and with codomain @e@. type Precompose f e = FunctorCompose (Dom f) (Cod f) e :.: Tuple2 (Nat (Cod f) e) (Nat (Dom f) (Cod f)) f@@ -166,10 +179,21 @@ -- | @Postcompose f c@ is the functor such that @Postcompose f c :% g = f :.: g@, --   for functors @g@ that compose with @f@ and with domain @c@. type Postcompose f c = FunctorCompose c (Dom f) (Cod f) :.: Tuple1 (Nat (Dom f) (Cod f)) (Nat c (Dom f)) f-pattern Postcompose :: (Category e, Functor f) => f -> Postcompose f e+pattern Postcompose :: (Category c, Functor f) => f -> Postcompose f c pattern Postcompose f = FunctorCompose :.: Tuple1 (NatId f)  +type Curry1 c1 c2 f = Postcompose f c2 :.: Tuple c1 c2+-- | Curry on the first "argument" of a functor from a product category.+pattern Curry1 :: (Functor f, Dom f ~ c1 :**: c2, Category c1, Category c2) => f -> Curry1 c1 c2 f+pattern Curry1 f = Postcompose f :.: Tuple++type Curry2 c1 c2 f = Postcompose f c1 :.: Curry1 c2 c1 (Swap c2 c1)+-- | Curry on the second "argument" of a functor from a product category.+pattern Curry2 :: (Functor f, Dom f ~ c1 :**: c2, Category c1, Category c2) => f -> Curry2 c1 c2 f+pattern Curry2 f = Postcompose f :.: Curry1 Swap++ data Wrap f h = Wrap f h  -- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@,@@ -182,7 +206,7 @@   Wrap f h % n = natId f `o` n `o` natId h  -data Apply (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Apply+data Apply (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Apply -- | 'Apply' is a bifunctor, @Apply :% (f, a)@ applies @f@ to @a@, i.e. @f :% a@. instance (Category c1, Category c2) => Functor (Apply c1 c2) where   type Dom (Apply c1 c2) = Nat c2 c1 :**: c2@@ -190,10 +214,53 @@   type Apply c1 c2 :% (f, a) = f :% a   Apply % (l :**: r) = l ! r -data Tuple (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Tuple+data Tuple (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Tuple -- | 'Tuple' converts an object @a@ to the functor 'Tuple1' @a@. instance (Category c1, Category c2) => Functor (Tuple c1 c2) where   type Dom (Tuple c1 c2) = c1   type Cod (Tuple c1 c2) = Nat c2 (c1 :**: c2)   type Tuple c1 c2 :% a = Tuple1 c1 c2 a-  Tuple % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) (\z -> f :**: z)+  Tuple % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) (f :**:)+++data Opp (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Opp+-- | Turning a functor into its dual is contravariantly functorial.+instance (Category c1, Category c2) => Functor (Opp c1 c2) where+  type Dom (Opp c1 c2) = Op (Nat c1 c2) :**: Op c1+  type Cod (Opp c1 c2) = Op c2+  type Opp c1 c2 :% (f, a) = f :% a+  Opp % (Op n :**: Op f) = Op (n ! f)++type Opposite f = Opp (Dom f) (Cod f) :.: Tuple1 (Op (Nat (Dom f) (Cod f))) (Op (Dom f)) f+-- | The dual of a functor+pattern Opposite :: Functor f => f -> Opposite f+pattern Opposite f = Opp :.: Tuple1 (Op (NatId f))+{-# COMPLETE Opposite #-}+++type HomF f g = Hom (Cod f) :.: (Opposite f :***: g)+pattern HomF :: (Functor f, Functor g, Cod f ~ Cod g) => f -> g -> HomF f g+pattern HomF f g = Hom :.: (Opposite f :***: g)+{-# COMPLETE HomF #-}++type Star f = HomF (Id (Cod f)) f+pattern Star :: Functor f => f -> Star f+pattern Star f = HomF Id f+{-# COMPLETE Star #-}++type Costar f = HomF f (Id (Cod f))+pattern Costar :: Functor f => f -> Costar f+pattern Costar f = HomF f Id+{-# COMPLETE Costar #-}++type x :*%: f = (x :*-: Cod f) :.: f+-- | The covariant functor Hom(X,F-)+pattern HomXF :: Functor f => Obj (Cod f) x -> f -> x :*%: f+pattern HomXF x f = HomX_ x :.: f+{-# COMPLETE HomXF #-}++type f :%*: x = (Cod f :-*: x) :.: Opposite f+-- | The contravariant functor Hom(F-,X)+pattern HomFX :: Functor f => f -> Obj (Cod f) x -> f :%*: x+pattern HomFX f x = Hom_X x :.: Opposite f+{-# COMPLETE HomFX #-}

@@ -0,0 +1,106 @@+{-# LANGUAGE GADTs, TypeFamilies, PatternSynonyms, ScopedTypeVariables, RankNTypes, TypeOperators #-}+module Data.Category.Preorder where++import Prelude hiding ((.), id, Functor)++import Data.Category+import Data.Category.Limit+import Data.Category.CartesianClosed+import Data.Category.Functor+import Data.Category.Adjunction+import Data.Category.Enriched+import Data.Category.Enriched.Functor+import Data.Category.Enriched.Limit hiding (HasEnds(..))++data Preorder a x y where+  (:<=:) :: a -> a -> Preorder a x y++pattern Obj :: a -> Preorder a x y+pattern Obj a <- a :<=: _ where+  Obj a = a :<=: a+{-# COMPLETE Obj #-} -- Note: only complete for identity arrows `Obj Preorder a`++unObj :: Obj (Preorder a) x -> a+unObj (Obj a) = a++instance Eq a => Category (Preorder a) where+  src (s :<=: _) = Obj s+  tgt (_ :<=: t) = Obj t+  (b :<=: c) . (a :<=: b') = if b == b' then a :<=: c else error "Invalid composition"++instance (Eq a, Bounded a) => HasInitialObject (Preorder a) where+  type InitialObject (Preorder a) = ()+  initialObject = Obj minBound+  initialize (Obj a) = minBound :<=: a++instance (Eq a, Bounded a) => HasTerminalObject (Preorder a) where+  type TerminalObject (Preorder a) = ()+  terminalObject = Obj maxBound+  terminate (Obj a) = a :<=: maxBound++instance Ord a => HasBinaryProducts (Preorder a) where+  type BinaryProduct (Preorder a) x y = ()+  proj1 (Obj a) (Obj b) = min a b :<=: a+  proj2 (Obj a) (Obj b) = min a b :<=: b+  (a :<=: x) &&& (_a :<=: y) = a :<=: min x y++instance Ord a => HasBinaryCoproducts (Preorder a) where+  type BinaryCoproduct (Preorder a) x y = ()+  inj1 (Obj a) (Obj b) = a :<=: max a b+  inj2 (Obj a) (Obj b) = b :<=: max a b+  (x :<=: a) ||| (y :<=: _a) = max x y :<=: a++-- | `ordExp a b` is the largest x such that min x a <= b+ordExp :: (Ord a, Bounded a) => a -> a -> a+ordExp a b = if a <= b then maxBound else b++instance (Ord a, Bounded a) => CartesianClosed (Preorder a) where+  type Exponential (Preorder a) x y = ()+  apply (Obj a) (Obj b) = min (ordExp a b) a :<=: b+  tuple (Obj a) (Obj b) = b :<=: ordExp a (min a b)+  (z1 :<=: z2) ^^^ (y2 :<=: y1) = ordExp y1 z1 :<=: ordExp y2 z2+++class Category k => EnumObjs k where+  enumObjs :: (forall a. Obj k a -> r) -> [r]++glb :: (Ord a, Bounded a) => [a] -> a+glb [] = maxBound+glb xs = minimum xs+++type End' t = ()+end+  :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a)+  => t -> Obj (Preorder a) (End' t)+end t = Obj $ glb (enumObjs (\a -> unObj (getSelf (t %% (EOp a :<>: a)))))++endCounit+  :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a)+  => t -> Obj k b -> Preorder a (End' t) (t :%% (b, b))+endCounit t a = unObj (end t) :<=: unObj (getSelf (t %% (EOp a :<>: a)))++endFactorizer+  :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a)+  => t -> Obj (Preorder a) x -> (forall b. Obj k b -> Preorder a x (t :%% (b, b))) -> Preorder a x (End' t)+endFactorizer _ (Obj x) f = x :<=: glb (enumObjs (\b -> case f b of _ :<=: tbb -> tbb))+++data Floor = Floor+instance Functor Floor where+  type Dom Floor = Preorder Double+  type Cod Floor = Preorder Integer+  type Floor :% a = ()+  Floor % (a :<=: b) = floor a :<=: floor b++data FromInteger = FromInteger+instance Functor FromInteger where+  type Dom FromInteger = Preorder Integer+  type Cod FromInteger = Preorder Double+  type FromInteger :% a = ()+  FromInteger % (a :<=: b) = fromInteger a :<=: fromInteger b++floorGaloisConnection :: Adjunction (Preorder Double) (Preorder Integer) FromInteger Floor+floorGaloisConnection = mkAdjunction FromInteger Floor+  (\(Obj a) (_fromIntegerA :<=: b) -> a :<=: floor b)+  (\(Obj b) (a :<=: _floorB) -> fromInteger a :<=: b)

@@ -10,16 +10,18 @@ ----------------------------------------------------------------------------- module Data.Category.Product where +import Data.Kind (Type)+ import Data.Category  -data (:**:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where+data (:**:) :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where   (:**:) :: c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)  -- | The product category of categories @c1@ and @c2@. instance (Category c1, Category c2) => Category (c1 :**: c2) where-  +   src (a1 :**: a2)            = src a1 :**: src a2   tgt (a1 :**: a2)            = tgt a1 :**: tgt a2-  +   (a1 :**: a2) . (b1 :**: b2) = (a1 . b1) :**: (a2 . b2)

@@ -42,7 +42,7 @@   , universalElement   = x   } -type InitialUniversal x u a = Representable ((x :*-: Cod u) :.: u) a+type InitialUniversal x u a = Representable (x :*%: u) a -- | An initial universal property, a universal morphism from x to u. initialUniversal :: Functor u                  => u@@ -50,14 +50,14 @@                  -> 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+initialUniversal u ob mor factorizer = Representable+  { representedFunctor = HomXF (src mor) u+  , representingObject = ob   , represent          = factorizer   , universalElement   = mor   } -type TerminalUniversal x u a = Representable ((Cod u :-*: x) :.: Opposite u) a+type TerminalUniversal x u a = Representable (u :%*: x) a -- | A terminal universal property, a universal morphism from u to x. terminalUniversal :: Functor u                   => u@@ -65,9 +65,9 @@                   -> 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+terminalUniversal u ob mor factorizer = Representable+  { representedFunctor = HomFX u (tgt mor)+  , representingObject = Op ob   , represent          = \(Op y) f -> Op (factorizer y f)   , universalElement   = mor   }

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, TypeOperators, UndecidableInstances, NoImplicitPrelude #-}+{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, TypeOperators, UndecidableInstances, LambdaCase, FlexibleContexts, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Simplex@@ -11,26 +11,29 @@ -- The (augmented) simplex category. ----------------------------------------------------------------------------- module Data.Category.Simplex (-  +   -- * Simplex Category     Simplex(..)   , Z, S   , suc-  +   -- * Functor   , Forget(..)   , Fin(..)   , Add(..)-  +   -- * The universal monoid   , universalMonoid   , Replicate(..)-        + ) where-  ++import Data.Kind (Type)+ import Data.Category import Data.Category.Product import Data.Category.Functor+import Data.Category.NaturalTransformation import Data.Category.Monoidal import Data.Category.Limit @@ -48,7 +51,7 @@ --      XY----+ --         x -> -data Simplex :: * -> * -> * where+data Simplex :: Type -> Type -> Type where   Z ::                    Simplex    Z     Z   Y :: Simplex x    y  -> Simplex    x  (S y)   X :: Simplex x (S y) -> Simplex (S x) (S y)@@ -63,11 +66,11 @@   src Z = Z   src (Y f) = src f   src (X f) = suc (src f)-  +   tgt Z = Z   tgt (Y f) = suc (tgt f)   tgt (X f) = tgt f-  +   Z   .   f = f   f   .   Z = f   Y f .   g = Y (f . g)@@ -78,9 +81,9 @@ -- | The ordinal @0@ is the initial object of the simplex category. instance HasInitialObject Simplex where   type InitialObject Simplex = Z-  +   initialObject = Z-  +   initialize Z = Z   initialize (X (Y f)) = Y (initialize f) @@ -94,7 +97,7 @@   terminate (X (Y f)) = X (terminate f)  -data Fin :: * -> * where+data Fin :: Type -> Type where   Fz ::          Fin (S n)   Fs :: Fin n -> Fin (S n) @@ -104,9 +107,9 @@   type Dom Forget = Simplex   type Cod Forget = (->)   type Forget :% n = Fin n-  Forget % Z   = \x -> x-  Forget % Y f = \x -> Fs ((Forget % f) x)-  Forget % X f = \x -> case x of+  Forget % Z   = obj+  Forget % Y f = Fs . (Forget % f)+  Forget % X f = \case     Fz -> Fz     Fs n -> (Forget % f) n @@ -126,7 +129,7 @@ instance TensorProduct Add where   type Unit Add = Z   unitObject Add = Z-  +   leftUnitor     Add       a   = a   leftUnitorInv  Add       a   = a   rightUnitor    Add       Z   = Z@@ -160,3 +163,11 @@       n' = Replicate f m % X n       a = tgt (unit m)       b = src (Replicate f m % n)++data Cobar f d = Cobar (Monad f) (Obj (Dom f) d)+-- | The cobar construction+instance Category (Dom f) => Functor (Cobar f d) where+  type Dom (Cobar f d) = Simplex+  type Cod (Cobar f d) = Dom f+  type Cobar f d :% s = (Replicate (EndoFunctorCompose (Dom f)) f :% s) :% d+  Cobar f d % s = (Replicate FunctorCompose f % s) ! d

@@ -10,6 +10,8 @@ ----------------------------------------------------------------------------- module Data.Category.Void where +import Data.Kind (Type)+ import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -34,7 +36,7 @@ voidNat f g = Nat f g magic  -data Magic (k :: * -> * -> *) = Magic+data Magic (k :: Type -> Type -> Type) = Magic -- | Since there is nothing to map in `Void`, there's a functor from it to any other category. instance Category k => Functor (Magic k) where   type Dom (Magic k) = Void

@@ -0,0 +1,142 @@+{-# LANGUAGE TypeOperators, RankNTypes, GADTs, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, NoImplicitPrelude, FlexibleContexts #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.WeightedLimit+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.WeightedLimit where++import Data.Kind (Type)++import Data.Category+import Data.Category.Functor+import Data.Category.Product+import Data.Category.NaturalTransformation+import qualified Data.Category.Limit as L+++type WeightedCone w d e = forall a. Obj (Dom w) a -> w :% a -> Cod d e (d :% a)++-- | @w@-weighted limits in the category @k@.+class (Functor w, Cod w ~ (->), Category k) => HasWLimits k w where+  type WeightedLimit k w d :: Type+  limitObj :: FunctorOf (Dom w) k d => w -> d -> Obj k (WLimit w d)+  limit :: FunctorOf (Dom w) k d => w -> d -> WeightedCone w d (WLimit w d)+  limitFactorizer :: FunctorOf (Dom w) k d => w -> d -> Obj k e -> WeightedCone w d e -> k e (WLimit w d)++type WLimit w d = WeightedLimit (Cod d) w d++data LimitFunctor (k :: Type -> Type -> Type) w = LimitFunctor w+instance HasWLimits k w => Functor (LimitFunctor k w) where+  type Dom (LimitFunctor k w) = Nat (Dom w) k+  type Cod (LimitFunctor k w) = k+  type LimitFunctor k w :% d = WeightedLimit k w d++  LimitFunctor w % Nat d d' n = limitFactorizer w d' (limitObj w d) (\a wa -> n a . limit w d a wa)+++-- | Regular limits as weigthed limits, weighted by the constant functor to '()'.+instance L.HasLimits j k => HasWLimits k (Const j (->) ()) where+  type WeightedLimit k (Const j (->) ()) d = L.Limit d+  limitObj Const{} d = L.coneVertex (L.limit (natId d))+  limit Const{} d a () = L.limit (natId d) ! a+  limitFactorizer Const{} d e f = L.limitFactorizer (Nat (Const e) d (`f` ()))+++class Category v => HasEnds v where+  type End (v :: Type -> Type -> Type) t :: Type+  end :: FunctorOf (Op k :**: k) v t => t -> Obj v (End v t)+  endCounit :: FunctorOf (Op k :**: k) v t => t -> Obj k a -> v (End v t) (t :% (a, a))+  endFactorizer :: FunctorOf (Op k :**: k) v t => t -> (forall a. Obj k a -> v x (t :% (a, a))) -> v x (End v t)++-- | Ends as Hom-weighted limits+instance HasEnds k => HasWLimits k (Hom k) where+  type WeightedLimit k (Hom k) d = End k d+  limitObj Hom d = end d+  limit Hom d (Op a :**: _) ab = d % (Op a :**: ab) . endCounit d a+  limitFactorizer Hom d _ f = endFactorizer d (\a -> f (Op a :**: a) a)++data EndFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type) = EndFunctor+instance (HasEnds v, Category k) => Functor (EndFunctor k v) where+  type Dom (EndFunctor k v) = Nat (Op k :**: k) v+  type Cod (EndFunctor k v) = v+  type EndFunctor k v :% t = End v t++  EndFunctor % Nat f g n = endFactorizer g (\a -> n (Op a :**: a) . endCounit f a)++newtype HaskEnd t = HaskEnd { getHaskEnd :: forall k a. FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> t :% (a, a) }+instance HasEnds (->) where+  type End (->) t = HaskEnd t+  end _ e = e+  endCounit t a (HaskEnd f) = f t a+  endFactorizer _ e x = HaskEnd (\_ a -> e a x)+++type WeightedCocone w d e = forall a. Obj (Dom w) a -> w :% a -> Cod d (d :% a) e++-- | @w@-weighted colimits in the category @k@.+class (Functor w, Cod w ~ (->), Category k) => HasWColimits k w where+  type WeightedColimit k w d :: Type+  colimitObj :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k (WColimit w d)+  colimit :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> WeightedCocone w d (WColimit w d)+  colimitFactorizer :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k e -> WeightedCocone w d e -> k (WColimit w d) e++type WColimit w d = WeightedColimit (Cod d) w d++data ColimitFunctor (k :: Type -> Type -> Type) w = ColimitFunctor w+instance (Functor w, Category k, HasWColimits k (w :.: OpOp (Dom w))) => Functor (ColimitFunctor k w) where+  type Dom (ColimitFunctor k w) = Nat (Op (Dom w)) k+  type Cod (ColimitFunctor k w) = k+  type ColimitFunctor k w :% d = WeightedColimit k (w :.: OpOp (Dom w)) d++  ColimitFunctor w % Nat d d' n = colimitFactorizer (w :.: OpOp) d (colimitObj (w :.: OpOp) d') (\(Op a) wa -> colimit (w :.: OpOp) d' (Op a) wa . n a)+++-- | Regular colimits as weigthed colimits, weighted by the constant functor to '()'.+instance L.HasColimits j k => HasWColimits k (Const (Op j) (->) ()) where+  type WeightedColimit k (Const (Op j) (->) ()) d = L.Colimit d+  colimitObj (Const _) d = L.coconeVertex (L.colimit (natId d))+  colimit (Const _) d (Op a) () = L.colimit (natId d) ! a+  colimitFactorizer (Const _) d e f = L.colimitFactorizer (Nat d (Const e) (\z -> f (Op z) ()))+++class Category v => HasCoends v where+  type Coend (v :: Type -> Type -> Type) t :: Type+  coend :: FunctorOf (Op k :**: k) v t => t -> Obj v (Coend v t)+  coendCounit :: FunctorOf (Op k :**: k) v t => t -> Obj k a -> v (t :% (a, a)) (Coend v t)+  coendFactorizer :: FunctorOf (Op k :**: k) v t => t -> (forall a. Obj k a -> v (t :% (a, a)) x) -> v (Coend v t) x++data OpHom (k :: Type -> Type -> Type) = OpHom+-- | The Hom-functor but with opposite domain.+instance Category k => Functor (OpHom k) where+  type Dom (OpHom k) = Op (Op k :**: k)+  type Cod (OpHom k) = (->)+  type OpHom k :% (a1, a2) = k a2 a1+  OpHom % Op (Op f1 :**: f2) = \g -> f1 . g . f2++-- | Coends as OpHom-weighted colimits+instance HasCoends k => HasWColimits k (OpHom k) where+  type WeightedColimit k (OpHom k) d = Coend k d+  colimitObj OpHom d = coend d+  colimit OpHom d (Op (Op a :**: _)) ab = coendCounit d a . d % (Op a :**: ab)+  colimitFactorizer OpHom d _ f = coendFactorizer d (\a -> f (Op (Op a :**: a)) a)++data CoendFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type) = CoendFunctor+instance (HasCoends v, Category k) => Functor (CoendFunctor k v) where+  type Dom (CoendFunctor k v) = Nat (Op k :**: k) v+  type Cod (CoendFunctor k v) = v+  type CoendFunctor k v :% t = Coend v t++  CoendFunctor % Nat f g n = coendFactorizer f (\a -> coendCounit g a . n (Op a :**: a))++data HaskCoend t where+  HaskCoend :: FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> t :% (a, a) -> HaskCoend t+instance HasCoends (->) where+  type Coend (->) t = HaskCoend t+  coend _ e = e+  coendCounit t a taa = HaskCoend t a taa+  coendFactorizer _ f (HaskCoend _ a taa) = f a taa

@@ -10,21 +10,20 @@ ----------------------------------------------------------------------------- module Data.Category.Yoneda where +import Data.Kind (Type)+ import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation import Data.Category.Adjunction -type YonedaEmbedding k =-  Postcompose (Hom k) (Op k) :.:-  (Postcompose (Swap k (Op k)) (Op k) :.: Tuple k (Op k))-+type YonedaEmbedding k = Curry2 (Op k) k (Hom k) -- | The Yoneda embedding functor, @C -> Set^(C^op)@. pattern YonedaEmbedding :: Category k => YonedaEmbedding k-pattern YonedaEmbedding = Postcompose Hom :.: (Postcompose Swap :.: Tuple)+pattern YonedaEmbedding = Curry2 Hom  -data Yoneda (k :: * -> * -> *) f = Yoneda+data Yoneda (k :: Type -> Type -> Type) f = Yoneda -- | 'Yoneda' converts a functor @f@ into a natural transformation from the hom functor to f. instance (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => Functor (Yoneda k f) where   type Dom (Yoneda k f) = Op k@@ -40,8 +39,9 @@ toYoneda   :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) f (Yoneda k f) toYoneda   f = Nat f Yoneda (\(Op a) fa -> Nat (Hom_X a) f (\_ h -> (f % Op h) fa)) + haskUnit :: Obj (->) ()-haskUnit () = ()+haskUnit = obj  data M1 = M1 instance Functor M1 where

@@ -1,5 +1,5 @@ name:                data-category-version:             0.10+version:             0.11 synopsis:            Category theory  description:         Data-category is a collection of categories, and some categorical constructions on them.@@ -38,19 +38,29 @@     Data.Category.RepresentableFunctor,     Data.Category.Adjunction,     Data.Category.Limit,+    Data.Category.WeightedLimit,     Data.Category.KanExtension,     Data.Category.Monoidal,     Data.Category.CartesianClosed,-    Data.Category.Enriched,     Data.Category.Yoneda,     Data.Category.Boolean,+    Data.Category.Fin,     Data.Category.Fix,     Data.Category.Kleisli,     Data.Category.Dialg,     Data.Category.NNO,     Data.Category.Simplex,     Data.Category.Cube,-    Data.Category.Comma+    Data.Category.Comma,+    Data.Category.Preorder,+    Data.Category.Enriched,+    Data.Category.Enriched.Functor,+    Data.Category.Enriched.Limit,+    Data.Category.Enriched.Yoneda,+    Data.Category.Enriched.Poset3+  build-depends:+    base >=4.15 && <5,+    ghc-prim    default-language:    Haskell2010