{-# LANGUAGE MultiParamTypeClasses #-}
module Math.Functors.DataMigration
(
deltaFunctor,
piFunctor,
sigmaFunctor
)
where
import Data.WeakSet (Set)
import qualified Data.WeakSet as Set
import Data.WeakSet.Safe
import Data.WeakMap (Map)
import qualified Data.WeakMap as Map
import Data.WeakMap.Safe
import Math.FiniteCategory
import Math.Categories.FunctorCategory
import Math.Functors.Adjunction
deltaFunctor :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
c3 -> Diagram c1 m1 o1 c2 m2 o2 -> Diagram (FunctorCategory c2 m2 o2 c3 m3 o3) (NaturalTransformation c2 m2 o2 c3 m3 o3) (Diagram c2 m2 o2 c3 m3 o3) (FunctorCategory c1 m1 o1 c3 m3 o3) (NaturalTransformation c1 m1 o1 c3 m3 o3) (Diagram c1 m1 o1 c3 m3 o3)
deltaFunctor :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
c3
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
deltaFunctor c3
c Diagram c1 m1 o1 c2 m2 o2
diag = Diagram{src :: FunctorCategory c2 m2 o2 c3 m3 o3
src = FunctorCategory c2 m2 o2 c3 m3 o3
forall {m1} {o1} {m2} {o2}. FunctorCategory c2 m1 o1 c3 m2 o2
s, tgt :: FunctorCategory c1 m1 o1 c3 m3 o3
tgt = FunctorCategory c1 m1 o1 c3 m3 o3
forall {m1} {o1} {m2} {o2}. FunctorCategory c1 m1 o1 c3 m2 o2
t,
omap :: Map (Diagram c2 m2 o2 c3 m3 o3) (Diagram c1 m1 o1 c3 m3 o3)
omap = (Diagram c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c3 m3 o3)
-> Set (Diagram c2 m2 o2 c3 m3 o3)
-> Map (Diagram c2 m2 o2 c3 m3 o3) (Diagram c1 m1 o1 c3 m3 o3)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (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 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, Category c2 m2 o2,
Morphism m2 o2, Eq o2, Eq m2, Morphism m3 o3) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- Diagram c1 m1 o1 c2 m2 o2
diag) (FunctorCategory c2 m2 o2 c3 m3 o3
-> Set (Diagram c2 m2 o2 c3 m3 o3)
forall c m o. FiniteCategory c m o => c -> Set o
ob FunctorCategory c2 m2 o2 c3 m3 o3
forall {m1} {o1} {m2} {o2}. FunctorCategory c2 m1 o1 c3 m2 o2
s),
mmap :: Map
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
mmap = (NaturalTransformation c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3)
-> Set (NaturalTransformation c2 m2 o2 c3 m3 o3)
-> Map
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, FiniteCategory c2 m2 o2,
Morphism m2 o2, Eq c2, Eq m2, Eq o2, Morphism m3 o3, Eq c3, Eq m3,
Eq o3) =>
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
<=@<- Diagram c1 m1 o1 c2 m2 o2
diag) (FunctorCategory c2 m2 o2 c3 m3 o3
-> Set (NaturalTransformation c2 m2 o2 c3 m3 o3)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows FunctorCategory c2 m2 o2 c3 m3 o3
forall {m1} {o1} {m2} {o2}. FunctorCategory c2 m1 o1 c3 m2 o2
s)}
where
s :: FunctorCategory c2 m1 o1 c3 m2 o2
s = c2 -> c3 -> FunctorCategory c2 m1 o1 c3 m2 o2
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (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) c3
c
t :: FunctorCategory c1 m1 o1 c3 m2 o2
t = c1 -> c3 -> FunctorCategory c1 m1 o1 c3 m2 o2
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (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
diag) c3
c
piFunctor :: c3
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
piFunctor c3
c = Diagram
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
-> Diagram
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
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 c2 m2 o2 c1 m1 o1 -> Diagram c1 m1 o1 c2 m2 o2
rightAdjoint(Diagram
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
-> Diagram
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3))
-> (Diagram c1 m1 o1 c2 m2 o2
-> Diagram
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3))
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(c3
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
c3
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
deltaFunctor c3
c)
sigmaFunctor :: c3
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
sigmaFunctor c3
c = Diagram
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
-> Diagram
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
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 -> Diagram c2 m2 o2 c1 m1 o1
leftAdjoint(Diagram
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
-> Diagram
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3))
-> (Diagram c1 m1 o1 c2 m2 o2
-> Diagram
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3))
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(c3
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
c3
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
(FunctorCategory c2 m2 o2 c3 m3 o3)
(NaturalTransformation c2 m2 o2 c3 m3 o3)
(Diagram c2 m2 o2 c3 m3 o3)
(FunctorCategory c1 m1 o1 c3 m3 o3)
(NaturalTransformation c1 m1 o1 c3 m3 o3)
(Diagram c1 m1 o1 c3 m3 o3)
deltaFunctor c3
c)