{-# LANGUAGE MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : Given two categories C and D, the `FunctorCategory` D^C has as objects functors from C to D and as morphisms natural transformations between functors.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Given two categories C and D, the `FunctorCategory` D^C has as objects functors from C to D and as morphisms natural transformations between functors.
-}

module FunctorCategory.FunctorCategory
(
    NaturalTransformation(..),
    preWhiskering,
    postWhiskering,
    FunctorCategory(..)
)
where
    import FiniteCategory.FiniteCategory
    import Diagram.Diagram
    import Data.List                               (intercalate)
    import Utils.EnumerateMaps
    import Utils.CartesianProduct
    import Data.Maybe                              (isJust, fromJust)
    import IO.PrettyPrint
    import IO.Show
    import Utils.AssociationList
    
    -- | A `NaturalTransformation` between two heterogeneous functors from /C/ to /D/ is a mapping from objects of /C/ to morphism of /D/ such that naturality is respected.

    --

    -- Formally, let /F/ and /G/ be functors, and eta : Ob(/C/) -> Ar(/D/). The following property should be respected :

    --

    -- prop> source F = source G

    -- prop> target F = target G

    -- prop> Forall f in arrows (source F) : eta(target f) @ F(f) = G(f) @ eta(source f)

    data NaturalTransformation c1 m1 o1 c2 m2 o2 = NaturalTransformation {forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT :: Diagram c1 m1 o1 c2 m2 o2
                                                                        , forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT :: Diagram c1 m1 o1 c2 m2 o2
                                                                        , forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component :: o1 -> m2}
    
    instance   (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => 
                Morphism (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) where
        @ :: NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
(@) NaturalTransformation{srcNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
s2,tgtNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
t2,component :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component=o1 -> m2
c2} NaturalTransformation{srcNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
s1,tgtNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
t1,component :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component=o1 -> m2
c1}
            | Diagram c1 m1 o1 c2 m2 o2
t1 Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= Diagram c1 m1 o1 c2 m2 o2
s2 = [Char] -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall a. HasCallStack => [Char] -> a
error [Char]
"Illegal composition of natural transformations"
            | Bool
otherwise = NaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> (o1 -> m2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
NaturalTransformation{srcNT :: Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
s1,tgtNT :: Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
t2,component :: o1 -> m2
component=(\o1
x -> (o1 -> m2
c2 o1
x) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ (o1 -> m2
c1 o1
x))}
        source :: NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
source = NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT
        target :: NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
target = NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT
        
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
              Eq (NaturalTransformation c1 m1 o1 c2 m2 o2) where
        NaturalTransformation{srcNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
s1,tgtNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
t1,component :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component=o1 -> m2
c1} == :: NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool
== NaturalTransformation{srcNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
s2,tgtNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
t2,component :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component=o1 -> m2
c2}
            | Diagram c1 m1 o1 c2 m2 o2
s1 Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= Diagram c1 m1 o1 c2 m2 o2
s2 = Bool
False
            | Diagram c1 m1 o1 c2 m2 o2
t1 Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= Diagram c1 m1 o1 c2 m2 o2
t2 = Bool
False
            | Bool
otherwise = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [o1 -> m2
c1 o1
o m2 -> m2 -> Bool
forall a. Eq a => a -> a -> Bool
== o1 -> m2
c2 o1
o | o1
o <- (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob(c1 -> [o1])
-> (Diagram c1 m1 o1 c2 m2 o2 -> c1)
-> Diagram c1 m1 o1 c2 m2 o2
-> [o1]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src) Diagram c1 m1 o1 c2 m2 o2
s1]
            
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Show c1, Show m1, Show o1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Show c2, Show m2, Show o2) =>
              Show (NaturalTransformation c1 m1 o1 c2 m2 o2) where
        show :: NaturalTransformation c1 m1 o1 c2 m2 o2 -> [Char]
show NaturalTransformation{srcNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
s,tgtNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
t,component :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component=o1 -> m2
c} = [Char]
"NaturalTransformation{srcNT = "[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++Diagram c1 m1 o1 c2 m2 o2 -> [Char]
forall a. Show a => a -> [Char]
show Diagram c1 m1 o1 c2 m2 o2
s[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
", tgtNT = "[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++Diagram c1 m1 o1 c2 m2 o2 -> [Char]
forall a. Show a => a -> [Char]
show Diagram c1 m1 o1 c2 m2 o2
t[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
", component = "[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++(o1 -> m2) -> [o1] -> [Char]
forall a b. (Show a, Show b) => (a -> b) -> [a] -> [Char]
showFunction o1 -> m2
c ((c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob(c1 -> [o1])
-> (Diagram c1 m1 o1 c2 m2 o2 -> c1)
-> Diagram c1 m1 o1 c2 m2 o2
-> [o1]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src) Diagram c1 m1 o1 c2 m2 o2
s)[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
"}"
           
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, PrettyPrintable c1, PrettyPrintable m1, PrettyPrintable o1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, PrettyPrintable c2, PrettyPrintable m2, PrettyPrintable o2) =>
              PrettyPrintable (NaturalTransformation c1 m1 o1 c2 m2 o2) where
        pprint :: NaturalTransformation c1 m1 o1 c2 m2 o2 -> [Char]
pprint NaturalTransformation{srcNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
s,tgtNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
t,component :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component=o1 -> m2
c} = [Char]
"Nat : "[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++Diagram c1 m1 o1 c2 m2 o2 -> [Char]
forall a. PrettyPrintable a => a -> [Char]
pprint Diagram c1 m1 o1 c2 m2 o2
s[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
" -> "[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++Diagram c1 m1 o1 c2 m2 o2 -> [Char]
forall a. PrettyPrintable a => a -> [Char]
pprint Diagram c1 m1 o1 c2 m2 o2
t[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
"\\n\\n"[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++(o1 -> m2) -> [o1] -> [Char]
forall a b.
(PrettyPrintable a, PrettyPrintable b) =>
(a -> b) -> [a] -> [Char]
pprintFunction o1 -> m2
c ((c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob(c1 -> [o1])
-> (Diagram c1 m1 o1 c2 m2 o2 -> c1)
-> Diagram c1 m1 o1 c2 m2 o2
-> [o1]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src) Diagram c1 m1 o1 c2 m2 o2
s)
        
    -- | Checks wether the naturality property of a natural transformation is respected.

    checkNaturality :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                                                 Morphism m2 o2, Eq m2, Eq o2) => 
                        NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool
    checkNaturality :: forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Morphism m2 o2, Eq m2, Eq o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool
checkNaturality NaturalTransformation{srcNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
s,tgtNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
t,component :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component=o1 -> m2
c} = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [((Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram c1 m1 o1 c2 m2 o2
t) AssociationList m1 m2 -> m1 -> m2
forall a b. Eq a => AssociationList a b -> a -> b
!-! m1
f) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ (o1 -> m2
c (m1 -> o1
forall m o. Morphism m o => m -> o
source m1
f)) m2 -> m2 -> Bool
forall a. Eq a => a -> a -> Bool
== (o1 -> m2
c (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
f)) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ ((Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram c1 m1 o1 c2 m2 o2
s) AssociationList m1 m2 -> m1 -> m2
forall a b. Eq a => AssociationList a b -> a -> b
!-! m1
f)| m1
f <- (c1 -> [m1]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows(c1 -> [m1])
-> (Diagram c1 m1 o1 c2 m2 o2 -> c1)
-> Diagram c1 m1 o1 c2 m2 o2
-> [m1]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src) Diagram c1 m1 o1 c2 m2 o2
s]
        
    -- | Pre-whiskering as defined in Category Theory for the Sciences (2014) by David I. Spivak

    preWhiskering :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
                    , FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2
                    , FiniteCategory c3 m3 o3, Morphism m3 o3) =>
        NaturalTransformation c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    preWhiskering :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3) =>
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
preWhiskering NaturalTransformation c2 m2 o2 c3 m3 o3
nt Diagram c1 m1 o1 c2 m2 o2
d = NaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> (o1 -> m2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
NaturalTransformation{   srcNT :: Diagram c1 m1 o1 c3 m3 o3
srcNT = (NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT NaturalTransformation c2 m2 o2 c3 m3 o3
nt) Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m1,
 Eq o1, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
`composeDiag` Diagram c1 m1 o1 c2 m2 o2
d 
                                                , tgtNT :: Diagram c1 m1 o1 c3 m3 o3
tgtNT = (NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT NaturalTransformation c2 m2 o2 c3 m3 o3
nt) Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m1,
 Eq o1, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
`composeDiag` Diagram c1 m1 o1 c2 m2 o2
d
                                                , component :: o1 -> m3
component = (NaturalTransformation c2 m2 o2 c3 m3 o3 -> o2 -> m3
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component NaturalTransformation c2 m2 o2 c3 m3 o3
nt)(o2 -> m3) -> (o1 -> o2) -> o1 -> m3
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(AssociationList o1 o2 -> o1 -> o2
forall a b. Eq a => AssociationList a b -> a -> b
assocListToFunct (Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
d))}
                                                
    -- | Pre-whiskering as defined in Category Theory for the Sciences (2014) by David I. Spivak

    postWhiskering ::   ( FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
                        , FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2
                        , FiniteCategory c3 m3 o3, Morphism m3 o3) =>
        Diagram c2 m2 o2 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    postWhiskering :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3) =>
Diagram c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
postWhiskering Diagram c2 m2 o2 c3 m3 o3
d NaturalTransformation c1 m1 o1 c2 m2 o2
nt = NaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> (o1 -> m2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
NaturalTransformation{  srcNT :: Diagram c1 m1 o1 c3 m3 o3
srcNT = Diagram c2 m2 o2 c3 m3 o3
d Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m1,
 Eq o1, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
`composeDiag` (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT NaturalTransformation c1 m1 o1 c2 m2 o2
nt) 
                                                , tgtNT :: Diagram c1 m1 o1 c3 m3 o3
tgtNT = Diagram c2 m2 o2 c3 m3 o3
d Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m1,
 Eq o1, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
`composeDiag` (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT NaturalTransformation c1 m1 o1 c2 m2 o2
nt)
                                                , component :: o1 -> m3
component = (AssociationList m2 m3 -> m2 -> m3
forall a b. Eq a => AssociationList a b -> a -> b
assocListToFunct (Diagram c2 m2 o2 c3 m3 o3 -> AssociationList m2 m3
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram c2 m2 o2 c3 m3 o3
d))(m2 -> m3) -> (o1 -> m2) -> o1 -> m3
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component NaturalTransformation c1 m1 o1 c2 m2 o2
nt)}
        
        
    -- | `FunctorCategory` D^C.

    data FunctorCategory c1 m1 o1 c2 m2 o2 = FunctorCategory {forall c1 m1 o1 c2 m2 o2. FunctorCategory c1 m1 o1 c2 m2 o2 -> c1
sourceCat :: c1 -- ^ /C/

                                                            , forall c1 m1 o1 c2 m2 o2. FunctorCategory c1 m1 o1 c2 m2 o2 -> c2
targetCat :: c2} -- ^ /D/

                                                            deriving (FunctorCategory c1 m1 o1 c2 m2 o2
-> FunctorCategory c1 m1 o1 c2 m2 o2 -> Bool
(FunctorCategory c1 m1 o1 c2 m2 o2
 -> FunctorCategory c1 m1 o1 c2 m2 o2 -> Bool)
-> (FunctorCategory c1 m1 o1 c2 m2 o2
    -> FunctorCategory c1 m1 o1 c2 m2 o2 -> Bool)
-> Eq (FunctorCategory c1 m1 o1 c2 m2 o2)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2) =>
FunctorCategory c1 m1 o1 c2 m2 o2
-> FunctorCategory c1 m1 o1 c2 m2 o2 -> Bool
/= :: FunctorCategory c1 m1 o1 c2 m2 o2
-> FunctorCategory c1 m1 o1 c2 m2 o2 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2) =>
FunctorCategory c1 m1 o1 c2 m2 o2
-> FunctorCategory c1 m1 o1 c2 m2 o2 -> Bool
== :: FunctorCategory c1 m1 o1 c2 m2 o2
-> FunctorCategory c1 m1 o1 c2 m2 o2 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2) =>
FunctorCategory c1 m1 o1 c2 m2 o2
-> FunctorCategory c1 m1 o1 c2 m2 o2 -> Bool
Eq, Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> ShowS
[FunctorCategory c1 m1 o1 c2 m2 o2] -> ShowS
FunctorCategory c1 m1 o1 c2 m2 o2 -> [Char]
(Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> ShowS)
-> (FunctorCategory c1 m1 o1 c2 m2 o2 -> [Char])
-> ([FunctorCategory c1 m1 o1 c2 m2 o2] -> ShowS)
-> Show (FunctorCategory c1 m1 o1 c2 m2 o2)
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
[FunctorCategory c1 m1 o1 c2 m2 o2] -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
FunctorCategory c1 m1 o1 c2 m2 o2 -> [Char]
showList :: [FunctorCategory c1 m1 o1 c2 m2 o2] -> ShowS
$cshowList :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
[FunctorCategory c1 m1 o1 c2 m2 o2] -> ShowS
show :: FunctorCategory c1 m1 o1 c2 m2 o2 -> [Char]
$cshow :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
FunctorCategory c1 m1 o1 c2 m2 o2 -> [Char]
showsPrec :: Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> ShowS
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> ShowS
Show)
    
    enumerateFunctors :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                          FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                          c1 -> c2 -> [Diagram c1 m1 o1 c2 m2 o2]
    enumerateFunctors :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
c1 -> c2 -> [Diagram c1 m1 o1 c2 m2 o2]
enumerateFunctors c1
cat1 c2
cat2 = [Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram{src :: c1
src=c1
cat1,tgt :: c2
tgt=c2
cat2,mmap :: AssociationList m1 m2
mmap=AssociationList m1 m2
appF, omap :: AssociationList o1 o2
omap=AssociationList o1 o2
appO} | AssociationList o1 o2
appO <- [AssociationList o1 o2]
appObj, AssociationList m1 m2
appF <- [AssociationList m1 m2] -> AssociationList m1 m2
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([AssociationList m1 m2] -> AssociationList m1 m2)
-> [[AssociationList m1 m2]] -> [AssociationList m1 m2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[AssociationList m1 m2]] -> [[AssociationList m1 m2]]
forall a. [[a]] -> [[a]]
cartesianProduct [o1 -> o1 -> AssociationList o1 o2 -> [AssociationList m1 m2]
forall {a} {a} {b} {b}.
(FiniteCategory c1 a a, FiniteCategory c2 b b, Morphism a a,
 Morphism b b, Eq a) =>
a -> a -> AssociationList a b -> [AssociationList a b]
twoObjToMaps o1
a o1
b AssociationList o1 o2
appO| o1
a <- c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob c1
cat1, o1
b <- c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob c1
cat1], Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Bool
checkFunctoriality Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram{src :: c1
src=c1
cat1,tgt :: c2
tgt=c2
cat2,mmap :: AssociationList m1 m2
mmap=AssociationList m1 m2
appF, omap :: AssociationList o1 o2
omap=AssociationList o1 o2
appO}]
            where
                appObj :: [AssociationList o1 o2]
appObj = [o1] -> [o2] -> [AssociationList o1 o2]
forall a b. [a] -> [b] -> [AssociationList a b]
enumMaps (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob c1
cat1) (c2 -> [o2]
forall c m o. FiniteCategory c m o => c -> [o]
ob c2
cat2)
                twoObjToMaps :: a -> a -> AssociationList a b -> [AssociationList a b]
twoObjToMaps a
a a
b AssociationList a b
appO = [a] -> [b] -> [AssociationList a b]
forall a b. [a] -> [b] -> [AssociationList a b]
enumMaps (c1 -> a -> a -> [a]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c1
cat1 a
a a
b) (c2 -> b -> b -> [b]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c2
cat2 (AssociationList a b
appO AssociationList a b -> a -> b
forall a b. Eq a => AssociationList a b -> a -> b
!-! a
a) (AssociationList a b
appO AssociationList a b -> a -> b
forall a b. Eq a => AssociationList a b -> a -> b
!-! a
b))
    
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
              FiniteCategory (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) where
        ob :: FunctorCategory c1 m1 o1 c2 m2 o2 -> [Diagram c1 m1 o1 c2 m2 o2]
ob FunctorCategory{sourceCat :: forall c1 m1 o1 c2 m2 o2. FunctorCategory c1 m1 o1 c2 m2 o2 -> c1
sourceCat=c1
cat1, targetCat :: forall c1 m1 o1 c2 m2 o2. FunctorCategory c1 m1 o1 c2 m2 o2 -> c2
targetCat=c2
cat2} = c1 -> c2 -> [Diagram c1 m1 o1 c2 m2 o2]
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
c1 -> c2 -> [Diagram c1 m1 o1 c2 m2 o2]
enumerateFunctors c1
cat1 c2
cat2
        
        identity :: Morphism
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2) =>
FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
identity FunctorCategory c1 m1 o1 c2 m2 o2
c Diagram c1 m1 o1 c2 m2 o2
diag = NaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> (o1 -> m2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
NaturalTransformation{srcNT :: Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
diag,tgtNT :: Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
diag,component :: o1 -> m2
component=(c2 -> o2 -> m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag))(o2 -> m2) -> (o1 -> o2) -> o1 -> m2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(AssociationList o1 o2 -> o1 -> o2
forall a b. Eq a => AssociationList a b -> a -> b
assocListToFunct (Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
diag))}
        
        ar :: Morphism
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2) =>
FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> [NaturalTransformation c1 m1 o1 c2 m2 o2]
ar FunctorCategory c1 m1 o1 c2 m2 o2
c Diagram c1 m1 o1 c2 m2 o2
diag1 Diagram c1 m1 o1 c2 m2 o2
diag2 = [NaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> (o1 -> m2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
NaturalTransformation{srcNT :: Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
diag1,tgtNT :: Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
diag2,component :: o1 -> m2
component=o1 -> m2
mapCompo} | o1 -> m2
mapCompo <- [o1 -> m2]
mapComponent, NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Morphism m2 o2, Eq m2, Eq o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool
checkNaturality NaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> (o1 -> m2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
NaturalTransformation{srcNT :: Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
diag1,tgtNT :: Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
diag2,component :: o1 -> m2
component=o1 -> m2
mapCompo}]
            where
                mapComponent :: [o1 -> m2]
mapComponent = [(o1, m2)] -> o1 -> m2
forall a b. Eq a => AssociationList a b -> a -> b
transformToFunction ([(o1, m2)] -> o1 -> m2) -> [[(o1, m2)]] -> [o1 -> m2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[(o1, m2)]] -> [[(o1, m2)]]
forall a. [[a]] -> [[a]]
cartesianProduct [(\m2
x -> (o1
o,m2
x)) (m2 -> (o1, m2)) -> [m2] -> [(o1, m2)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c2 -> o2 -> o2 -> [m2]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag1) ((Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
diag1) AssociationList o1 o2 -> o1 -> o2
forall a b. Eq a => AssociationList a b -> a -> b
!-! o1
o) ((Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
diag2) AssociationList o1 o2 -> o1 -> o2
forall a b. Eq a => AssociationList a b -> a -> b
!-! o1
o)) | o1
o <- (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
diag1))]
                transformToFunction :: [(t, b)] -> t -> b
transformToFunction ((t
o,b
f):[(t, b)]
xs) t
x = if t
o t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
x then b
f else [(t, b)] -> t -> b
transformToFunction [(t, b)]
xs t
x
                    
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
              GeneratedFiniteCategory (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) where
        genAr :: Morphism
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2) =>
FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> [NaturalTransformation c1 m1 o1 c2 m2 o2]
genAr = FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> [NaturalTransformation c1 m1 o1 c2 m2 o2]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
defaultGenAr
        decompose :: Morphism
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2) =>
FunctorCategory c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> [NaturalTransformation c1 m1 o1 c2 m2 o2]
decompose = FunctorCategory c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> [NaturalTransformation c1 m1 o1 c2 m2 o2]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
defaultDecompose
        
    instance (PrettyPrintable c1, PrettyPrintable c2) =>
              PrettyPrintable (FunctorCategory c1 m1 o1 c2 m2 o2) where
        pprint :: FunctorCategory c1 m1 o1 c2 m2 o2 -> [Char]
pprint FunctorCategory{sourceCat :: forall c1 m1 o1 c2 m2 o2. FunctorCategory c1 m1 o1 c2 m2 o2 -> c1
sourceCat=c1
s, targetCat :: forall c1 m1 o1 c2 m2 o2. FunctorCategory c1 m1 o1 c2 m2 o2 -> c2
targetCat=c2
t} = [Char]
"Fonct("[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++c1 -> [Char]
forall a. PrettyPrintable a => a -> [Char]
pprint c1
s[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
","[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++c2 -> [Char]
forall a. PrettyPrintable a => a -> [Char]
pprint c2
t[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
")"