packages feed

data-category 0.8 → 0.8.1

raw patch · 9 files changed

+124/−93 lines, 9 files

Files

Data/Category/Adjunction.hs view
@@ -14,6 +14,8 @@     Adjunction(..)   , mkAdjunction   , mkAdjunctionUnits+  , mkAdjunctionUnit+  , mkAdjunctionCounit    , leftAdjunct   , rightAdjunct@@ -67,6 +69,20 @@   -> (forall a. Obj c a -> Component (f :.: g) (Id c) a)   -> Adjunction c d f g mkAdjunctionUnits f g un coun = mkAdjunction f g (\a h -> (g % h) . un a) (\b h -> coun b . (f % h))++mkAdjunctionUnit :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)+  => f -> g+  -> (forall a. Obj d a -> Component (Id d) (g :.: f) a)+  -> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)+  -> Adjunction c d f g+mkAdjunctionUnit f g un adj = mkAdjunction f g (\a h -> (g % h) . un a) adj++mkAdjunctionCounit :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)+  => f -> g+  -> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))+  -> (forall a. Obj c a -> Component (f :.: g) (Id c) a)+  -> Adjunction c d f g+mkAdjunctionCounit f g adj coun = mkAdjunction f g adj (\b h -> coun b . (f % h))  leftAdjunct :: Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b) leftAdjunct (Adjunction _ _ l _) a h = (l ! (Op a :**: tgt h)) h
Data/Category/Boolean.hs view
@@ -175,10 +175,10 @@ -- | 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+  limitFactorizer 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+  colimitFactorizer n = n ! Tru
Data/Category/Comma.hs view
@@ -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  @@ -48,12 +48,14 @@ 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 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
Data/Category/Dialg.hs view
@@ -39,10 +39,10 @@  -- | The category of (F,G)-dialgebras. instance Category (Dialg f g) where-  +   src (DialgA s _ _) = dialgId s   tgt (DialgA _ t _) = dialgId t-  +   DialgA _ t f . DialgA s _ g = DialgA s t (f . g)  @@ -76,11 +76,11 @@ -- | The category for defining the natural numbers and primitive recursion can be described as -- @Dialg(F,G)@, with @F(A)=\<1,A>@ and @G(A)=\<A,A>@. instance HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) where-  +   type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) = NatNum-    +   initialObject = dialgId (Dialgebra (\x -> x) (Z :**: S))-  +   initialize (dialgebra -> d@(Dialgebra _ (z :**: s))) = DialgA (dialgebra initialObject) d (primRec z s)  @@ -91,11 +91,11 @@   type Dom (FreeAlg m) = Dom m   type Cod (FreeAlg m) = Alg m   type FreeAlg m :% a = m :% a-  FreeAlg m % f = DialgA (alg (src f)) (alg (tgt f)) (monadFunctor m % f)-    where-      alg :: Obj k x -> Algebra m (m :% x)-      alg x = Dialgebra (monadFunctor m % x) (multiply m ! x)+  FreeAlg m % f = DialgA (freeAlg m (src f)) (freeAlg m (tgt f)) (monadFunctor m % f) +freeAlg :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj (Cod m) x -> Algebra m (m :% x)+freeAlg m x = Dialgebra (monadFunctor m % x) (multiply m ! x)+ data ForgetAlg m = ForgetAlg -- | @ForgetAlg m@ is the forgetful functor for @Alg m@. instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (ForgetAlg m) where@@ -107,5 +107,5 @@ eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k)   => Monad m -> A.Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m) eilenbergMooreAdj m = A.mkAdjunctionUnits (FreeAlg m) ForgetAlg-  (\x -> unit m ! x)-  (\(DialgA (Dialgebra _ h) _ _) -> DialgA (Dialgebra (src h) (monadFunctor m % h)) (Dialgebra (tgt h) h) h)+  (unit m !)+  (\(DialgA b@(Dialgebra _ h) _ _) -> DialgA (Dialgebra (src h) (monadFunctor m % h)) b h)
Data/Category/Kleisli.hs view
@@ -12,7 +12,7 @@ -- of an adjunction for each monad. ----------------------------------------------------------------------------- module Data.Category.Kleisli where-  + import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -28,30 +28,28 @@  -- | The category of Kleisli arrows. instance Category (Kleisli m) where-  +   src (Kleisli m _ f) = kleisliId m (src f)   tgt (Kleisli m b _) = kleisliId m b-  +   (Kleisli m c f) . (Kleisli _ _ g) = Kleisli m c ((multiply m ! c) . (monadFunctor m % f) . g)   -data KleisliAdjF m = KleisliAdjF (Monad m)-instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjF m) where-  type Dom (KleisliAdjF m) = Dom m-  type Cod (KleisliAdjF m) = Kleisli m-  type KleisliAdjF m :% a = a-  KleisliAdjF m % f = Kleisli m (tgt f) ((unit m ! tgt f) . f)-   -data KleisliAdjG m = KleisliAdjG (Monad m)-instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjG m) where-  type Dom (KleisliAdjG m) = Kleisli m-  type Cod (KleisliAdjG m) = Dom m-  type KleisliAdjG m :% a = m :% a-  KleisliAdjG m % Kleisli _ b f = (multiply m ! b) . (monadFunctor m % f)+newtype KleisliFree m = KleisliFree (Monad m)+instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliFree m) where+  type Dom (KleisliFree m) = Dom m+  type Cod (KleisliFree m) = Kleisli m+  type KleisliFree m :% a = a+  KleisliFree m % f = Kleisli m (tgt f) ((unit m ! tgt f) . f) +data KleisliForget m = KleisliForget+instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliForget m) where+  type Dom (KleisliForget m) = Kleisli m+  type Cod (KleisliForget m) = Dom m+  type KleisliForget m :% a = m :% a+  KleisliForget % Kleisli m b f = (multiply m ! b) . (monadFunctor m % f)+ kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k)-  => Monad m -> A.Adjunction (Kleisli m) k (KleisliAdjF m) (KleisliAdjG m)-kleisliAdj m = A.mkAdjunctionUnits (KleisliAdjF m) (KleisliAdjG m)-  (\x -> unit m ! x)-  (\(Kleisli _ x _) -> Kleisli m x (monadFunctor m % x))+  => Monad m -> A.Adjunction (Kleisli m) k (KleisliFree m) (KleisliForget m)+kleisliAdj m = A.mkAdjunctionUnit (KleisliFree m) KleisliForget (unit m !) (\(Kleisli _ x _) f -> Kleisli m x f)
Data/Category/Limit.hs view
@@ -41,6 +41,8 @@   , HasLimits(..)   , LimitFunctor(..)   , limitAdj+  , adjLimit+  , adjLimitFactorizer   , rightAdjointPreservesLimits   , rightAdjointPreservesLimitsInv @@ -50,6 +52,8 @@   , HasColimits(..)   , ColimitFunctor(..)   , colimitAdj+  , adjColimit+  , adjColimitFactorizer   , leftAdjointPreservesColimits   , leftAdjointPreservesColimitsInv @@ -103,18 +107,18 @@   -- | A cone from N to F is a natural transformation from the constant functor to N to F.-type Cone   f n = Nat (Dom f) (Cod f) (ConstF f n) f+type Cone   j k f n = Nat j k (Const j k n) f  -- | A co-cone from F to N is a natural transformation from F to the constant functor to N.-type Cocone f n = Nat (Dom f) (Cod f) f (ConstF f n)+type Cocone j k f n = Nat j k f (Const j k n)   -- | The vertex (or apex) of a cone.-coneVertex :: Cone f n -> Obj (Cod f) n+coneVertex :: Cone j k f n -> Obj k n coneVertex (Nat (Const x) _ _) = x  -- | The vertex (or apex) of a co-cone.-coconeVertex :: Cocone f n -> Obj (Cod f) n+coconeVertex :: Cocone j k f n -> Obj k n coconeVertex (Nat _ (Const x) _) = x  @@ -127,10 +131,10 @@ -- | An instance of @HasLimits j k@ says that @k@ has all limits of type @j@. class (Category j, Category k) => HasLimits j k where   -- | 'limit' returns the limiting cone for a functor @f@.-  limit           :: Obj (Nat j k) f -> Cone f (Limit 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   --   by returning the morphism between the vertices of the cones.-  limitFactorizer :: Obj (Nat j k) f -> Cone f n -> k n (Limit f)+  limitFactorizer :: Cone j k f n -> k n (LimitFam j k f)  data LimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = LimitFunctor -- | If every diagram of type @j@ has a limit in @k@ there exists a limit functor.@@ -140,13 +144,19 @@   type Cod (LimitFunctor j k) = k   type LimitFunctor j k :% f = LimitFam j k f -  LimitFunctor % n @ Nat{}  = limitFactorizer (tgt n) (n . limit (src n))+  LimitFunctor % n = limitFactorizer (n . limit (src n))  -- | The limit functor is right adjoint to the diagonal functor. limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)-limitAdj = mkAdjunctionUnits diag LimitFunctor (\a -> limitFactorizer (diag % a) (diag % a)) (\f @ Nat{} -> limit f)-  where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same.+limitAdj = mkAdjunctionCounit Diag LimitFunctor (\_ -> limitFactorizer) limit +adjLimit :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Obj (Nat j k) f -> Cone j k f (r :% f)+adjLimit adj f = adjunctionCounit adj ! f++adjLimitFactorizer :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Cone j k f n -> k n (r :% f)+adjLimitFactorizer adj cone = leftAdjunct adj (coneVertex cone) cone++ -- Cone (g :.: t) (Limit (g :.: t)) -- Obj j z -> d (Limit (g :.: t)) ((g :.: t) :% z) -- Obj j z -> d (f :% Limit (g :.: t)) (t :% z)@@ -157,7 +167,7 @@   :: (HasLimits j c, HasLimits j d)   => Adjunction c d f g -> Obj (Nat j c) t -> d (Limit (g :.: t)) (g :% Limit t) rightAdjointPreservesLimits adj@(Adjunction f g _ _) (Nat t _ _) =-  leftAdjunct adj x (limitFactorizer (natId t) cone)+  leftAdjunct adj x (limitFactorizer cone)     where       l = limit (natId (g :.: t))       x = coneVertex l@@ -169,8 +179,8 @@ -- d (g :% Limit t) (Limit (g :.: t)) rightAdjointPreservesLimitsInv   :: (HasLimits j c, HasLimits j d)-  => Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% Limit t) (Limit (g :.: t))-rightAdjointPreservesLimitsInv g@Nat{} t@Nat{} = limitFactorizer (g `o` t) (constPrecompIn (g `o` limit t))+  => Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% LimitFam j c t) (LimitFam j d (g :.: t))+rightAdjointPreservesLimitsInv g t = limitFactorizer (constPrecompIn (g `o` limit t))  -- | Colimits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@. type family ColimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *@@ -180,10 +190,10 @@ -- | An instance of @HasColimits j k@ says that @k@ has all colimits of type @j@. class (Category j, Category k) => HasColimits j k where   -- | 'colimit' returns the limiting co-cone for a functor @f@.-  colimit           :: Obj (Nat j k) f -> Cocone f (Colimit 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   --   by returning the morphism between the vertices of the cones.-  colimitFactorizer :: Obj (Nat j k) f -> Cocone f n -> k (Colimit f) n+  colimitFactorizer :: Cocone j k f n -> k (ColimitFam j k f) n  data ColimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = ColimitFunctor -- | If every diagram of type @j@ has a colimit in @k@ there exists a colimit functor.@@ -193,19 +203,24 @@   type Cod (ColimitFunctor j k) = k   type ColimitFunctor j k :% f = ColimitFam j k f -  ColimitFunctor % n @ Nat{}  = colimitFactorizer (src n) (colimit (tgt n) . n)+  ColimitFunctor % n = colimitFactorizer (colimit (tgt n) . n)  -- | The colimit functor is left adjoint to the diagonal functor. colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)-colimitAdj = mkAdjunctionUnits ColimitFunctor diag (\f @ Nat{} -> colimit f) (\a -> colimitFactorizer (diag % a) (diag % a))-  where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same.+colimitAdj = mkAdjunctionUnit ColimitFunctor Diag colimit (\_ -> colimitFactorizer) +adjColimit :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Obj (Nat j k) f -> Cocone j k f (l :% f)+adjColimit adj f = adjunctionUnit adj ! f +adjColimitFactorizer :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Cocone j k f n -> k (l :% f) n+adjColimitFactorizer adj cocone = rightAdjunct adj (coconeVertex cocone) cocone++ leftAdjointPreservesColimits   :: (HasColimits j c, HasColimits j d)   => Adjunction c d f g -> Obj (Nat j d) t -> c (f :% Colimit t) (Colimit (f :.: t)) leftAdjointPreservesColimits adj@(Adjunction f g _ _) (Nat t _ _) =-  rightAdjunct adj x (colimitFactorizer (natId t) cocone)+  rightAdjunct adj x (colimitFactorizer cocone)     where       l = colimit (natId (f :.: t))       x = coconeVertex l@@ -213,8 +228,8 @@  leftAdjointPreservesColimitsInv   :: (HasColimits j c, HasColimits j d)-  => Obj (Nat d c) f -> Obj (Nat j d) t -> c (Colimit (f :.: t)) (f :% Colimit t)-leftAdjointPreservesColimitsInv f@Nat{} t@Nat{} = colimitFactorizer (f `o` t) (constPrecompOut (f `o` colimit t))+  => Obj (Nat d c) f -> Obj (Nat j d) t -> c (ColimitFam j c (f :.: t)) (f :% ColimitFam j d t)+leftAdjointPreservesColimitsInv f t = colimitFactorizer (constPrecompOut (f `o` colimit t))   class Category k => HasTerminalObject k where@@ -232,7 +247,7 @@ instance (Category k, HasTerminalObject k) => HasLimits Void k where    limit (Nat f _ _) = voidNat (Const terminalObject) f-  limitFactorizer Nat{} = terminate . coneVertex+  limitFactorizer = terminate . coneVertex   -- | @()@ is the terminal object in @Hask@.@@ -300,7 +315,7 @@ instance (Category k, HasInitialObject k) => HasColimits Void k where    colimit (Nat f _ _) = voidNat f (Const initialObject)-  colimitFactorizer Nat{} = initialize . coconeVertex+  colimitFactorizer = initialize . coconeVertex   data Zero@@ -376,7 +391,7 @@    limit = limit'     where-      limit' :: forall f. Obj (Nat (i :++: j) k) f -> Cone f (Limit f)+      limit' :: forall f. Obj (Nat (i :++: j) k) f -> Cone (i :++: j) k f (LimitFam (i :++: j) k f)       limit' l@Nat{} = Nat (Const (x *** y)) (srcF l) h         where           x = coneVertex lim1@@ -387,10 +402,10 @@           h (I1 n) = lim1 ! n . proj1 x y           h (I2 n) = lim2 ! n . proj2 x y -  limitFactorizer l@Nat{} c =-    limitFactorizer (l `o` natId Inj1) (constPostcompIn (c `o` natId Inj1))+  limitFactorizer c =+    limitFactorizer (constPostcompIn (c `o` natId Inj1))     &&&-    limitFactorizer (l `o` natId Inj2) (constPostcompIn (c `o` natId Inj2))+    limitFactorizer (constPostcompIn (c `o` natId Inj2))   -- | The tuple is the binary product in @Hask@.@@ -512,7 +527,7 @@    colimit = colimit'     where-      colimit' :: forall f. Obj (Nat (i :++: j) k) f -> Cocone f (Colimit f)+      colimit' :: forall f. Obj (Nat (i :++: j) k) f -> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f)       colimit' l@Nat{} = Nat (srcF l) (Const (x +++ y)) h         where           x = coconeVertex col1@@ -523,10 +538,10 @@           h (I1 n) = inj1 x y . col1 ! n           h (I2 n) = inj2 x y . col2 ! n -  colimitFactorizer l@Nat{} c =-    colimitFactorizer (l `o` natId Inj1) (constPostcompOut (c `o` natId Inj1))+  colimitFactorizer c =+    colimitFactorizer (constPostcompOut (c `o` natId Inj1))     |||-    colimitFactorizer (l `o` natId Inj2) (constPostcompOut (c `o` natId Inj2))+    colimitFactorizer (constPostcompOut (c `o` natId Inj2))   -- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'.@@ -654,7 +669,7 @@ instance Category k => HasLimits Unit k where    limit (Nat f _ _) = Nat (Const (f % Unit)) f (\Unit -> f % Unit)-  limitFactorizer Nat{} n = n ! Unit+  limitFactorizer n = n ! Unit  type instance LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j) @@ -662,7 +677,7 @@ instance (HasInitialObject (i :>>: j), Category i, Category j, Category k) => HasLimits (i :>>: j) k where    limit (Nat f _ _) = Nat (Const (f % initialObject)) f (\z -> f % initialize z)-  limitFactorizer Nat{} n = n ! initialObject+  limitFactorizer n = n ! initialObject   type instance ColimitFam Unit k f = f :% ()@@ -671,7 +686,7 @@ instance Category k => HasColimits Unit k where    colimit (Nat f _ _) = Nat f (Const (f % Unit)) (\Unit -> f % Unit)-  colimitFactorizer Nat{} n = n ! Unit+  colimitFactorizer n = n ! Unit  type instance ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j) @@ -679,7 +694,7 @@ instance (HasTerminalObject (i :>>: j), Category i, Category j, Category k) => HasColimits (i :>>: j) k where    colimit (Nat f _ _) = Nat f (Const (f % terminalObject)) (\z -> f % terminate z)-  colimitFactorizer Nat{} n = n ! terminalObject+  colimitFactorizer n = n ! terminalObject   data ForAll f = ForAll (forall a. Obj (->) a -> f :% a)@@ -687,11 +702,11 @@  instance HasLimits (->) (->) where   limit (Nat f _ _) = Nat (Const (\x -> x)) f (\a (ForAll g) -> g a)-  limitFactorizer Nat{} n = \z -> ForAll (\a -> (n ! a) z)+  limitFactorizer n = \z -> ForAll (\a -> (n ! a) z)  data Exists f = forall a. Exists (Obj (->) a) (f :% a) type instance ColimitFam (->) (->) f = Exists f  instance HasColimits (->) (->) where   colimit (Nat f _ _) = Nat f (Const (\x -> x)) Exists-  colimitFactorizer Nat{} n = \(Exists a fa) -> (n ! a) fa+  colimitFactorizer n = \(Exists a fa) -> (n ! a) fa
Data/Category/NNO.hs view
@@ -18,24 +18,24 @@   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) @@ -43,14 +43,14 @@ -- type Nat = Fix ((:++:) Unit)  -- instance HasNaturalNumberObject Cat where----   type NaturalNumberObject Cat = Nat-+  +--   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
Data/Category/Yoneda.hs view
@@ -51,6 +51,6 @@   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)))+haskIsTotal = mkAdjunctionUnit M1 YonedaEmbedding+  (\(Nat f _ _) -> Nat f (Hom_X (f % Op haskUnit)) (\_ fz z -> (f % Op (\() -> z)) fz))   (\_ n@(Nat f _ _) fu -> (n ! Op haskUnit) fu ())
data-category.cabal view
@@ -1,5 +1,5 @@ name:                data-category-version:             0.8+version:             0.8.1 synopsis:            Category theory  description:         Data-category is a collection of categories, and some categorical constructions on them.