{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Algebra.Category.NatTrans where

import Algebra.Category
import Prelude (Functor(..))
import Algebra.Types

import Data.Kind

newtype NatTrans (f :: Type -> Type) (g :: Type -> Type) = NatTrans (forall x. f x -> g x)

instance Category NatTrans where
  type Obj NatTrans = Functor
  NatTrans forall x. b x -> c x
f . :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *).
(Obj NatTrans a, Obj NatTrans b, Obj NatTrans c) =>
NatTrans b c -> NatTrans a b -> NatTrans a c
. NatTrans forall x. a x -> b x
g = (forall x. a x -> c x) -> NatTrans a c
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans (b x -> c x
forall x. b x -> c x
f (b x -> c x) -> (a x -> b x) -> a x -> c x
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k)
       (con :: k -> Constraint).
(Category cat, con ~ Obj cat, con a, con b, con c) =>
cat b c -> cat a b -> cat a c
∘ a x -> b x
forall x. a x -> b x
g)
  id :: forall (a :: * -> *). Obj NatTrans a => NatTrans a a
id = (forall x. a x -> a x) -> NatTrans a a
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans a x -> a x
forall x. a x -> a x
forall a. Obj (->) a => a -> a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id

instance Monoidal (∘) Id NatTrans where
  assoc_ :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *).
(Obj NatTrans a, Obj NatTrans b, Obj NatTrans c) =>
NatTrans (a ∘ (b ∘ c)) ((a ∘ b) ∘ c)
assoc_ = (forall x. (∘) a (b ∘ c) x -> (∘) (a ∘ b) c x)
-> NatTrans (a ∘ (b ∘ c)) ((a ∘ b) ∘ c)
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans ((∘) a b (c x) -> (∘) (a ∘ b) c x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (x :: k1).
f (g x) -> (∘) f g x
Comp ((∘) a b (c x) -> (∘) (a ∘ b) c x)
-> ((∘) a (b ∘ c) x -> (∘) a b (c x))
-> (∘) a (b ∘ c) x
-> (∘) (a ∘ b) c x
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. a (b (c x)) -> (∘) a b (c x)
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (x :: k1).
f (g x) -> (∘) f g x
Comp (a (b (c x)) -> (∘) a b (c x))
-> ((∘) a (b ∘ c) x -> a (b (c x)))
-> (∘) a (b ∘ c) x
-> (∘) a b (c x)
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. ((∘) b c x -> b (c x)) -> a ((∘) b c x) -> a (b (c x))
forall a b. (a -> b) -> a a -> a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (∘) b c x -> b (c x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (x :: k2).
(∘) f g x -> f (g x)
fromComp (a ((∘) b c x) -> a (b (c x)))
-> ((∘) a (b ∘ c) x -> a ((∘) b c x))
-> (∘) a (b ∘ c) x
-> a (b (c x))
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. (∘) a (b ∘ c) x -> a ((∘) b c x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (x :: k2).
(∘) f g x -> f (g x)
fromComp)
  unitorR_ :: forall (a :: * -> *).
(Obj NatTrans a, Obj NatTrans Id) =>
NatTrans (a ∘ Id) a
unitorR_ = (forall x. (∘) a Id x -> a x) -> NatTrans (a ∘ Id) a
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans ((Id x -> x) -> a (Id x) -> a x
forall a b. (a -> b) -> a a -> a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Id x -> x
forall x. Id x -> x
fromId (a (Id x) -> a x) -> ((∘) a Id x -> a (Id x)) -> (∘) a Id x -> a x
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. (∘) a Id x -> a (Id x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (x :: k2).
(∘) f g x -> f (g x)
fromComp)
  NatTrans forall x. a x -> b x
f ⊗ :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *) (d :: * -> *).
(Obj NatTrans a, Obj NatTrans b, Obj NatTrans c, Obj NatTrans d) =>
NatTrans a b -> NatTrans c d -> NatTrans (a ∘ c) (b ∘ d)
⊗ NatTrans forall x. c x -> d x
g = (forall x. (∘) a c x -> (∘) b d x) -> NatTrans (a ∘ c) (b ∘ d)
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans (b (d x) -> (∘) b d x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (x :: k1).
f (g x) -> (∘) f g x
Comp (b (d x) -> (∘) b d x)
-> ((∘) a c x -> b (d x)) -> (∘) a c x -> (∘) b d x
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. a (d x) -> b (d x)
forall x. a x -> b x
f (a (d x) -> b (d x))
-> ((∘) a c x -> a (d x)) -> (∘) a c x -> b (d x)
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. (c x -> d x) -> a (c x) -> a (d x)
forall a b. (a -> b) -> a a -> a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c x -> d x
forall x. c x -> d x
g (a (c x) -> a (d x))
-> ((∘) a c x -> a (c x)) -> (∘) a c x -> a (d x)
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. (∘) a c x -> a (c x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (x :: k2).
(∘) f g x -> f (g x)
fromComp)
  assoc :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *).
(Obj NatTrans a, Obj NatTrans b, Obj NatTrans c) =>
NatTrans ((a ∘ b) ∘ c) (a ∘ (b ∘ c))
assoc =  (forall x. (∘) (a ∘ b) c x -> (∘) a (b ∘ c) x)
-> NatTrans ((a ∘ b) ∘ c) (a ∘ (b ∘ c))
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans (a ((∘) b c x) -> (∘) a (b ∘ c) x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (x :: k1).
f (g x) -> (∘) f g x
Comp (a ((∘) b c x) -> (∘) a (b ∘ c) x)
-> ((∘) (a ∘ b) c x -> a ((∘) b c x))
-> (∘) (a ∘ b) c x
-> (∘) a (b ∘ c) x
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. (b (c x) -> (∘) b c x) -> a (b (c x)) -> a ((∘) b c x)
forall a b. (a -> b) -> a a -> a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b (c x) -> (∘) b c x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (x :: k1).
f (g x) -> (∘) f g x
Comp (a (b (c x)) -> a ((∘) b c x))
-> ((∘) (a ∘ b) c x -> a (b (c x)))
-> (∘) (a ∘ b) c x
-> a ((∘) b c x)
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. (∘) a b (c x) -> a (b (c x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (x :: k2).
(∘) f g x -> f (g x)
fromComp ((∘) a b (c x) -> a (b (c x)))
-> ((∘) (a ∘ b) c x -> (∘) a b (c x))
-> (∘) (a ∘ b) c x
-> a (b (c x))
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. (∘) (a ∘ b) c x -> (∘) a b (c x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (x :: k2).
(∘) f g x -> f (g x)
fromComp)
  unitorR :: forall (a :: * -> *).
(Obj NatTrans a, Obj NatTrans Id) =>
NatTrans a (a ∘ Id)
unitorR = (forall x. a x -> (∘) a Id x) -> NatTrans a (a ∘ Id)
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans (a (Id x) -> (∘) a Id x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (x :: k1).
f (g x) -> (∘) f g x
Comp (a (Id x) -> (∘) a Id x) -> (a x -> a (Id x)) -> a x -> (∘) a Id x
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. (x -> Id x) -> a x -> a (Id x)
forall a b. (a -> b) -> a a -> a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> Id x
forall x. x -> Id x
Id)
  unitorL :: forall (a :: * -> *).
(Obj NatTrans a, Obj NatTrans Id) =>
NatTrans a (Id ∘ a)
unitorL = (forall x. a x -> (∘) Id a x) -> NatTrans a (Id ∘ a)
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans (Id (a x) -> (∘) Id a x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (x :: k1).
f (g x) -> (∘) f g x
Comp (Id (a x) -> (∘) Id a x) -> (a x -> Id (a x)) -> a x -> (∘) Id a x
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. a x -> Id (a x)
forall x. x -> Id x
Id)
  unitorL_ :: forall (a :: * -> *).
(Obj NatTrans a, Obj NatTrans Id) =>
NatTrans (Id ∘ a) a
unitorL_ = (forall x. (∘) Id a x -> a x) -> NatTrans (Id ∘ a) a
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans (Id (a x) -> a x
forall x. Id x -> x
fromId (Id (a x) -> a x) -> ((∘) Id a x -> Id (a x)) -> (∘) Id a x -> a x
forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. (∘) Id a x -> Id (a x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (x :: k2).
(∘) f g x -> f (g x)
fromComp)

instance Monoidal (⊗) One NatTrans where
  assoc :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *).
(Obj NatTrans a, Obj NatTrans b, Obj NatTrans c) =>
NatTrans ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc = (forall x. (⊗) (a ⊗ b) c x -> (⊗) a (b ⊗ c) x)
-> NatTrans ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans (\(FunctorProd (FunctorProd a x
x b x
y) c x
z) -> a x -> (⊗) b c x -> (⊗) a (b ⊗ c) x
forall (f :: * -> *) (g :: * -> *) x. f x -> g x -> (⊗) f g x
FunctorProd a x
x (b x -> c x -> (⊗) b c x
forall (f :: * -> *) (g :: * -> *) x. f x -> g x -> (⊗) f g x
FunctorProd b x
y c x
z))
  assoc_ :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *).
(Obj NatTrans a, Obj NatTrans b, Obj NatTrans c) =>
NatTrans (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc_ = (forall x. (⊗) a (b ⊗ c) x -> (⊗) (a ⊗ b) c x)
-> NatTrans (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans (\(FunctorProd a x
x (FunctorProd b x
y c x
z)) -> ((⊗) a b x -> c x -> (⊗) (a ⊗ b) c x
forall (f :: * -> *) (g :: * -> *) x. f x -> g x -> (⊗) f g x
FunctorProd (a x -> b x -> (⊗) a b x
forall (f :: * -> *) (g :: * -> *) x. f x -> g x -> (⊗) f g x
FunctorProd a x
x b x
y) c x
z))
  unitorR :: forall (a :: * -> *).
(Obj NatTrans a, Obj NatTrans One) =>
NatTrans a (a ⊗ One)
unitorR = (forall x. a x -> (⊗) a One x) -> NatTrans a (a ⊗ One)
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans (\a x
x -> a x -> One x -> (⊗) a One x
forall (f :: * -> *) (g :: * -> *) x. f x -> g x -> (⊗) f g x
FunctorProd a x
x One x
forall x. One x
FunctorOne)
  unitorR_ :: forall (a :: * -> *).
(Obj NatTrans a, Obj NatTrans One) =>
NatTrans (a ⊗ One) a
unitorR_ = (forall x. (⊗) a One x -> a x) -> NatTrans (a ⊗ One) a
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans (\(FunctorProd a x
x One x
_) -> a x
x)
  unitorL :: forall (a :: * -> *).
(Obj NatTrans a, Obj NatTrans One) =>
NatTrans a (One ⊗ a)
unitorL = (forall x. a x -> (⊗) One a x) -> NatTrans a (One ⊗ a)
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans (One x -> a x -> (⊗) One a x
forall (f :: * -> *) (g :: * -> *) x. f x -> g x -> (⊗) f g x
FunctorProd One x
forall x. One x
FunctorOne)
  unitorL_ :: forall (a :: * -> *).
(Obj NatTrans a, Obj NatTrans One) =>
NatTrans (One ⊗ a) a
unitorL_ = (forall x. (⊗) One a x -> a x) -> NatTrans (One ⊗ a) a
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans (\(FunctorProd One x
_ a x
x) -> a x
x)
  NatTrans forall x. a x -> b x
f ⊗ :: forall (a :: * -> *) (b :: * -> *) (c :: * -> *) (d :: * -> *).
(Obj NatTrans a, Obj NatTrans b, Obj NatTrans c, Obj NatTrans d) =>
NatTrans a b -> NatTrans c d -> NatTrans (a ⊗ c) (b ⊗ d)
⊗ NatTrans forall x. c x -> d x
g = (forall x. (⊗) a c x -> (⊗) b d x) -> NatTrans (a ⊗ c) (b ⊗ d)
forall (f :: * -> *) (g :: * -> *).
(forall x. f x -> g x) -> NatTrans f g
NatTrans (\(FunctorProd a x
x c x
y) ->  b x -> d x -> (⊗) b d x
forall (f :: * -> *) (g :: * -> *) x. f x -> g x -> (⊗) f g x
FunctorProd (a x -> b x
forall x. a x -> b x
f a x
x) (c x -> d x
forall x. c x -> d x
g c x
y))