data-category 0.7.1 → 0.7.2

raw patch · 11 files changed

+140/−92 lines, 11 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Data/Category/Adjunction.hs +7/−7
• Data/Category/Boolean.hs +29/−1
• Data/Category/CartesianClosed.hs +7/−6
• Data/Category/Comma.hs +8/−8
• Data/Category/Enriched.hs +3/−2
• Data/Category/Functor.hs +27/−27
• Data/Category/NNO.hs +21/−21
• Data/Category/NaturalTransformation.hs +12/−10
• Data/Category/RepresentableFunctor.hs +4/−4
• Data/Category/Yoneda.hs +21/−5
• data-category.cabal +1/−1

@@ -59,7 +59,7 @@   -> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))   -> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)   -> Adjunction c d f g-mkAdjunction f g l r = Adjunction f g (Nat (costar f) (star g) (\(Op a :**: _) -> l a)) (Nat (star g) (costar f) (\(_ :**: b) -> r b))+mkAdjunction f g l r = Adjunction f g (Nat (Costar f) (Star g) (\(Op a :**: _) -> l a)) (Nat (Star g) (Costar f) (\(_ :**: b) -> r b))  mkAdjunctionUnits :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)   => f -> g@@ -124,21 +124,21 @@  precomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e) precomposeAdj adj@(Adjunction f g _ _) = mkAdjunctionUnits-  (precompose g)-  (precompose f)+  (Precompose g)+  (Precompose f)   (\nh@(Nat h _ _) -> compAssocInv h g f . (nh `o` adjunctionUnit adj) . idPrecompInv h)   (\nh@(Nat h _ _) -> idPrecomp h . (nh `o` adjunctionCounit adj) . 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 adj@(Adjunction f g _ _) = mkAdjunctionUnits-  (postcompose f)-  (postcompose g)+  (Postcompose f)+  (Postcompose g)   (\nh@(Nat h _ _) -> compAssoc g f h . (adjunctionUnit adj `o` nh) . idPostcompInv h)   (\nh@(Nat h _ _) -> idPostcomp h . (adjunctionCounit adj `o` nh) . compAssocInv f g h)  contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r) contAdj = mkAdjunction-  (Opposite (hom_X (\x -> x)) :.: OpOpInv)-  (hom_X (\x -> x))+  (Opposite (Hom_X (\x -> x)) :.: OpOpInv)+  (Hom_X (\x -> x))   (\_ -> \(Op f) -> \b a -> f a b)   (\_ -> \f -> Op (\b a -> f a b))

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude #-}+{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, LambdaCase, ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Boolean@@ -19,7 +19,10 @@ import Data.Category.Monoidal import Data.Category.CartesianClosed +import Data.Category.Functor+import Data.Category.NaturalTransformation + data Fls data Tru @@ -154,3 +157,28 @@  falseProductComonoid :: ComonoidObject (ProductFunctor Boolean) Fls falseProductComonoid = ComonoidObject F2T Fls+++data 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+  type Cod (Arrow k a b) = k+  type Arrow k a b :% Fls = a+  type Arrow k a b :% Tru = b+  Arrow f % Fls = src f+  Arrow f % F2T = f+  Arrow f % Tru = tgt f+++type instance LimitFam Boolean k f = f :% Fls+-- | The limit of a functor from the Boolean category is the source of the arrow it points to.+instance Category k => HasLimits Boolean k where+  limit (Nat f _ _) = Nat (Const (f % Fls)) f (\case Fls -> f % Fls; Tru -> f % F2T)+  limitFactorizer Nat{} = \n -> n ! Fls++type instance ColimitFam Boolean k f = f :% Tru+-- | The colimit of a functor from the Boolean category is the target of the arrow it points to.+instance Category k => HasColimits Boolean k where+  colimit (Nat f _ _) = Nat f (Const (f % Tru)) (\case Fls -> f % F2T; Tru -> f % Tru)+  colimitFactorizer Nat{} = \n -> n ! Tru

@@ -3,6 +3,7 @@   TypeFamilies,   GADTs,   Rank2Types,+  PatternSynonyms,   ScopedTypeVariables,   UndecidableInstances,   TypeSynonymInstances,@@ -83,16 +84,16 @@   :.: Tuple2 (Presheaves k) (Presheaves k) y   :.: 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)+pattern PshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z+pattern 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   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))-  zn ^^^ yn = Nat (pshExponential (tgt yn) (src zn)) (pshExponential (src yn) (tgt zn)) (\(Op i) n -> zn . n . (natId (hom_X i) *** yn))+  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))+  zn ^^^ yn = Nat (PshExponential (tgt yn) (src zn)) (PshExponential (src yn) (tgt zn)) (\(Op i) n -> zn . n . (natId (Hom_X i) *** yn))   @@ -102,7 +103,7 @@          -> Adjunction k k               (ProductFunctor k :.: Tuple2 k k y)               (ExpFunctor k :.: Tuple1 (Op k) k y)-curryAdj y = mkAdjunctionUnits (ProductFunctor :.: tuple2 y) (ExpFunctor :.: tuple1 (Op y)) (tuple y) (apply y)+curryAdj y = mkAdjunctionUnits (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.

@@ -21,12 +21,12 @@ data CommaO :: * -> * -> * -> * 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-  CommaA ::+    +data (:/\:) :: * -> * -> * -> * -> * where +  CommaA ::      CommaO t s (a, b) ->-    Dom t a a' ->-    Dom s b b' ->+    Dom t a a' -> +    Dom s b b' ->      CommaO t s (a', b') ->     (t :/\: s) (a, b) (a', b') @@ -35,10 +35,10 @@  -- | The comma category T \\downarrow S instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s) where-+       src (CommaA so _ _ _) = commaId so   tgt (CommaA _ _ _ to) = commaId to-+     (CommaA _ g h to) . (CommaA so g' h' _) = CommaA so (g . g') (h . h') to  @@ -53,7 +53,7 @@                        . (Functor u, c ~ (u `ObjectsFUnder` x), HasInitialObject c, (a_, a) ~ InitialObject c)                       => u -> InitialUniversal x u a initialUniversalComma u = case initialObject :: Obj c (a_, a) of-  CommaA (CommaO _ mor a) _ _ _ ->+  CommaA (CommaO _ mor a) _ _ _ ->      initialUniversal u a mor factorizer       where         factorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y

@@ -3,6 +3,7 @@   , TypeFamilies   , GADTs   , RankNTypes+  , PatternSynonyms   , FlexibleContexts   , NoImplicitPrelude   , UndecidableInstances@@ -24,7 +25,7 @@  import Data.Category (Category(..), Obj, Op(..)) import Data.Category.Product-import Data.Category.Functor (Functor(..), Hom(..), (:*-:), homX_)+import Data.Category.Functor (Functor(..), Hom(..), (:*-:), pattern HomX_) import Data.Category.Limit hiding (HasLimits) import Data.Category.CartesianClosed import Data.Category.Boolean@@ -46,7 +47,7 @@ -- | The elements of @k@ as a functor from @V k@ to @(->)@  type Elem k = TerminalObject (V k) :*-: (V k) elem :: CartesianClosed (V k) => Elem k-elem = homX_ terminalObject+elem = HomX_ terminalObject  -- | Arrows as elements of @k@ type Arr k a b = Elem k :% (k $ (a, b))

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, ConstraintKinds, NoImplicitPrelude #-}+{-# LANGUAGE TypeOperators, TypeFamilies, PatternSynonyms, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, ConstraintKinds, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Functor@@ -31,17 +31,17 @@   , Proj2(..)   , (:***:)(..)   , DiagProd(..)-  , Tuple1, tuple1-  , Tuple2, tuple2-  , Swap, swap+  , Tuple1, pattern Tuple1+  , Tuple2, pattern Tuple2+  , Swap, pattern Swap    -- *** Hom functors   , Hom(..)-  , (:*-:), homX_-  , (:-*:), hom_X-  , HomF, homF-  , Star, star-  , Costar, costar+  , (:*-:), pattern HomX_+  , (:-*:), pattern Hom_X+  , HomF, pattern HomF+  , Star, pattern Star+  , Costar, pattern Costar  ) where @@ -138,7 +138,7 @@    Opposite f % Op a = Op (f % a) -+   data OpOp (k :: * -> * -> *) = OpOp  -- | The @Op (Op x) = x@ functor.@@ -183,7 +183,7 @@   Proj2 % (_ :**: f2) = f2  -data f1 :***: f2 = f1 :***: f2+data f1 :***: f2 where (:***:) :: (Functor f1, Functor f2) => f1 -> f2 -> f1 :***: f2  -- | @f1 :***: f2@ is the product of the functors @f1@ and @f2@. instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where@@ -208,8 +208,8 @@ type Tuple1 c1 c2 a = (Const c2 c1 a :***: Id c2) :.: DiagProd c2  -- | 'Tuple1' tuples with a fixed object on the left.-tuple1 :: (Category c1, Category c2) => Obj c1 a -> Tuple1 c1 c2 a-tuple1 a = (Const a :***: Id) :.: DiagProd+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 --@@ -219,13 +219,13 @@  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+pattern Swap :: (Category c1, Category c2) => Swap c1 c2+pattern 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.-tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a-tuple2 a = swap :.: tuple1 a+pattern Tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a+pattern Tuple2 a = Swap :.: Tuple1 a   @@ -242,23 +242,23 @@  type x :*-: k = Hom k :.: Tuple1 (Op k) k x -- | The covariant functor Hom(X,--)-homX_ :: Category k => Obj k x -> x :*-: k-homX_ x = Hom :.: tuple1 (Op x)+pattern HomX_ :: Category k => Obj k x -> x :*-: k+pattern HomX_ x = Hom :.: Tuple1 (Op x)  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+pattern Hom_X :: Category k => Obj k x -> k :-*: x+pattern Hom_X x = Hom :.: Tuple2 x   type HomF f g = Hom (Cod f) :.: (Opposite f :***: g)-homF :: (Functor f, Functor g, Cod f ~ Cod g) => f -> g -> HomF f g-homF f g = Hom :.: (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-star :: Functor f => f -> Star f-star f = homF Id f+pattern Star :: Functor f => f -> Star f+pattern Star f = HomF Id f  type Costar f = HomF f (Id (Cod f))-costar :: Functor f => f -> Costar f-costar f = homF f Id+pattern Costar :: Functor f => f -> Costar f+pattern Costar f = HomF f Id

@@ -18,44 +18,44 @@   class HasTerminalObject k => HasNaturalNumberObject k where-+     type NaturalNumberObject k :: *-+     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)  -type Nat = Fix ((:++:) Unit)+-- 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-  type Cod (PrimRec z s) = Cod z-  type PrimRec z s :% I1 () = z :% ()-  type PrimRec z s :% I2 n  = s :% PrimRec z s :% n-  PrimRec z _ % Fix (I1 Unit) = z % Unit-  PrimRec z s % Fix (I2 n) = s % PrimRec z s % n+  +-- 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+--   type Cod (PrimRec z s) = Cod z+--   type PrimRec z s :% I1 () = z :% ()+--   type PrimRec z s :% I2 n  = s :% PrimRec z s :% n+--   PrimRec z _ % Fix (I1 Unit) = z % Unit+--   PrimRec z s % Fix (I2 n) = s % PrimRec z s % n

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, LiberalTypeSynonyms, NoImplicitPrelude #-}+{-# LANGUAGE TypeOperators, TypeFamilies, PatternSynonyms, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, LiberalTypeSynonyms, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.NaturalTransformation@@ -40,10 +40,8 @@   -- * Related functors   , FunctorCompose(..)   , EndoFunctorCompose-  , Precompose-  , precompose-  , Postcompose-  , postcompose+  , Precompose, pattern Precompose+  , Postcompose, pattern Postcompose   , Wrap(..)   , Apply(..)   , Tuple(..)@@ -84,6 +82,10 @@ natId :: Functor f => f -> Nat (Dom f) (Cod f) f f natId f = Nat f f (\i -> f % i) +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)+ srcF :: Nat c d f g -> f srcF (Nat f _ _) = f @@ -158,14 +160,14 @@ -- | @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)+pattern Precompose :: (Category e, Functor f) => f -> Precompose f e+pattern 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@. 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)+pattern Postcompose :: (Category e, Functor f) => f -> Postcompose f e+pattern Postcompose f = FunctorCompose :.: Tuple1 (NatId f)   data Wrap f h = Wrap f h@@ -194,4 +196,4 @@   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)) (\z -> f :**: z)

@@ -26,7 +26,7 @@  covariantHomRepr :: Category k => Obj k x -> Representable (x :*-: k) x covariantHomRepr x = Representable-  { representedFunctor = homX_ x+  { representedFunctor = HomX_ x   , representingObject = x   , represent          = \_ h -> h   , universalElement   = x@@ -34,7 +34,7 @@  contravariantHomRepr :: Category k => Obj k x -> Representable (k :-*: x) x contravariantHomRepr x = Representable-  { representedFunctor = hom_X x+  { representedFunctor = Hom_X x   , representingObject = Op x   , represent          = \_ h -> Op h   , universalElement   = x@@ -49,7 +49,7 @@                  -> (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+  { representedFunctor = HomX_ (src mor) :.: u   , representingObject = obj   , represent          = factorizer   , universalElement   = mor@@ -64,7 +64,7 @@                   -> (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+  { representedFunctor = Hom_X (tgt mor) :.: Opposite u   , representingObject = Op obj   , represent          = \(Op y) f -> Op (factorizer y f)   , universalElement   = mor

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, RankNTypes, TypeFamilies, NoImplicitPrelude #-}+{-# LANGUAGE TypeOperators, RankNTypes, TypeFamilies, PatternSynonyms, UndecidableInstances, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Yoneda@@ -13,14 +13,15 @@ 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))  -- | The Yoneda embedding functor, @C -> Set^(C^op)@.-yonedaEmbedding :: Category k => YonedaEmbedding k-yonedaEmbedding = postcompose Hom :.: (postcompose swap :.: Tuple)+pattern YonedaEmbedding :: Category k => YonedaEmbedding k+pattern YonedaEmbedding = Postcompose Hom :.: (Postcompose Swap :.: Tuple)   data Yoneda (k :: * -> * -> *) f = Yoneda@@ -29,7 +30,7 @@   type Dom (Yoneda k f) = Op k   type Cod (Yoneda k f) = (->)   type Yoneda k f :% a = Nat (Op k) (->) (k :-*: a) f-  Yoneda % Op ab = \n -> n . yonedaEmbedding % ab+  Yoneda % Op ab = \n -> n . YonedaEmbedding % ab   -- | 'fromYoneda' and 'toYoneda' are together the isomophism from the Yoneda lemma.@@ -37,4 +38,19 @@ fromYoneda f = Nat Yoneda f (\(Op a) n -> (n ! Op a) a)  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))+toYoneda   f = Nat f Yoneda (\(Op a) fa -> Nat (Hom_X a) f (\_ h -> (f % Op h) fa))++haskUnit :: Obj (->) ()+haskUnit () = ()++data M1 = M1+instance Functor M1 where+  type Dom M1 = Nat (Op (->)) (->)+  type Cod M1 = (->)+  type M1 :% f = f :% ()+  M1 % n = n ! Op haskUnit++haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) M1 (YonedaEmbedding (->))+haskIsTotal = mkAdjunction M1 YonedaEmbedding+  (\(Nat f _ _) fu2b -> Nat f (Hom :.: (Swap :.: Tuple1 (\x -> x))) (\_ fz z -> fu2b ((f % Op (\() -> z)) fz)))+  (\_ n@(Nat f _ _) fu -> (n ! Op haskUnit) fu ())

@@ -1,5 +1,5 @@ name:                data-category-version:             0.7.1+version:             0.7.2 synopsis:            Category theory  description:         Data-category is a collection of categories, and some categorical constructions on them.