{-# LANGUAGE RankNTypes, PolyKinds, GADTs, MultiParamTypeClasses, TypeOperators, Arrows, Safe, ConstraintKinds #-}
 module Math.Tools.NaturalTransformation where
 
 -- Basic support for natural transformations.
 -- This is very basic concept from category theory.
 -- 
 -- For reference I've used:
 -- <Natural transformation in wikipedia|https://en.wikipedia.org/wiki/Natural_transformation>
 -- <Natural transformation in ncatlab|https://ncatlab.org/nlab/show/natural+transformation>
 -- Roy L. Crole: Categories for Types.
 import Data.Kind
 import Math.Tools.I
 import Math.Tools.CoMonad
 import Control.Monad
 import Control.Applicative
 import Control.Category
 import Control.Arrow
 import Math.Tools.Adjunction
 import Math.Tools.OppositeArrow
 import Math.Tools.Arrow
 import Math.Tools.CoFunctor
 import Math.Tools.Isomorphism
 import Math.Tools.FixedPoint
 import Math.Matrix.Interface
 import Prelude hiding ((.),id)

  -- === NATURAL TRANSFORMATION ============

 newtype (f :: k -> Type) :~> (g :: k -> Type) = NatTrans {
    forall k (f :: k -> *) (g :: k -> *).
(f :~> g) -> forall (a :: k). f a -> g a
nattransComponent :: forall (a :: k). f a -> g a
  }

 instance Category (:~>) where
    id :: forall (a :: k -> *). a :~> a
id = (forall (a :: k). a a -> a a) -> a :~> a
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans a a -> a a
forall (a :: k). a a -> a a
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
    (NatTrans forall (a :: k). b a -> c a
f) . :: forall (b :: k -> *) (c :: k -> *) (a :: k -> *).
(b :~> c) -> (a :~> b) -> a :~> c
. (NatTrans forall (a :: k). a a -> b a
g) = (forall (a :: k). a a -> c a) -> a :~> c
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (b a -> c a
forall (a :: k). b a -> c a
f (b a -> c a) -> (a a -> b a) -> a a -> c a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a a -> b a
forall (a :: k). a a -> b a
g)

 type MaybeNT m = Maybe :~> m
 type EitherNT a m = (Either a) :~> m
 type PairNT a m = ((,) a) :~> m
 type IndexNT a m = ((->) a) :~> m
 type ListNT m = [] :~> m

 type IMT m = I :~> m
 type IOMT m = m :~> IO
 type NondetMT m = m :~> []
 type FailMT m = m :~> Maybe
 type AltMT a m  = m :~> Either a
 type FunctorMT a m = m :~> ((->) a)

 type MonadNT m = (m :*: m) :~> m
 type ComonadNT m = m :~> (m :*: m)
 type TransposeNT m n = (m :*: n) :~> (n :*: m)

 type (row ::*:: col) elem = (((:==:) row) :*: ((:==:) col)) elem

 failFailMT :: FailMT f
 failFailMT :: forall (f :: * -> *). FailMT f
failFailMT = (forall a. f a -> Maybe a) -> f :~> Maybe
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (Maybe a -> f a -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing)
 succeedFailMT :: FailMT I
 succeedFailMT :: FailMT I
succeedFailMT = (forall a. I a -> Maybe a) -> FailMT I
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (\ (I a
x) -> a -> Maybe a
forall a. a -> Maybe a
Just a
x)
 returnMT :: (Monad m) => I :~> m
 returnMT :: forall (m :: * -> *). Monad m => I :~> m
returnMT = (forall a. I a -> m a) -> I :~> m
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> (I a -> a) -> I a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. I a -> a
forall a. I a -> a
unI)
 extractMT :: (Comonad m) => m :~> I
 extractMT :: forall (m :: * -> *). Comonad m => m :~> I
extractMT = (forall a. m a -> I a) -> m :~> I
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (a -> I a
forall a. a -> I a
I (a -> I a) -> (m a -> a) -> m a -> I a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. m a -> a
forall a. m a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract)
 duplicateMT :: (Comonad m) => m :~> (m :*: m)
 duplicateMT :: forall (m :: * -> *). Comonad m => m :~> (m :*: m)
duplicateMT = (forall a. m a -> (:*:) m m a) -> m :~> (m :*: m)
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (m (m a) -> (:*:) m m a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> (:*:) f g a
Matrix (m (m a) -> (:*:) m m a) -> (m a -> m (m a)) -> m a -> (:*:) m m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. m a -> m (m a)
forall a. m a -> m (m a)
forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate)
 joinMT :: (Monad m) => (m :*: m) :~> m
 joinMT :: forall (m :: * -> *). Monad m => (m :*: m) :~> m
joinMT = (forall a. (:*:) m m a -> m a) -> (m :*: m) :~> m
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (m (m a) -> m a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (m (m a) -> m a) -> ((:*:) m m a -> m (m a)) -> (:*:) m m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (:*:) m m a -> m (m a)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
(:*:) f g a -> f (g a)
cells)

 idTrans :: f :~> f
 idTrans :: forall k (a :: k -> *). a :~> a
idTrans = (forall (a :: k). f a -> f a) -> f :~> f
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans f a -> f a
forall (a :: k). f a -> f a
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

 unitTrans :: (Adjunction f g) => I :~> (g :*: f)
 unitTrans :: forall (f :: * -> *) (g :: * -> *).
Adjunction f g =>
I :~> (g :*: f)
unitTrans = (forall a. I a -> (:*:) g f a) -> I :~> (g :*: f)
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (\ (I a
x) -> g (f a) -> (:*:) g f a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> (:*:) f g a
Matrix (g (f a) -> (:*:) g f a) -> g (f a) -> (:*:) g f a
forall a b. (a -> b) -> a -> b
$ a -> g (f a)
forall a. a -> g (f a)
forall (f :: * -> *) (g :: * -> *) a.
Adjunction f g =>
a -> g (f a)
unit a
x)

 counitTrans :: (Adjunction f g) => (f :*: g) :~> I
 counitTrans :: forall (f :: * -> *) (g :: * -> *).
Adjunction f g =>
(f :*: g) :~> I
counitTrans = (forall a. (:*:) f g a -> I a) -> (f :*: g) :~> I
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (\ (Matrix f (g a)
f) -> a -> I a
forall a. a -> I a
I (a -> I a) -> a -> I a
forall a b. (a -> b) -> a -> b
$ f (g a) -> a
forall b. f (g b) -> b
forall (f :: * -> *) (g :: * -> *) b.
Adjunction f g =>
f (g b) -> b
counit f (g a)
f)

 vert :: g :~> h -> f :~> g -> f :~> h
 vert :: forall k (b :: k -> *) (c :: k -> *) (a :: k -> *).
(b :~> c) -> (a :~> b) -> a :~> c
vert (NatTrans forall (a :: k). g a -> h a
f) (NatTrans forall (a :: k). f a -> g a
g) = (forall (a :: k). f a -> h a) -> f :~> h
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (g a -> h a
forall (a :: k). g a -> h a
f (g a -> h a) -> (f a -> g a) -> f a -> h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f a -> g a
forall (a :: k). f a -> g a
g)

 horiz :: (Functor h) => h :~> k -> f :~> g -> (h :*: f) :~> (k :*: g)
 horiz :: forall {k1} (h :: * -> *) (k :: * -> *) (f :: k1 -> *)
       (g :: k1 -> *).
Functor h =>
(h :~> k) -> (f :~> g) -> (h :*: f) :~> (k :*: g)
horiz h :~> k
s f :~> g
t = (forall (a :: k1). (:*:) h f a -> (:*:) k g a)
-> (h :*: f) :~> (k :*: g)
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (k (g a) -> (:*:) k g a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> (:*:) f g a
Matrix (k (g a) -> (:*:) k g a)
-> ((:*:) h f a -> k (g a)) -> (:*:) h f a -> (:*:) k g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.  (h :~> k) -> forall a. h a -> k a
forall k (f :: k -> *) (g :: k -> *).
(f :~> g) -> forall (a :: k). f a -> g a
nattransComponent h :~> k
s (h (g a) -> k (g a))
-> ((:*:) h f a -> h (g a)) -> (:*:) h f a -> k (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (f a -> g a) -> h (f a) -> h (g a)
forall a b. (a -> b) -> h a -> h b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f :~> g) -> forall (a :: k1). f a -> g a
forall k (f :: k -> *) (g :: k -> *).
(f :~> g) -> forall (a :: k). f a -> g a
nattransComponent f :~> g
t) (h (f a) -> h (g a))
-> ((:*:) h f a -> h (f a)) -> (:*:) h f a -> h (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (:*:) h f a -> h (f a)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
(:*:) f g a -> f (g a)
cells)

 mapNaturalMatrix :: (Functor f, Functor h) 
            => f :~> g -> h :~> i -> (a -> b) -> (f :*: h) a -> (g :*: i) b
 mapNaturalMatrix :: forall (f :: * -> *) (h :: * -> *) (g :: * -> *) (i :: * -> *) a b.
(Functor f, Functor h) =>
(f :~> g) -> (h :~> i) -> (a -> b) -> (:*:) f h a -> (:*:) g i b
mapNaturalMatrix f :~> g
f h :~> i
g a -> b
t = ((f :*: i) :~> (g :*: i)) -> forall a. (:*:) f i a -> (:*:) g i a
forall k (f :: k -> *) (g :: k -> *).
(f :~> g) -> forall (a :: k). f a -> g a
nattransComponent ((f :~> g) -> (f :*: i) :~> (g :*: i)
forall {k} {k1} (f :: k -> *) (g :: k -> *) (h :: k1 -> k).
(f :~> g) -> (f :*: h) :~> (g :*: h)
mapColumns f :~> g
f)
                          ((:*:) f i b -> (:*:) g i b)
-> ((:*:) f h a -> (:*:) f i b) -> (:*:) f h a -> (:*:) g i b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((f :*: h) :~> (f :*: i)) -> forall a. (:*:) f h a -> (:*:) f i a
forall k (f :: k -> *) (g :: k -> *).
(f :~> g) -> forall (a :: k). f a -> g a
nattransComponent ((h :~> i) -> (f :*: h) :~> (f :*: i)
forall {k1} (h :: * -> *) (f :: k1 -> *) (g :: k1 -> *).
Functor h =>
(f :~> g) -> (h :*: f) :~> (h :*: g)
mapRows h :~> i
g)
                          ((:*:) f h b -> (:*:) f i b)
-> ((:*:) f h a -> (:*:) f h b) -> (:*:) f h a -> (:*:) f i b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> b) -> (:*:) f h a -> (:*:) f h b
forall a b. (a -> b) -> (:*:) f h a -> (:*:) f h b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
t

 data Day f g c = forall a b. Day ((a,b) -> c) (f a) (g b)

 convolve :: (Functor f, Functor g) => Day f g c -> (f :*: g) c
 convolve :: forall (f :: * -> *) (g :: * -> *) c.
(Functor f, Functor g) =>
Day f g c -> (:*:) f g c
convolve (Day (a, b) -> c
f f a
x g b
y) = (a -> b -> c) -> f a -> g b -> (:*:) f g c
forall (m :: * -> *) (n :: * -> *) a b c.
(Functor m, Functor n) =>
(a -> b -> c) -> m a -> n b -> (:*:) m n c
matrix (((a, b) -> c) -> a -> b -> c
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (a, b) -> c
f) f a
x g b
y

 convolveTrans :: (Functor f, Functor g) => Day f g :~> (f :*: g)
 convolveTrans :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Day f g :~> (f :*: g)
convolveTrans = (forall a. Day f g a -> (:*:) f g a) -> Day f g :~> (f :*: g)
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans Day f g a -> (:*:) f g a
forall a. Day f g a -> (:*:) f g a
forall (f :: * -> *) (g :: * -> *) c.
(Functor f, Functor g) =>
Day f g c -> (:*:) f g c
convolve

 mapRows :: (Functor h) => f :~> g -> (h :*: f) :~> (h :*: g)
 mapRows :: forall {k1} (h :: * -> *) (f :: k1 -> *) (g :: k1 -> *).
Functor h =>
(f :~> g) -> (h :*: f) :~> (h :*: g)
mapRows (NatTrans forall (a :: k1). f a -> g a
f) = (forall (a :: k1). (:*:) h f a -> (:*:) h g a)
-> (h :*: f) :~> (h :*: g)
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (h (g a) -> (:*:) h g a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> (:*:) f g a
Matrix (h (g a) -> (:*:) h g a)
-> ((:*:) h f a -> h (g a)) -> (:*:) h f a -> (:*:) h g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (f a -> g a) -> h (f a) -> h (g a)
forall a b. (a -> b) -> h a -> h b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> g a
forall (a :: k1). f a -> g a
f (h (f a) -> h (g a))
-> ((:*:) h f a -> h (f a)) -> (:*:) h f a -> h (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (:*:) h f a -> h (f a)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
(:*:) f g a -> f (g a)
cells)

 mapColumns :: f :~> g -> (f :*: h) :~> (g :*: h)
 mapColumns :: forall {k} {k1} (f :: k -> *) (g :: k -> *) (h :: k1 -> k).
(f :~> g) -> (f :*: h) :~> (g :*: h)
mapColumns (NatTrans forall (a :: k). f a -> g a
f) = (forall (a :: k1). (:*:) f h a -> (:*:) g h a)
-> (f :*: h) :~> (g :*: h)
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (g (h a) -> (:*:) g h a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> (:*:) f g a
Matrix (g (h a) -> (:*:) g h a)
-> ((:*:) f h a -> g (h a)) -> (:*:) f h a -> (:*:) g h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f (h a) -> g (h a)
forall (a :: k). f a -> g a
f (f (h a) -> g (h a))
-> ((:*:) f h a -> f (h a)) -> (:*:) f h a -> g (h a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (:*:) f h a -> f (h a)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
(:*:) f g a -> f (g a)
cells)

 mapMatrixNat :: (Functor f, Functor g)
  => f :~> f' -> g :~> g' -> (a -> b) -> (f :*: g) a -> (f' :*: g') b
 mapMatrixNat :: forall (f :: * -> *) (h :: * -> *) (g :: * -> *) (i :: * -> *) a b.
(Functor f, Functor h) =>
(f :~> g) -> (h :~> i) -> (a -> b) -> (:*:) f h a -> (:*:) g i b
mapMatrixNat f :~> f'
col g :~> g'
row a -> b
elem (:*:) f g a
m = (f :~> f'
col (f :~> f') -> (g :~> g') -> (f :*: g) :~> (f' :*: g')
forall {k1} (h :: * -> *) (k :: * -> *) (f :: k1 -> *)
       (g :: k1 -> *).
Functor h =>
(h :~> k) -> (f :~> g) -> (h :*: f) :~> (k :*: g)
`horiz` g :~> g'
row) ((f :*: g) :~> (f' :*: g'))
-> forall a. (:*:) f g a -> (:*:) f' g' a
forall k (f :: k -> *) (g :: k -> *).
(f :~> g) -> forall (a :: k). f a -> g a
`nattransComponent` ((a -> b) -> (:*:) f g a -> (:*:) f g b
forall a b. (a -> b) -> (:*:) f g a -> (:*:) f g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
elem (:*:) f g a
m)

 recMap :: (Functor f) =>  f :~> g -> Rec f -> Rec g
 recMap :: forall (f :: * -> *) (g :: * -> *).
Functor f =>
(f :~> g) -> Rec f -> Rec g
recMap f :~> g
z (In f (Rec f)
x) = g (Rec g) -> Rec g
forall (f :: * -> *). f (Rec f) -> Rec f
In (g (Rec g) -> Rec g) -> g (Rec g) -> Rec g
forall a b. (a -> b) -> a -> b
$ (f :~> g) -> forall a. f a -> g a
forall k (f :: k -> *) (g :: k -> *).
(f :~> g) -> forall (a :: k). f a -> g a
nattransComponent f :~> g
z (f (Rec g) -> g (Rec g)) -> f (Rec g) -> g (Rec g)
forall a b. (a -> b) -> a -> b
$ (Rec f -> Rec g) -> f (Rec f) -> f (Rec g)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f :~> g) -> Rec f -> Rec g
forall (f :: * -> *) (g :: * -> *).
Functor f =>
(f :~> g) -> Rec f -> Rec g
recMap f :~> g
z) f (Rec f)
x

 transformMap :: (Functor f, Functor g)
  => Coalgebra f a -> f :~> g -> Algebra g b -> a -> b
 transformMap :: forall (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
Coalgebra f a -> (f :~> g) -> Algebra g b -> a -> b
transformMap Coalgebra f a
divide f :~> g
f Algebra g b
combine = Algebra g b -> Rec g -> b
forall (f :: * -> *) a. Functor f => (f a -> a) -> Rec f -> a
fold Algebra g b
combine (Rec g -> b) -> (a -> Rec g) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (f :~> g) -> Rec f -> Rec g
forall (f :: * -> *) (g :: * -> *).
Functor f =>
(f :~> g) -> Rec f -> Rec g
recMap f :~> g
f (Rec f -> Rec g) -> (a -> Rec f) -> a -> Rec g
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coalgebra f a -> a -> Rec f
forall (f :: * -> *) a. Functor f => (a -> f a) -> a -> Rec f
unfold Coalgebra f a
divide

 tmap :: (InitialAlgebra f a, FinalCoalgebra g b) => f :~> g -> a -> b
 tmap :: forall (f :: * -> *) a (g :: * -> *) b.
(InitialAlgebra f a, FinalCoalgebra g b) =>
(f :~> g) -> a -> b
tmap f :~> g
f = Coalgebra f a -> (f :~> g) -> Algebra g b -> a -> b
forall (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
Coalgebra f a -> (f :~> g) -> Algebra g b -> a -> b
transformMap Coalgebra f a
forall (f :: * -> *) a. InitialAlgebra f a => a -> f a
unCreate f :~> g
f Algebra g b
forall (f :: * -> *) a. FinalCoalgebra f a => f a -> a
unDestroy

 tapp :: (Functor f) => f :~> g -> (a -> b) -> f a -> g b
 tapp :: forall (f :: * -> *) (g :: * -> *) a b.
Functor f =>
(f :~> g) -> (a -> b) -> f a -> g b
tapp (NatTrans forall a. f a -> g a
f) a -> b
g f a
x = f b -> g b
forall a. f a -> g a
f ((a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
g f a
x)

 unyoneda :: (Category cat) => cat a :~> f -> f a
 unyoneda :: forall {k} (cat :: k -> k -> *) (a :: k) (f :: k -> *).
Category cat =>
(cat a :~> f) -> f a
unyoneda (NatTrans forall (a :: k). cat a a -> f a
f) = cat a a -> f a
forall (a :: k). cat a a -> f a
f cat a a
forall (a :: k). cat a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

 yonedaFunction :: (Functor t) => t a -> (->) a :~> t
 yonedaFunction :: forall (t :: * -> *) a. Functor t => t a -> (->) a :~> t
yonedaFunction t a
f = (forall a. (a -> a) -> t a) -> (->) a :~> t
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (\a -> a
g -> (a -> a) -> t a -> t a
forall a b. (a -> b) -> t a -> t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
g t a
f)

 inverseHoriz :: (CoFunctor k) => f :~> k -> f' :~> k'
               -> (f :*: k') :~> (k :*: f')
 inverseHoriz :: forall {k1} (k :: * -> *) (f :: * -> *) (f' :: k1 -> *)
       (k' :: k1 -> *).
CoFunctor k =>
(f :~> k) -> (f' :~> k') -> (f :*: k') :~> (k :*: f')
inverseHoriz f :~> k
s f' :~> k'
t = (forall (a :: k1). (:*:) f k' a -> (:*:) k f' a)
-> (f :*: k') :~> (k :*: f')
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (k (f' a) -> (:*:) k f' a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> (:*:) f g a
Matrix (k (f' a) -> (:*:) k f' a)
-> ((:*:) f k' a -> k (f' a)) -> (:*:) f k' a -> (:*:) k f' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (f' a -> k' a) -> k (k' a) -> k (f' a)
forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage ((f' :~> k') -> forall (a :: k1). f' a -> k' a
forall k (f :: k -> *) (g :: k -> *).
(f :~> g) -> forall (a :: k). f a -> g a
nattransComponent f' :~> k'
t) (k (k' a) -> k (f' a))
-> ((:*:) f k' a -> k (k' a)) -> (:*:) f k' a -> k (f' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (f :~> k) -> forall a. f a -> k a
forall k (f :: k -> *) (g :: k -> *).
(f :~> g) -> forall (a :: k). f a -> g a
nattransComponent f :~> k
s (f (k' a) -> k (k' a))
-> ((:*:) f k' a -> f (k' a)) -> (:*:) f k' a -> k (k' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (:*:) f k' a -> f (k' a)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
(:*:) f g a -> f (g a)
cells)

 firstTrans :: (y -> x) -> (->) (x,d) :~> (->) (y,d)
 firstTrans :: forall y x d. (y -> x) -> (->) (x, d) :~> (->) (y, d)
firstTrans y -> x
g = (forall a. ((x, d) -> a) -> (y, d) -> a)
-> (->) (x, d) :~> (->) (y, d)
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (\ (x, d) -> a
f (y
y,d
d) -> (x, d) -> a
f (y -> x
g y
y,d
d))

 reverseList :: [] :~> []
 reverseList :: [] :~> []
reverseList = (forall a. [a] -> [a]) -> [] :~> []
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans [a] -> [a]
forall a. [a] -> [a]
reverse

 concatList :: ([] :*: []) :~> []
 concatList :: ([] :*: []) :~> []
concatList = (forall a. (:*:) [] [] a -> [a]) -> ([] :*: []) :~> []
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans ((forall a. (:*:) [] [] a -> [a]) -> ([] :*: []) :~> [])
-> (forall a. (:*:) [] [] a -> [a]) -> ([] :*: []) :~> []
forall a b. (a -> b) -> a -> b
$ [[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[a]] -> [a]) -> ((:*:) [] [] a -> [[a]]) -> (:*:) [] [] a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (:*:) [] [] a -> [[a]]
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
(:*:) f g a -> f (g a)
cells

 returnTrans :: (Monad m) => I :~> m
 returnTrans :: forall (m :: * -> *). Monad m => I :~> m
returnTrans = (forall a. I a -> m a) -> I :~> m
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> (I a -> a) -> I a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. I a -> a
forall a. I a -> a
unI)

 joinTrans :: (Monad m) => (m :*: m) :~> m
 joinTrans :: forall (m :: * -> *). Monad m => (m :*: m) :~> m
joinTrans = (forall a. (:*:) m m a -> m a) -> (m :*: m) :~> m
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (m (m a) -> m a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (m (m a) -> m a) -> ((:*:) m m a -> m (m a)) -> (:*:) m m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (:*:) m m a -> m (m a)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
(:*:) f g a -> f (g a)
cells)

 swapDimensions :: (Applicative g, Traversable f) => (f :*: g) :~> (g :*: f)
 swapDimensions :: forall (g :: * -> *) (f :: * -> *).
(Applicative g, Traversable f) =>
(f :*: g) :~> (g :*: f)
swapDimensions = (forall a. (:*:) f g a -> (:*:) g f a) -> (f :*: g) :~> (g :*: f)
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans (g (f a) -> (:*:) g f a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> (:*:) f g a
Matrix (g (f a) -> (:*:) g f a)
-> ((:*:) f g a -> g (f a)) -> (:*:) f g a -> (:*:) g f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f (g a) -> g (f a)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => f (f a) -> f (f a)
sequenceA (f (g a) -> g (f a))
-> ((:*:) f g a -> f (g a)) -> (:*:) f g a -> g (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (:*:) f g a -> f (g a)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
(:*:) f g a -> f (g a)
cells)

 data f :<~>: g = NaturalIso { forall {k} (f :: k -> *) (g :: k -> *). (f :<~>: g) -> f :~> g
fwdNaturalIso :: f :~> g,
                               forall {k} (f :: k -> *) (g :: k -> *). (f :<~>: g) -> g :~> f
bckNaturalIso :: g :~> f }

 instance Category (:<~>:) where
   id :: forall (a :: k -> *). a :<~>: a
id = (a :~> a) -> (a :~> a) -> a :<~>: a
forall {k} (f :: k -> *) (g :: k -> *).
(f :~> g) -> (g :~> f) -> f :<~>: g
NaturalIso a :~> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
forall (a :: k -> *). a :~> a
id a :~> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
forall (a :: k -> *). a :~> a
id
   (NaturalIso b :~> c
f c :~> b
g) . :: forall (b :: k -> *) (c :: k -> *) (a :: k -> *).
(b :<~>: c) -> (a :<~>: b) -> a :<~>: c
. (NaturalIso a :~> b
f' b :~> a
g') = (a :~> c) -> (c :~> a) -> a :<~>: c
forall {k} (f :: k -> *) (g :: k -> *).
(f :~> g) -> (g :~> f) -> f :<~>: g
NaturalIso (b :~> c
f (b :~> c) -> (a :~> b) -> a :~> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
forall (b :: k -> *) (c :: k -> *) (a :: k -> *).
(b :~> c) -> (a :~> b) -> a :~> c
. a :~> b
f') (b :~> a
g' (b :~> a) -> (c :~> b) -> c :~> a
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
forall (b :: k -> *) (c :: k -> *) (a :: k -> *).
(b :~> c) -> (a :~> b) -> a :~> c
. c :~> b
g)
 
 idIso :: f :<~>: f
 idIso :: forall k (a :: k -> *). a :<~>: a
idIso = (f :~> f) -> (f :~> f) -> f :<~>: f
forall {k} (f :: k -> *) (g :: k -> *).
(f :~> g) -> (g :~> f) -> f :<~>: g
NaturalIso f :~> f
forall k (a :: k -> *). a :~> a
idTrans f :~> f
forall k (a :: k -> *). a :~> a
idTrans

 symmetricIso :: g :<~>: f -> f :<~>: g
 symmetricIso :: forall {k} (g :: k -> *) (f :: k -> *). (g :<~>: f) -> f :<~>: g
symmetricIso (NaturalIso g :~> f
f f :~> g
g) = (f :~> g) -> (g :~> f) -> f :<~>: g
forall {k} (f :: k -> *) (g :: k -> *).
(f :~> g) -> (g :~> f) -> f :<~>: g
NaturalIso f :~> g
g g :~> f
f

 vertIso :: g :<~>: h -> f :<~>: g -> f :<~>: h
 vertIso :: forall k (b :: k -> *) (c :: k -> *) (a :: k -> *).
(b :<~>: c) -> (a :<~>: b) -> a :<~>: c
vertIso (NaturalIso g :~> h
x h :~> g
x') (NaturalIso f :~> g
y g :~> f
y')
    = (f :~> h) -> (h :~> f) -> f :<~>: h
forall {k} (f :: k -> *) (g :: k -> *).
(f :~> g) -> (g :~> f) -> f :<~>: g
NaturalIso (g :~> h
x (g :~> h) -> (f :~> g) -> f :~> h
forall k (b :: k -> *) (c :: k -> *) (a :: k -> *).
(b :~> c) -> (a :~> b) -> a :~> c
`vert` f :~> g
y) (g :~> f
y' (g :~> f) -> (h :~> g) -> h :~> f
forall k (b :: k -> *) (c :: k -> *) (a :: k -> *).
(b :~> c) -> (a :~> b) -> a :~> c
`vert` h :~> g
x')

 horizIso :: (Functor f, Functor f') => f :<~>: f' -> g :<~>: g' -> (f :*: g) :<~>: (f' :*: g')
 horizIso :: forall {k1} (f :: * -> *) (f' :: * -> *) (g :: k1 -> *)
       (g' :: k1 -> *).
(Functor f, Functor f') =>
(f :<~>: f') -> (g :<~>: g') -> (f :*: g) :<~>: (f' :*: g')
horizIso (NaturalIso f :~> f'
x f' :~> f
xinv) (NaturalIso g :~> g'
y g' :~> g
yinv) = ((f :*: g) :~> (f' :*: g'))
-> ((f' :*: g') :~> (f :*: g)) -> (f :*: g) :<~>: (f' :*: g')
forall {k} (f :: k -> *) (g :: k -> *).
(f :~> g) -> (g :~> f) -> f :<~>: g
NaturalIso (f :~> f'
x (f :~> f') -> (g :~> g') -> (f :*: g) :~> (f' :*: g')
forall {k1} (h :: * -> *) (k :: * -> *) (f :: k1 -> *)
       (g :: k1 -> *).
Functor h =>
(h :~> k) -> (f :~> g) -> (h :*: f) :~> (k :*: g)
`horiz` g :~> g'
y) (f' :~> f
xinv (f' :~> f) -> (g' :~> g) -> (f' :*: g') :~> (f :*: g)
forall {k1} (h :: * -> *) (k :: * -> *) (f :: k1 -> *)
       (g :: k1 -> *).
Functor h =>
(h :~> k) -> (f :~> g) -> (h :*: f) :~> (k :*: g)
`horiz` g' :~> g
yinv)
 
 isoMatrix :: (Functor g, Functor g') => f :<~>: (g :*: h) -> g :<~>: g' -> h :<~>: h' -> f :<~>: (g' :*: h')
 isoMatrix :: forall {k1} (g :: * -> *) (g' :: * -> *) (f :: k1 -> *)
       (h :: k1 -> *) (h' :: k1 -> *).
(Functor g, Functor g') =>
(f :<~>: (g :*: h))
-> (g :<~>: g') -> (h :<~>: h') -> f :<~>: (g' :*: h')
isoMatrix f :<~>: (g :*: h)
f g :<~>: g'
x h :<~>: h'
y = (g :<~>: g'
x (g :<~>: g') -> (h :<~>: h') -> (g :*: h) :<~>: (g' :*: h')
forall {k1} (f :: * -> *) (f' :: * -> *) (g :: k1 -> *)
       (g' :: k1 -> *).
(Functor f, Functor f') =>
(f :<~>: f') -> (g :<~>: g') -> (f :*: g) :<~>: (f' :*: g')
`horizIso` h :<~>: h'
y) ((g :*: h) :<~>: (g' :*: h'))
-> (f :<~>: (g :*: h)) -> f :<~>: (g' :*: h')
forall k (b :: k -> *) (c :: k -> *) (a :: k -> *).
(b :<~>: c) -> (a :<~>: b) -> a :<~>: c
`vertIso` f :<~>: (g :*: h)
f

 isoMatrix_ :: (Functor g') =>
  f :<~>: ((->) row :*: (->) col) -> (->) row :<~>: g' -> (->) col :<~>: h' -> f :<~>: (g' :*: h')
 isoMatrix_ :: forall (g' :: * -> *) (f :: * -> *) row col (h' :: * -> *).
Functor g' =>
(f :<~>: ((->) row :*: (->) col))
-> ((->) row :<~>: g')
-> ((->) col :<~>: h')
-> f :<~>: (g' :*: h')
isoMatrix_ f :<~>: ((->) row :*: (->) col)
f (->) row :<~>: g'
x (->) col :<~>: h'
y = ((->) row :<~>: g'
x ((->) row :<~>: g')
-> ((->) col :<~>: h') -> ((->) row :*: (->) col) :<~>: (g' :*: h')
forall {k1} (f :: * -> *) (f' :: * -> *) (g :: k1 -> *)
       (g' :: k1 -> *).
(Functor f, Functor f') =>
(f :<~>: f') -> (g :<~>: g') -> (f :*: g) :<~>: (f' :*: g')
`horizIso` (->) col :<~>: h'
y) (((->) row :*: (->) col) :<~>: (g' :*: h'))
-> (f :<~>: ((->) row :*: (->) col)) -> f :<~>: (g' :*: h')
forall k (b :: k -> *) (c :: k -> *) (a :: k -> *).
(b :<~>: c) -> (a :<~>: b) -> a :<~>: c
`vertIso` f :<~>: ((->) row :*: (->) col)
f

 outerIso :: (Functor g') => (->) row :<~>: g' -> (->) col :<~>: h'
       -> ((->) row :*: (->) col) :<~>: (g' :*: h')
 outerIso :: forall (g' :: * -> *) row col (h' :: * -> *).
Functor g' =>
((->) row :<~>: g')
-> ((->) col :<~>: h') -> ((->) row :*: (->) col) :<~>: (g' :*: h')
outerIso = (((->) row :*: (->) col) :<~>: ((->) row :*: (->) col))
-> ((->) row :<~>: g')
-> ((->) col :<~>: h')
-> ((->) row :*: (->) col) :<~>: (g' :*: h')
forall (g' :: * -> *) (f :: * -> *) row col (h' :: * -> *).
Functor g' =>
(f :<~>: ((->) row :*: (->) col))
-> ((->) row :<~>: g')
-> ((->) col :<~>: h')
-> f :<~>: (g' :*: h')
isoMatrix_ ((->) row :*: (->) col) :<~>: ((->) row :*: (->) col)
forall k (a :: k -> *). a :<~>: a
idIso

 matrixFrom :: (Functor g) => (row -> col -> a)
    -> ((->) row :<~>: g) -> ((->) col :<~>: h) -> (g :*: h) a
 matrixFrom :: forall (g :: * -> *) row col a (h :: * -> *).
Functor g =>
(row -> col -> a)
-> ((->) row :<~>: g) -> ((->) col :<~>: h) -> (:*:) g h a
matrixFrom row -> col -> a
f (->) row :<~>: g
a (->) col :<~>: h
b = (((->) row :*: (->) col) :<~>: (g :*: h))
-> (:*:) ((->) row) ((->) col) a :==: (:*:) g h a
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(f :<~>: g) -> f a :==: g a
runNaturalIso (((->) row :<~>: g)
-> ((->) col :<~>: h) -> ((->) row :*: (->) col) :<~>: (g :*: h)
forall (g' :: * -> *) row col (h' :: * -> *).
Functor g' =>
((->) row :<~>: g')
-> ((->) col :<~>: h') -> ((->) row :*: (->) col) :<~>: (g' :*: h')
outerIso (->) row :<~>: g
a (->) col :<~>: h
b) ((:*:) ((->) row) ((->) col) a :==: (:*:) g h a)
-> (:*:) ((->) row) ((->) col) a -> (:*:) g h a
forall a b. (a :==: b) -> a -> b
`runIso` ((row -> col -> a) -> (:*:) ((->) row) ((->) col) a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> (:*:) f g a
Matrix row -> col -> a
f)

 matrixIso :: (Functor f, Functor f', Functor g, Functor g')
  => f :<~>: f' -> g :<~>: g' -> a :==: b -> ((f :*: g) a) :==: ((f' :*: g') b)
 matrixIso :: forall (f :: * -> *) (f' :: * -> *) (g :: * -> *) (g' :: * -> *) a
       b.
(Functor f, Functor f', Functor g, Functor g') =>
(f :<~>: f')
-> (g :<~>: g') -> (a :==: b) -> (:*:) f g a :==: (:*:) f' g' b
matrixIso (NaturalIso f :~> f'
f f' :~> f
f') (NaturalIso g :~> g'
g g' :~> g
g') (Iso a -> b
x b -> a
x') =
    ((:*:) f g a -> (:*:) f' g' b)
-> ((:*:) f' g' b -> (:*:) f g a) -> (:*:) f g a :==: (:*:) f' g' b
forall a b. (a -> b) -> (b -> a) -> a :==: b
Iso ((f :~> f')
-> (g :~> g') -> (a -> b) -> (:*:) f g a -> (:*:) f' g' b
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) (i :: * -> *) a b.
(Functor f, Functor h) =>
(f :~> g) -> (h :~> i) -> (a -> b) -> (:*:) f h a -> (:*:) g i b
mapMatrixNat f :~> f'
f g :~> g'
g a -> b
x) ((f' :~> f)
-> (g' :~> g) -> (b -> a) -> (:*:) f' g' b -> (:*:) f g a
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) (i :: * -> *) a b.
(Functor f, Functor h) =>
(f :~> g) -> (h :~> i) -> (a -> b) -> (:*:) f h a -> (:*:) g i b
mapMatrixNat f' :~> f
f' g' :~> g
g' b -> a
x')


 swapDimensionsIso :: (Traversable f, Traversable g,
                         Applicative f, Applicative g)
                     => (f :*: g) :<~>: (g :*: f)
 swapDimensionsIso :: forall (f :: * -> *) (g :: * -> *).
(Traversable f, Traversable g, Applicative f, Applicative g) =>
(f :*: g) :<~>: (g :*: f)
swapDimensionsIso = ((f :*: g) :~> (g :*: f))
-> ((g :*: f) :~> (f :*: g)) -> (f :*: g) :<~>: (g :*: f)
forall {k} (f :: k -> *) (g :: k -> *).
(f :~> g) -> (g :~> f) -> f :<~>: g
NaturalIso (f :*: g) :~> (g :*: f)
forall (g :: * -> *) (f :: * -> *).
(Applicative g, Traversable f) =>
(f :*: g) :~> (g :*: f)
swapDimensions (g :*: f) :~> (f :*: g)
forall (g :: * -> *) (f :: * -> *).
(Applicative g, Traversable f) =>
(f :*: g) :~> (g :*: f)
swapDimensions

 runNaturalIso :: f :<~>: g -> f a :==: g a
 runNaturalIso :: forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(f :<~>: g) -> f a :==: g a
runNaturalIso (NaturalIso f :~> g
fwd g :~> f
bck) = (f :~> g) -> forall (a :: k). f a -> g a
forall k (f :: k -> *) (g :: k -> *).
(f :~> g) -> forall (a :: k). f a -> g a
nattransComponent f :~> g
fwd (f a -> g a) -> (g a -> f a) -> f a :==: g a
forall a b. (a -> b) -> (b -> a) -> a :==: b
forall (arr :: * -> * -> *) a b.
BiArrow arr =>
(a -> b) -> (b -> a) -> arr a b
<-> (g :~> f) -> forall (a :: k). g a -> f a
forall k (f :: k -> *) (g :: k -> *).
(f :~> g) -> forall (a :: k). f a -> g a
nattransComponent g :~> f
bck


 newtype (f :~~> g) a = NaturalTrans { forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(:~~>) f g a -> f a -> g a
unNatTrans :: f a -> g a }


  -- matrix_map :: (f :*: h) (a -> b)
  --            -> (f :*: h) a -> (g :*: i) b
  -- matrix_map (Matrix f) (Matrix x) = unNatTrans f x
  --
  -- map_map :: (f :~~> g) ((h :~~> i) (a -> b)) -> f (h a) -> g (i b)
  --
  -- mapmatrix :: (Applicative f) => 
  --         f ((g :~~> h) a)
  --      -> (f :~~> i) (h a)
  --      -> (f :*: g) a
  --      -> (i :*: h) a
  --
  -- mapmatrix :: (Applicative f) => ((f :~~> i) :*: h) a
  --                              -> (f :*: (g :~~> h)) a
  --                              -> (f :*: g) a
  --                              -> (i :*: h) a

 transformMatrix :: (Applicative f') => ((f :~~> f') :*: g) a
                              -> (f' :*: (g :~~> g')) a
                              -> (f  :*: g) a
                              -> (f' :*: g') a
 transformMatrix :: forall {k1} (f' :: * -> *) (f :: * -> *) (g :: k1 -> *) (a :: k1)
       (g' :: k1 -> *).
Applicative f' =>
(:*:) (f :~~> f') g a
-> (:*:) f' (g :~~> g') a -> (:*:) f g a -> (:*:) f' g' a
transformMatrix (Matrix (:~~>) f f' (g a)
u) (Matrix f' ((:~~>) g g' a)
t)  (Matrix f (g a)
x) = f' (g' a) -> (:*:) f' g' a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> (:*:) f g a
Matrix (f' (g' a) -> (:*:) f' g' a) -> f' (g' a) -> (:*:) f' g' a
forall a b. (a -> b) -> a -> b
$ ((:~~>) g g' a -> g a -> g' a) -> f' ((:~~>) g g' a -> g a -> g' a)
forall a. a -> f' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (:~~>) g g' a -> g a -> g' a
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(:~~>) f g a -> f a -> g a
unNatTrans f' ((:~~>) g g' a -> g a -> g' a)
-> f' ((:~~>) g g' a) -> f' (g a -> g' a)
forall a b. f' (a -> b) -> f' a -> f' b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f' ((:~~>) g g' a)
t f' (g a -> g' a) -> f' (g a) -> f' (g' a)
forall a b. f' (a -> b) -> f' a -> f' b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (:~~>) f f' (g a) -> f (g a) -> f' (g a)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(:~~>) f g a -> f a -> g a
unNatTrans (:~~>) f f' (g a)
u f (g a)
x

 newtype NaturalTransA (arr :: k -> k -> Type) f g a = NaturalTransA { forall {k} k (arr :: k -> k -> *) (f :: k -> k) (g :: k -> k)
       (a :: k).
NaturalTransA arr f g a -> arr (f a) (g a)
unNatTransA :: arr (f a) (g a) }
 newtype NatTransA (arr :: k -> k -> Type) f g = NatTransA { forall {k} k (arr :: k -> k -> *) (f :: k -> k) (g :: k -> k).
NatTransA arr f g -> forall (a :: k). arr (f a) (g a)
nattransComponentA :: forall a. arr (f a) (g a) }

 instance (Category arr) => Category (NatTransA arr) where
   id :: forall (a :: k -> k). NatTransA arr a a
id = (forall (a :: k). arr (a a) (a a)) -> NatTransA arr a a
forall {k} k (arr :: k -> k -> *) (f :: k -> k) (g :: k -> k).
(forall (a :: k). arr (f a) (g a)) -> NatTransA arr f g
NatTransA arr (a a) (a a)
forall (a :: k). arr a a
forall (a :: k). arr (a a) (a a)
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
   (NatTransA forall (a :: k). arr (b a) (c a)
f) . :: forall (b :: k -> k) (c :: k -> k) (a :: k -> k).
NatTransA arr b c -> NatTransA arr a b -> NatTransA arr a c
. (NatTransA forall (a :: k). arr (a a) (b a)
g) = (forall (a :: k). arr (a a) (c a)) -> NatTransA arr a c
forall {k} k (arr :: k -> k -> *) (f :: k -> k) (g :: k -> k).
(forall (a :: k). arr (f a) (g a)) -> NatTransA arr f g
NatTransA (arr (b a) (c a)
forall (a :: k). arr (b a) (c a)
f arr (b a) (c a) -> arr (a a) (b a) -> arr (a a) (c a)
forall (b :: k) (c :: k) (a :: k). arr b c -> arr a b -> arr a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. arr (a a) (b a)
forall (a :: k). arr (a a) (b a)
g)

 idTransA :: (Arrow arr) => NatTransA arr f f
 idTransA :: forall {k} (arr :: * -> * -> *) (f :: k -> *).
Arrow arr =>
NatTransA arr f f
idTransA = (forall (a :: k). arr (f a) (f a)) -> NatTransA arr f f
forall {k} k (arr :: k -> k -> *) (f :: k -> k) (g :: k -> k).
(forall (a :: k). arr (f a) (g a)) -> NatTransA arr f g
NatTransA arr (f a) (f a)
forall (a :: k). arr (f a) (f a)
forall (a :: * -> * -> *) b. Arrow a => a b b
returnA

 horizA :: (Arrow arr,FunctorArrow k arr arr) => NatTransA arr h k -> NatTransA arr f g -> NatTransA arr (h :*: f) (k :*: g)
 horizA :: forall {k1} (arr :: * -> * -> *) (k :: * -> *) (h :: * -> *)
       (f :: k1 -> *) (g :: k1 -> *).
(Arrow arr, FunctorArrow k arr arr) =>
NatTransA arr h k
-> NatTransA arr f g -> NatTransA arr (h :*: f) (k :*: g)
horizA NatTransA arr h k
s NatTransA arr f g
t = (forall (a :: k1). arr ((:*:) h f a) ((:*:) k g a))
-> NatTransA arr (h :*: f) (k :*: g)
forall {k} k (arr :: k -> k -> *) (f :: k -> k) (g :: k -> k).
(forall (a :: k). arr (f a) (g a)) -> NatTransA arr f g
NatTransA ((k (g a) -> (:*:) k g a) -> arr (k (g a)) ((:*:) k g a)
forall b c. (b -> c) -> arr b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr k (g a) -> (:*:) k g a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> (:*:) f g a
Matrix arr (k (g a)) ((:*:) k g a)
-> arr ((:*:) h f a) (k (g a)) -> arr ((:*:) h f a) ((:*:) k g a)
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
<<< arr (f a) (g a) -> arr (k (f a)) (k (g a))
forall c d. arr c d -> arr (k c) (k d)
forall {k} {k1} (f :: k -> k1) (arr :: k -> k -> *)
       (arr' :: k1 -> k1 -> *) (c :: k) (d :: k).
FunctorArrow f arr arr' =>
arr c d -> arr' (f c) (f d)
amap (NatTransA arr f g -> forall (a :: k1). arr (f a) (g a)
forall {k} k (arr :: k -> k -> *) (f :: k -> k) (g :: k -> k).
NatTransA arr f g -> forall (a :: k). arr (f a) (g a)
nattransComponentA NatTransA arr f g
t) arr (k (f a)) (k (g a))
-> arr ((:*:) h f a) (k (f a)) -> arr ((:*:) h f a) (k (g a))
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
<<< NatTransA arr h k -> forall a. arr (h a) (k a)
forall {k} k (arr :: k -> k -> *) (f :: k -> k) (g :: k -> k).
NatTransA arr f g -> forall (a :: k). arr (f a) (g a)
nattransComponentA NatTransA arr h k
s arr (h (f a)) (k (f a))
-> arr ((:*:) h f a) (h (f a)) -> arr ((:*:) h f a) (k (f a))
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
<<< ((:*:) h f a -> h (f a)) -> arr ((:*:) h f a) (h (f a))
forall b c. (b -> c) -> arr b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (:*:) h f a -> h (f a)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
(:*:) f g a -> f (g a)
cells)

 vertA :: (Arrow arr) => NatTransA arr g h -> NatTransA arr f g -> NatTransA arr f h
 vertA :: forall {k} (arr :: * -> * -> *) (g :: k -> *) (h :: k -> *)
       (f :: k -> *).
Arrow arr =>
NatTransA arr g h -> NatTransA arr f g -> NatTransA arr f h
vertA (NatTransA forall (a :: k). arr (g a) (h a)
f) (NatTransA forall (a :: k). arr (f a) (g a)
g) = (forall (a :: k). arr (f a) (h a)) -> NatTransA arr f h
forall {k} k (arr :: k -> k -> *) (f :: k -> k) (g :: k -> k).
(forall (a :: k). arr (f a) (g a)) -> NatTransA arr f g
NatTransA (arr (g a) (h a)
forall (a :: k). arr (g a) (h a)
f arr (g a) (h a) -> arr (f a) (g a) -> arr (f a) (h a)
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
<<< arr (f a) (g a)
forall (a :: k). arr (f a) (g a)
g)

 invertNatTransA :: NatTransA arr f g -> NatTransA (OpA arr) g f
 invertNatTransA :: forall {k} {k} (arr :: k -> k -> *) (f :: k -> k) (g :: k -> k).
NatTransA arr f g -> NatTransA (OpA arr) g f
invertNatTransA (NatTransA forall (a :: k). arr (f a) (g a)
f) = (forall (a :: k). OpA arr (g a) (f a)) -> NatTransA (OpA arr) g f
forall {k} k (arr :: k -> k -> *) (f :: k -> k) (g :: k -> k).
(forall (a :: k). arr (f a) (g a)) -> NatTransA arr f g
NatTransA (arr (f a) (g a) -> OpA arr (g a) (f a)
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k1) (b :: k).
arr b a -> OpA arr a b
OpA arr (f a) (g a)
forall (a :: k). arr (f a) (g a)
f)

 -- | For exposition of coyonedaA, see Bartosz Milewski's youtube videos
 -- https://www.youtube.com/watch?v=p_ydgYm9-yg

 coyonedaA :: (Category cat, ArrowApply arr, ArrowChoice arr)
  => arr (NatTransA arr (OpA cat a) f) (f a)
 coyonedaA :: forall {k} (cat :: k -> k -> *) (arr :: * -> * -> *) (a :: k)
       (f :: k -> *).
(Category cat, ArrowApply arr, ArrowChoice arr) =>
arr (NatTransA arr (OpA cat a) f) (f a)
coyonedaA = proc NatTransA arr (OpA cat a) f
z -> case NatTransA arr (OpA cat a) f
z of { (NatTransA forall (a :: k). arr (OpA cat a a) (f a)
f) -> arr (OpA cat a a) (f a)
forall (a :: k). arr (OpA cat a a) (f a)
f -<< OpA cat a a
forall (a :: k). OpA cat a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id }

  -- uncoyoneda f = NatTransA $ proc x -> inverseImageA x -<< f

 unyonedaA :: (Category cat, ArrowApply arr) => arr (NatTransA arr (cat a) f) (f a)
 unyonedaA :: forall {k} (cat :: k -> k -> *) (arr :: * -> * -> *) (a :: k)
       (f :: k -> *).
(Category cat, ArrowApply arr) =>
arr (NatTransA arr (cat a) f) (f a)
unyonedaA = proc (NatTransA forall (a :: k). arr (cat a a) (f a)
f) -> arr (cat a a) (f a)
forall (a :: k). arr (cat a a) (f a)
f -<< cat a a
forall (a :: k). cat a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

 yonedaA :: (FunctorArrow f arr arr, ArrowApply arr) => f c -> NatTransA arr (arr c) f
 yonedaA :: forall (f :: * -> *) (arr :: * -> * -> *) c.
(FunctorArrow f arr arr, ArrowApply arr) =>
f c -> NatTransA arr (arr c) f
yonedaA f c
f = (forall a. arr (arr c a) (f a)) -> NatTransA arr (arr c) f
forall {k} k (arr :: k -> k -> *) (f :: k -> k) (g :: k -> k).
(forall (a :: k). arr (f a) (g a)) -> NatTransA arr f g
NatTransA (proc arr c a
g -> arr c a -> arr (f c) (f a)
forall c d. arr c d -> arr (f c) (f d)
forall {k} {k1} (f :: k -> k1) (arr :: k -> k -> *)
       (arr' :: k1 -> k1 -> *) (c :: k) (d :: k).
FunctorArrow f arr arr' =>
arr c d -> arr' (f c) (f d)
amap arr c a
g -<< f c
f)

 natTransToA :: f :~> g -> NatTransA (->) f g
 natTransToA :: forall {k} (f :: k -> *) (g :: k -> *).
(f :~> g) -> NatTransA (->) f g
natTransToA (NatTrans forall (a :: k). f a -> g a
f) = (forall (a :: k). f a -> g a) -> NatTransA (->) f g
forall {k} k (arr :: k -> k -> *) (f :: k -> k) (g :: k -> k).
(forall (a :: k). arr (f a) (g a)) -> NatTransA arr f g
NatTransA f a -> g a
forall (a :: k). f a -> g a
f

 arrowNatTrans :: NatTransA (->) f g -> f :~> g
 arrowNatTrans :: forall {k} (f :: k -> *) (g :: k -> *).
NatTransA (->) f g -> f :~> g
arrowNatTrans (NatTransA forall (a :: k). f a -> g a
f) = (forall (a :: k). f a -> g a) -> f :~> g
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> f :~> g
NatTrans f a -> g a
forall (a :: k). f a -> g a
f