{-# LANGUAGE MultiParamTypeClasses #-}
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
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)
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]
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))}
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)}
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
, forall c1 m1 o1 c2 m2 o2. FunctorCategory c1 m1 o1 c2 m2 o2 -> c2
targetCat :: c2}
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]
")"