packages feed

data-category 0.5.1.1 → 0.6.0

raw patch · 11 files changed

+129/−136 lines, 11 files

Files

Data/Category/Adjunction.hs view
@@ -31,6 +31,8 @@   , adjunctionTerminalProp      -- * Examples+  , precomposeAdj+  , postcomposeAdj   , contAdj    ) where@@ -90,8 +92,8 @@  composeAdj :: Adjunction d e f g -> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g') composeAdj (Adjunction f g u c) (Adjunction f' g' u' c') = Adjunction (f' :.: f) (g :.: g') -  (compAssoc (g :.: g') f' f . Precompose f % (compAssocInv g g' f' . Postcompose g % u' . idPrecompInv g) . u)-  (c' . Precompose g' % (idPrecomp f' . Postcompose f' % c . compAssoc f' f g) . compAssocInv (f' :.: f) g g')+  (compAssoc (g :.: g') f' f . precompose f % (compAssocInv g g' f' . postcompose g % u' . idPrecompInv g) . u)+  (c' . precompose g' % (idPrecomp f' . postcompose f' % c . compAssoc f' f g) . compAssocInv (f' :.: f) g g')   data AdjArrow c d where@@ -109,15 +111,15 @@  precomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e) precomposeAdj (Adjunction f g un coun) = mkAdjunction -  (Precompose g)-  (Precompose f)+  (precompose g)+  (precompose f)   (\nh@(Nat h _ _) -> compAssocInv h g f . (nh `o` un) . idPrecompInv h)   (\nh@(Nat h _ _) -> idPrecomp h . (nh `o` coun) . compAssoc h f g)  postcomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat e c) (Nat e d) (Postcompose f e) (Postcompose g e) postcomposeAdj (Adjunction f g un coun) = mkAdjunction -  (Postcompose f)-  (Postcompose g)+  (postcompose f)+  (postcompose g)   (\nh@(Nat h _ _) -> compAssoc g f h . (un `o` nh) . idPostcompInv h)   (\nh@(Nat h _ _) -> idPostcomp h . (coun `o` nh) . compAssocInv f g h)
Data/Category/CartesianClosed.hs view
@@ -48,29 +48,21 @@   -data Apply (y :: * -> * -> *) (z :: * -> * -> *) = Apply+data Apply (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Apply -- | 'Apply' is a bifunctor, @Apply :% (f, a)@ applies @f@ to @a@, i.e. @f :% a@.-instance (Category y, Category z) => Functor (Apply y z) where-  type Dom (Apply y z) = Nat y z :**: y-  type Cod (Apply y z) = z-  type Apply y z :% (f, a) = f :% a+instance (Category c1, Category c2) => Functor (Apply c1 c2) where+  type Dom (Apply c1 c2) = Nat c2 c1 :**: c2+  type Cod (Apply c1 c2) = c1+  type Apply c1 c2 :% (f, a) = f :% a   Apply % (l :**: r) = l ! r -data ToTuple1 (y :: * -> * -> *) (z :: * -> * -> *) = ToTuple1--- | 'ToTuple1' converts an object @a@ to the functor 'Tuple1' @a@.-instance (Category y, Category z) => Functor (ToTuple1 y z) where-  type Dom (ToTuple1 y z) = z-  type Cod (ToTuple1 y z) = Nat y (z :**: y)-  type ToTuple1 y z :% a = Tuple1 z y a-  ToTuple1 % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) (\z -> f :**: z)--data ToTuple2 (y :: * -> * -> *) (z :: * -> * -> *) = ToTuple2--- | 'ToTuple2' converts an object @a@ to the functor 'Tuple2' @a@.-instance (Category y, Category z) => Functor (ToTuple2 y z) where-  type Dom (ToTuple2 y z) = y-  type Cod (ToTuple2 y z) = Nat z (z :**: y)-  type ToTuple2 y z :% a = Tuple2 z y a-  ToTuple2 % f = Nat (Tuple2 (src f)) (Tuple2 (tgt f)) (\y -> y :**: f)+data Tuple (c1 :: * -> * -> *) (c2 :: * -> * -> *) = 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)   -- | Exponentials in @Cat@ are the functor categories.@@ -78,7 +70,7 @@   type Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)      apply CatA{} CatA{}   = CatA Apply-  tuple CatA{} CatA{}   = CatA ToTuple1+  tuple CatA{} CatA{}   = CatA Tuple   (CatA f) ^^^ (CatA h) = CatA (Wrap f h)  @@ -88,7 +80,7 @@          -> Adjunction k k               (ProductFunctor k :.: Tuple2 k k y)               (ExpFunctor k :.: Tuple1 (Op k) k y)-curryAdj y = mkAdjunction (ProductFunctor :.: Tuple2 y) (ExpFunctor :.: Tuple1 (Op y)) (tuple y) (apply y)+curryAdj y = mkAdjunction (ProductFunctor :.: tuple2 y) (ExpFunctor :.: Tuple1 (Op y)) (tuple y) (apply y)  -- | From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions, --   generalized to any cartesian closed category.
Data/Category/Fix.hs view
@@ -13,6 +13,7 @@ import Data.Category import Data.Category.Functor import Data.Category.Limit+import Data.Category.CartesianClosed  import Data.Category.Unit import Data.Category.Coproduct@@ -52,6 +53,13 @@   inj2 (Fix a) (Fix b) = Fix (inj2 a b)   Fix a ||| Fix b = Fix (a ||| b) +-- | @Fix f@ inherits its exponentials from @f (Fix f)@.+instance CartesianClosed (f (Fix f)) => CartesianClosed (Fix f) where+  type Exponential (Fix f) a b = Exponential (f (Fix f)) a b+  apply (Fix a) (Fix b) = Fix (apply a b)+  tuple (Fix a) (Fix b) = Fix (tuple a b)+  Fix a ^^^ Fix b = Fix (a ^^^ b)+   data Wrap (f :: (* -> * -> *) -> * -> * -> *) = Wrap -- | The `Wrap` functor wraps `Fix` around @f (Fix f)@. instance Category (f (Fix f)) => Functor (Wrap f) where
Data/Category/Functor.hs view
@@ -31,7 +31,8 @@   , (:***:)(..)   , DiagProd(..)   , Tuple1(..)-  , Tuple2(..)+  , Swap, swap+  , Tuple2, tuple2    -- *** Hom functors   , Hom(..)@@ -110,7 +111,7 @@   data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where-  Const :: Category c2 => Obj c2 x -> Const c1 c2 x+  Const :: Obj c2 x -> Const c1 c2 x  -- | The constant functor. instance (Category c1, Category c2) => Functor (Const c1 c2 x) where@@ -212,18 +213,18 @@      Tuple1 a % f = a :**: f --data Tuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple2 (Obj c2 a)+type Swap (c1 :: * -> * -> *) (c2 :: * -> * -> *) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2)+-- | 'swap' swaps the 2 categories of the product of categories.+swap :: (Category c1, Category c2) => Swap c1 c2+swap = (Proj2 :***: Proj1) :.: DiagProd +type Tuple2 c1 c2 a = Swap c2 c1 :.: Tuple1 c2 c1 a -- | 'Tuple2' tuples with a fixed object on the right.-instance (Category c1, Category c2) => Functor (Tuple2 c1 c2 a2) where-  type Dom (Tuple2 c1 c2 a2) = c1-  type Cod (Tuple2 c1 c2 a2) = c1 :**: c2-  type Tuple2 c1 c2 a2 :% a1 = (a1, a2)-  -  Tuple2 a % f = f :**: a+tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a+tuple2 a = swap :.: Tuple1 a  + data Hom (k :: * -> * -> *) = Hom  -- | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument.@@ -243,4 +244,4 @@ type k :-*: x = Hom k :.: Tuple2 (Op k) k x -- | The contravariant functor Hom(--,X) hom_X :: Category k => Obj k x -> k :-*: x-hom_X x = Hom :.: Tuple2 x+hom_X x = Hom :.: tuple2 x
Data/Category/Limit.hs view
@@ -56,9 +56,11 @@   , HasBinaryProducts(..)   , ProductFunctor(..)   , (:*:)(..)+  , prodAdj   , HasBinaryCoproducts(..)   , CoproductFunctor(..)   , (:+:)(..)+  , coprodAdj    ) where @@ -418,6 +420,10 @@    ProductFunctor % (a1 :**: a2) = a1 *** a2 +-- | A specialisation of the limit adjunction to products.+prodAdj :: HasBinaryProducts k => Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)+prodAdj = mkAdjunction DiagProd ProductFunctor (\x -> x &&& x) (\(l :**: r) -> proj1 l r :**: proj2 l r)+ data p :*: q where   (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q -- | The product of two functors, passing the same object to both functors and taking the product of the results.@@ -438,8 +444,8 @@   Nat a f af &&& Nat _ g ag = Nat a (f :*: g) (\z -> af z &&& ag z)   Nat f1 f2 f *** Nat g1 g2 g = Nat (f1 :*: g1) (f2 :*: g2) (\z -> f z *** g z)   -   + class Category k => HasBinaryCoproducts k where   type BinaryCoproduct (k :: * -> * -> *) x y :: * @@ -538,6 +544,10 @@   type CoproductFunctor k :% (a, b) = BinaryCoproduct k a b    CoproductFunctor % (a1 :**: a2) = a1 +++ a2++-- | A specialisation of the colimit adjunction to coproducts.+coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)+coprodAdj = mkAdjunction CoproductFunctor DiagProd (\(l :**: r) -> inj1 l r :**: inj2 l r) (\x -> x ||| x)  data p :+: q where   (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q
Data/Category/Monoidal.hs view
@@ -1,4 +1,13 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ViewPatterns, NoImplicitPrelude #-}+{-# LANGUAGE +    TypeOperators+  , TypeFamilies+  , GADTs+  , Rank2Types+  , ViewPatterns+  , TypeSynonymInstances+  , FlexibleInstances+  , NoImplicitPrelude +  #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Monoidal@@ -65,9 +74,9 @@   associatorInv _ a b c = (inj1 (a +++ b) c . inj1 a b) ||| (inj2 a b +++ c)    -- | Functor composition makes the category of endofunctors monoidal, with the identity functor as unit.-instance Category k => TensorProduct (FunctorCompose k) where+instance Category k => TensorProduct (EndoFunctorCompose k) where   -  type Unit (FunctorCompose k) = Id k+  type Unit (EndoFunctorCompose k) = Id k   unitObject _ = natId Id      leftUnitor     _ (Nat g _ _) = idPostcomp g@@ -85,12 +94,26 @@   , multiply :: (Cod f ~ k) => k ((f :% (a, a))) a   }   +trivialMonoid :: TensorProduct f => f -> MonoidObject f (Unit f)+trivialMonoid f = MonoidObject (unitObject f) (leftUnitor f (unitObject f))++coproductMonoid :: (HasInitialObject k, HasBinaryCoproducts k) => Obj k a -> MonoidObject (CoproductFunctor k) a+coproductMonoid a = MonoidObject (initialize a) (a ||| a)++ -- | @ComonoidObject f a@ defines a comonoid @a@ in a comonoidal category with tensor product @f@. data ComonoidObject f a = ComonoidObject   { counit     :: (Cod f ~ k) => k a (Unit f)   , comultiply :: (Cod f ~ k) => k a (f :% (a, a))   } +trivialComonoid :: TensorProduct f => f -> ComonoidObject f (Unit f)+trivialComonoid f = ComonoidObject (unitObject f) (leftUnitorInv f (unitObject f))+  +productComonoid :: (HasTerminalObject k, HasBinaryProducts k) => Obj k a -> ComonoidObject (ProductFunctor k) a+productComonoid a = ComonoidObject (terminate a) (a &&& a)++ data MonoidAsCategory f m a b where   MonoidValue :: (TensorProduct f, Dom f ~ (k :**: k), Cod f ~ k)               => f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m m@@ -105,7 +128,7 @@   -- | A monad is a monoid in the category of endofunctors.-type Monad f = MonoidObject (FunctorCompose (Dom f)) f+type Monad f = MonoidObject (EndoFunctorCompose (Dom f)) f  mkMonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k)    => f @@ -122,7 +145,7 @@   -- | A comonad is a comonoid in the category of endofunctors.-type Comonad f = ComonoidObject (FunctorCompose (Dom f)) f+type Comonad f = ComonoidObject (EndoFunctorCompose (Dom f)) f  mkComonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k)    => f
Data/Category/NaturalTransformation.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, NoImplicitPrelude #-}+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, LiberalTypeSynonyms, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.NaturalTransformation@@ -38,8 +38,11 @@        -- * Related functors   , FunctorCompose(..)-  , Precompose(..)-  , Postcompose(..)+  , EndoFunctorCompose+  , Precompose+  , precompose+  , Postcompose+  , postcompose   , Wrap(..)    ) where@@ -120,59 +123,50 @@ idPostcompInv f = Nat f (Id :.: f) (f %)  -constPrecomp :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (f :.: Const c1 (Dom f) x) (Const c1 (Cod f) (f :% x))+constPrecomp :: (Category c1, Functor f) +             => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (f :.: Const c1 (Dom f) x) (Const c1 (Cod f) (f :% x)) constPrecomp (Const x) f = let fx = f % x in Nat (f :.: Const x) (Const fx) (\_ -> fx) -constPrecompInv :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (Const c1 (Cod f) (f :% x)) (f :.: Const c1 (Dom f) x)+constPrecompInv :: (Category c1, Functor f) +                => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (Const c1 (Cod f) (f :% x)) (f :.: Const c1 (Dom f) x) constPrecompInv (Const x) f = let fx = f % x in Nat (Const fx) (f :.: Const x) (\_ -> fx) -constPostcomp :: Functor f => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 x)+constPostcomp :: (Category c2, Functor f) +              => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 x) constPostcomp (Const x) f = Nat (Const x :.: f) (Const x) (\_ -> x) -constPostcompInv :: Functor f => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Dom f) c2 x) (Const (Cod f) c2 x :.: f)+constPostcompInv :: (Category c2, Functor f) +                 => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Dom f) c2 x) (Const (Cod f) c2 x :.: f) constPostcompInv (Const x) f = Nat (Const x) (Const x :.: f) (\_ -> x)  ---- | The category of endofunctors.-type Endo k = Nat k k---data FunctorCompose (k :: * -> * -> *) = FunctorCompose+data FunctorCompose (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) = FunctorCompose --- | Composition of endofunctors is a functor.-instance Category k => Functor (FunctorCompose k) where-  type Dom (FunctorCompose k) = Endo k :**: Endo k-  type Cod (FunctorCompose k) = Endo k-  type FunctorCompose k :% (f, g) = f :.: g+-- | Composition of functors is a functor.+instance (Category c, Category d, Category e) => Functor (FunctorCompose c d e) where+  type Dom (FunctorCompose c d e) = Nat d e :**: Nat c d+  type Cod (FunctorCompose c d e) = Nat c e+  type FunctorCompose c d e :% (f, g) = f :.: g      FunctorCompose % (n1 :**: n2) = n1 `o` n2  -data Precompose :: * -> (* -> * -> *) -> * where-  Precompose :: f -> Precompose f d---- | @Precompose f d@ is the functor such that @Precompose f d :% g = g :.: f@,---   for functors @g@ that compose with @f@ and with codomain @d@.-instance (Functor f, Category d) => Functor (Precompose f d) where-  type Dom (Precompose f d) = Nat (Cod f) d-  type Cod (Precompose f d) = Nat (Dom f) d-  type Precompose f d :% g = g :.: f-  -  Precompose f % n = n `o` natId f-+-- | The category of endofunctors.+type Endo k = Nat k k+-- | Composition of endofunctors is a functor.+type EndoFunctorCompose k = FunctorCompose k k k -data Postcompose :: * -> (* -> * -> *) -> * where-  Postcompose :: f -> Postcompose f 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+precompose :: (Category e, Functor f) => f -> Precompose f e+precompose f = FunctorCompose :.: tuple2 (natId f)  -- | @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@.-instance (Functor f, Category c) => Functor (Postcompose f c) where-  type Dom (Postcompose f c) = Nat c (Dom f)-  type Cod (Postcompose f c) = Nat c (Cod f)-  type Postcompose f c :% g = f :.: g-  -  Postcompose f % n = natId f `o` n+type Postcompose f c = FunctorCompose c (Dom f) (Cod f) :.: Tuple1 (Nat (Dom f) (Cod f)) (Nat c (Dom f)) f+postcompose :: (Category e, Functor f) => f -> Postcompose f e+postcompose f = FunctorCompose :.: Tuple1 (natId f)   data Wrap f h = Wrap f h
Data/Category/Presheaf.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, TypeSynonymInstances, GADTs, FlexibleInstances, NoImplicitPrelude #-}+{-# LANGUAGE TypeOperators, TypeFamilies, TypeSynonymInstances, GADTs, FlexibleInstances, UndecidableInstances, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Presheaf@@ -26,7 +26,7 @@   :.: YonedaEmbedding k   ) pshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z-pshExponential y z = hom_X z :.: Opposite (ProductFunctor :.: Tuple2 y :.: yonedaEmbedding)+pshExponential y z = hom_X z :.: Opposite (ProductFunctor :.: tuple2 y :.: yonedaEmbedding)  -- | The category of presheaves on a category @C@ is cartesian closed for any @C@. instance Category k => CartesianClosed (Presheaves k) where
Data/Category/Simplex.hs view
@@ -68,11 +68,11 @@   tgt (Y f) = suc (tgt f)   tgt (X f) = tgt f   -  Z     .    f  = f-  f     .    Z  = f-  (Y f) .    g  = Y (f . g)-  (X f) . (Y g) = f . g-  (X f) . (X g) = X ((X f) . g)+  Z   .   f = f+  f   .   Z = f+  Y f .   g = Y (f . g)+  X f . Y g = f . g+  X f . X g = X (X f . g)   -- | The ordinal @0@ is the initial object of the simplex category.@@ -94,45 +94,6 @@   terminate (X (Y f)) = X (terminate f)  --type Merge m n = BinaryCoproduct Simplex m n--mergeLS :: Obj Simplex m -> Obj Simplex n -> Simplex (Merge (S m) n) (S (Merge m n))-mergeLS Z Z = X (Y Z)-mergeLS Z (X (Y n)) = X (Y (X (Y (Z +++ n))))-mergeLS (X (Y m)) Z = X (Y (X (Y (m +++ Z))))-mergeLS (X (Y m)) (X (Y n)) = X (Y (X (Y (mergeLS m n))))--mergeRS :: Obj Simplex m -> Obj Simplex n -> Simplex (Merge m (S n)) (S (Merge m n))-mergeRS Z Z = X (Y Z)-mergeRS Z (X (Y n)) = X (Y (X (Y (Z +++ n))))-mergeRS (X (Y m)) Z = X (Y (X (Y (m +++ Z))))-mergeRS (X (Y m)) (X (Y n)) = X (Y (X (Y (mergeRS m n))))---- | The coproduct in the simplex category is a merge operation.-instance HasBinaryCoproducts Simplex where-  type BinaryCoproduct Simplex  Z       Z  = Z-  type BinaryCoproduct Simplex  Z    (S n) = S (Merge Z n)-  type BinaryCoproduct Simplex (S m)    Z  = S (Merge m Z)-  type BinaryCoproduct Simplex (S m) (S n) = S (S (Merge m n))--  inj1       Z         Z   = Z-  inj1       Z   (X (Y n)) = Y (inj1 Z n)-  inj1 (X (Y m))       Z   = X (Y (inj1 m Z))-  inj1 (X (Y m)) (X (Y n)) = X (Y (Y (inj1 m n)))--  inj2       Z         Z   = Z-  inj2       Z   (X (Y n)) = X (Y (inj2 Z n))-  inj2 (X (Y m))       Z   = Y (inj2 m Z)-  inj2 (X (Y m)) (X (Y n)) = Y (X (Y (inj2 m n)))--  Z   ||| Z   = Z-  X f ||| X g = X (X (f ||| g))-  X f ||| Y g = X (f ||| Y g) . mergeLS (src f) (src g)-  Y f ||| X g = X (Y f ||| g) . mergeRS (src f) (src g)-  Y f ||| Y g = Y (f ||| g)-- data Fin :: * -> * where   Fz ::          Fin (S n)   Fs :: Fin n -> Fin (S n)@@ -143,9 +104,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   = \x -> x+  Forget % Y f = \x -> Fs ((Forget % f) x)+  Forget % X f = \x -> case x of     Fz -> Fz     Fs n -> (Forget % f) n @@ -181,7 +142,7 @@   -- | The maps @0 -> 1@ and @2 -> 1@ form a monoid, which is universal, c.f. `Replicate`.-universalMonoid :: MonoidObject (CoproductFunctor Simplex) (S Z)+universalMonoid :: MonoidObject Add (S Z) universalMonoid = MonoidObject { unit = Y Z, multiply = X (X (Y Z)) }  data Replicate f a = Replicate f (MonoidObject f a)
Data/Category/Yoneda.hs view
@@ -15,11 +15,13 @@ import Data.Category.NaturalTransformation import Data.Category.CartesianClosed -type YonedaEmbedding k = Postcompose (Hom k) (Op k) :.: ToTuple2 k (Op k)+type YonedaEmbedding k = +  Postcompose (Hom k) (Op k) :.: +  (Postcompose (Swap k (Op k)) (Op k) :.: Tuple k (Op k))  -- | The Yoneda embedding functor, @C -> Set^(C^op)@. yonedaEmbedding :: Category k => YonedaEmbedding k-yonedaEmbedding = Postcompose Hom :.: ToTuple2+yonedaEmbedding = postcompose Hom :.: (postcompose swap :.: Tuple)   data Yoneda (k :: * -> * -> *) f = Yoneda
data-category.cabal view
@@ -1,5 +1,5 @@ name:                data-category-version:             0.5.1.1+version:             0.6.0 synopsis:            Category theory  description:         Data-category is a collection of categories, and some categorical constructions on them.