{-# LANGUAGE MultiParamTypeClasses, MonadComprehensions  #-}

{-| Module  : FiniteCategories
Description : A 'FunctorCategory' has 'Diagram's as objects and 'NaturalTransformation's between them as morphisms.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A 'FunctorCategory' /D/^/C/ (also written [/C/,/D/]) where /C/ is a 'FiniteCategory' and /D/ is a 'Category' has 'Diagram's @F : C -> D@ as objects and 'NaturalTransformation's between them as morphisms. 'NaturalTransformation's compose vertically in this category. See the operator ('<=@<=') for horizontal composition.

A 'Diagram' is a heterogeneous functor, meaning that the source category might be different from the target category. We don't see a diagram as a morphism of categories but as a selection in the target category. See 'FinCat' for a context where 'Diagram's are seen as morphisms of categories.

'Diagram's are objects in a 'FunctorCategory', they therefore can not be composed with the usual operator ('@'). See ('<-@<-') for composing 'Diagram's.

Beware that 'source' and 'target' are not defined on 'Diagram' because it is not a 'Morphism', use 'src' and 'tgt' instead.

You can also do left and right whiskering with the operators ('<=@<-') and ('<-@<=').

A `FunctorCategory` is a 'FiniteCategory' if the source and target category are finite, but it is only a 'Category' if the target category is not finite. 

All operators defined in this module respect the following convention: a "->" arrow represent a functor and a "=>" represent a natural transformation. For example ('<-@<=') allows to compose a natural transformation (the "<=" arrow) with a functor (the "<-" arrow), note that composition is always read from right to left.

-}

module Math.Categories.FunctorCategory
(
    -- * Diagram

    Diagram(..),
    -- ** Check diagram structure

    DiagramError,
    checkFiniteDiagram,
    checkDiagram,
    diagram,
    -- ** Operators

    (->$),
    (->£),
    (<-@<-),
    -- ** Usual diagrams

    selectObject,
    constantDiagram,
    discreteDiagram,
    parallelDiagram,
    -- *** Insertion diagrams for subcategories

    insertionFunctor1,
    insertionFunctor2,
    -- ** Diagram construction helper

    completeDiagram,
    pickRandomDiagram,
    -- * Natural transformation

    NaturalTransformation,
    -- ** Getter

    components,
    -- ** Check structure

    NaturalTransformationError,
    checkNaturalTransformation,
    naturalTransformation,
    unsafeNaturalTransformation,
    -- ** Operators

    (=>$),
    (<=@<=),
    horizontalComposition,
    (<=@<-),
    leftWhiskering,
    (<-@<=),
    rightWhiskering,
    -- * Functor categories

    FunctorCategory(..),
    PrecomposedFunctorCategory(..),
    PostcomposedFunctorCategory(..),
)
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.Category
    import              Math.FiniteCategories.One
    import              Math.Categories.Galaxy
    import              Math.FiniteCategories.DiscreteCategory
    import              Math.FiniteCategories.Parallel
    import              Math.FiniteCategories.FullSubcategory
    import              Math.FiniteCategory
    import              Math.IO.PrettyPrint
    
    import              System.Random            (RandomGen, uniformR)
    
    
    -- | A 'Diagram' is a functor from a 'FiniteCategory' to a 'Category'.

    --    

    -- A 'Diagram' can have a source category and a target category with different types. It must obey the following rules :

    --

    -- prop> funct ->$ (source f) == source (funct ->£ f)

    -- prop> funct ->$ (target f) == target (funct ->£ f)

    -- prop> funct ->£ (f @ g) = (funct ->£ f) @ (funct ->£ g)

    -- prop> funct ->£ (identity a) = identity (funct ->$ a)

    --

    -- 'Diagram' is not private because we can't always check functoriality if the target category is infinite.

    -- However it is recommanded to use the smart constructor 'diagram' which checks the structure of the 'Diagram' at construction.

    data Diagram c1 m1 o1 c2 m2 o2 = Diagram { 
                                                forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src :: c1, -- ^ The source category

                                                forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt :: c2, -- ^ The target category

                                                forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap :: Map o1 o2, -- ^ The object map

                                                forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap :: Map m1 m2 -- ^ The morphism map

                                              } deriving (Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
(Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool)
-> (Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool)
-> Eq (Diagram 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, Eq o1, Eq o2, Eq m1, Eq m2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
== :: Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
/= :: Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
Eq, Int -> Diagram c1 m1 o1 c2 m2 o2 -> ShowS
[Diagram c1 m1 o1 c2 m2 o2] -> ShowS
Diagram c1 m1 o1 c2 m2 o2 -> String
(Int -> Diagram c1 m1 o1 c2 m2 o2 -> ShowS)
-> (Diagram c1 m1 o1 c2 m2 o2 -> String)
-> ([Diagram c1 m1 o1 c2 m2 o2] -> ShowS)
-> Show (Diagram c1 m1 o1 c2 m2 o2)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
Int -> Diagram c1 m1 o1 c2 m2 o2 -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
[Diagram c1 m1 o1 c2 m2 o2] -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
Int -> Diagram c1 m1 o1 c2 m2 o2 -> ShowS
showsPrec :: Int -> Diagram c1 m1 o1 c2 m2 o2 -> ShowS
$cshow :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String
show :: Diagram c1 m1 o1 c2 m2 o2 -> String
$cshowList :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
[Diagram c1 m1 o1 c2 m2 o2] -> ShowS
showList :: [Diagram c1 m1 o1 c2 m2 o2] -> ShowS
Show)
    
    instance (  PrettyPrint c1, PrettyPrint m1, PrettyPrint o1, Eq m1, Eq o1,
                PrettyPrint c2, PrettyPrint m2, PrettyPrint o2, Eq m2, Eq o2) => PrettyPrint (Diagram c1 m1 o1 c2 m2 o2) where
        pprint :: Diagram c1 m1 o1 c2 m2 o2 -> String
pprint Diagram c1 m1 o1 c2 m2 o2
funct = String
"Diagram(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ c1 -> String
forall a. PrettyPrint a => a -> String
pprint (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
funct) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"->" String -> ShowS
forall a. [a] -> [a] -> [a]
++ c2 -> String
forall a. PrettyPrint a => a -> String
pprint (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
funct) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ Map o1 o2 -> String
forall a. PrettyPrint a => a -> String
pprint (Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
funct) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ Map m1 m2 -> String
forall a. PrettyPrint a => a -> String
pprint (Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram c1 m1 o1 c2 m2 o2
funct) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
    
    -- | Apply a 'Diagram' on an object of the source category.

    (->$) :: (Eq o1) => Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
    ->$ :: forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
(->$) Diagram c1 m1 o1 c2 m2 o2
f o1
x = Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
f Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| o1
x
    
    -- | Apply a 'Diagram' on a morphism of the source category.

    (->£) :: (Eq m1) => Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
    ->£ :: forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
(->£) Diagram c1 m1 o1 c2 m2 o2
f m1
x = Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram c1 m1 o1 c2 m2 o2
f Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| m1
x
    
    -- | Compose two 'Diagram's.

    (<-@<-) :: (Eq o2, Eq m2) => Diagram c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
    <-@<- :: forall o2 m2 c2 c3 m3 o3 c1 m1 o1.
(Eq o2, Eq m2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
(<-@<-) Diagram c2 m2 o2 c3 m3 o3
g Diagram c1 m1 o1 c2 m2 o2
f = Diagram{src :: c1
src = 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
f, tgt :: c3
tgt = Diagram c2 m2 o2 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c2 m2 o2 c3 m3 o3
g, omap :: Map o1 o3
omap = (Diagram c2 m2 o2 c3 m3 o3 -> Map o2 o3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram c2 m2 o2 c3 m3 o3
g) Map o2 o3 -> Map o1 o2 -> Map o1 o3
forall b c a. Eq b => Map b c -> Map a b -> Map a c
|.| (Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
f), mmap :: Map m1 m3
mmap = (Diagram c2 m2 o2 c3 m3 o3 -> Map m2 m3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram c2 m2 o2 c3 m3 o3
g) Map m2 m3 -> Map m1 m2 -> Map m1 m3
forall b c a. Eq b => Map b c -> Map a b -> Map a c
|.| (Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram c1 m1 o1 c2 m2 o2
f)}
    
    -- | Construct a 'Diagram' selecting an object in a category.

    --

    -- There is no check that the object belongs in the category.

    selectObject :: (Category c m o, Morphism m o, Eq o) => c -> o -> Diagram One One One c m o
    selectObject :: forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> o -> Diagram One One One c m o
selectObject c
c o
o = Diagram{src :: One
src=One
One, tgt :: c
tgt=c
c, omap :: Map One o
omap=AssociationList One o -> Map One o
forall k v. AssociationList k v -> Map k v
weakMap [(One
One,o
o)], mmap :: Map One m
mmap=AssociationList One m -> Map One m
forall k v. AssociationList k v -> Map k v
weakMap [(One
One, c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c o
o)]}
    
    -- | Construct a constant 'Diagram' on an object of the target 'Category' given an indexing 'FiniteCategory'.

    --

    -- There is no check that the object belongs in the category.

    constantDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1,
                              Category c2 m2 o2, Morphism m2 o2) => 
            c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
    constantDiagram :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram c1
index c2
targ o2
o = Diagram{src :: c1
src=c1
index, tgt :: c2
tgt=c2
targ, omap :: Map o1 o2
omap=(o1 -> o2) -> Set o1 -> Map o1 o2
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (o2 -> o1 -> o2
forall a b. a -> b -> a
const o2
o) (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
index), mmap :: Map m1 m2
mmap=(m1 -> m2) -> Set m1 -> Map m1 m2
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (m2 -> m1 -> m2
forall a b. a -> b -> a
const (c2 -> o2 -> m2
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c2
targ o2
o)) (c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c1
index)}
    
    -- | Construct a discrete 'Diagram' on a list of objects of the target 'Category'.

    --

    -- We consider list of objects because a single object can be selected several times.

    --

    -- There is no check that the objects belongs in the category.

    discreteDiagram :: (Category c m o, Morphism m o, Eq o) => 
            c -> [o] -> Diagram (DiscreteCategory Int) (DiscreteMorphism Int) Int c m o
    discreteDiagram :: forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c
-> [o]
-> Diagram (DiscreteCategory Int) (DiscreteMorphism Int) Int c m o
discreteDiagram c
targ [o]
os = Diagram{src :: DiscreteCategory Int
src=Set Int -> DiscreteCategory Int
forall a. Set a -> DiscreteCategory a
discreteCategory Set Int
indices, tgt :: c
tgt=c
targ, omap :: Map Int o
omap=(Int -> o) -> Set Int -> Map Int o
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction ([o]
os [o] -> Int -> o
forall a. HasCallStack => [a] -> Int -> a
!!) Set Int
indices, mmap :: Map (DiscreteMorphism Int) m
mmap=(DiscreteMorphism Int -> m)
-> Set (DiscreteMorphism Int) -> Map (DiscreteMorphism Int) m
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (\(StarIdentity Int
x) -> c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
targ ([o]
os [o] -> Int -> o
forall a. HasCallStack => [a] -> Int -> a
!! Int
x)) (DiscreteCategory Int -> Set (DiscreteMorphism Int)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (Set Int -> DiscreteCategory Int
forall a. Set a -> DiscreteCategory a
discreteCategory Set Int
indices))}
        where
            indices :: Set Int
indices = [Int] -> Set Int
forall a. [a] -> Set a
set [Int
0..(([o] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [o]
os)Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
    
    -- | Construct a parallel 'Diagram' on two parallel morphisms of the target 'Category'.

    --

    -- There is no check that the morphisms belongs in the category and no check that the two morphisms are parallel.

    parallelDiagram :: (Category c m o, Morphism m o, Eq o) => 
            c -> m -> m -> Diagram Parallel ParallelAr ParallelOb c m o
    parallelDiagram :: forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> m -> m -> Diagram Parallel ParallelAr ParallelOb c m o
parallelDiagram c
targ m
f m
g = Diagram Parallel ParallelAr ParallelOb c m o
-> Diagram Parallel ParallelAr ParallelOb c m o
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: Parallel
src=Parallel
Parallel, tgt :: c
tgt=c
targ, omap :: Map ParallelOb o
omap=AssociationList ParallelOb o -> Map ParallelOb o
forall k v. AssociationList k v -> Map k v
weakMap [(ParallelOb
ParallelA,m -> o
forall m o. Morphism m o => m -> o
source m
f),(ParallelOb
ParallelB,m -> o
forall m o. Morphism m o => m -> o
target m
f)], mmap :: Map ParallelAr m
mmap=AssociationList ParallelAr m -> Map ParallelAr m
forall k v. AssociationList k v -> Map k v
weakMap [(ParallelAr
ParallelF, m
f), (ParallelAr
ParallelG, m
g)]}
    
    
    -- Diagram structure check

    
    -- | A datatype to represent a malformation of a 'Diagram'.

    data DiagramError c1 m1 o1 c2 m2 o2 = WrongDomainObjects{forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> Set o1
srcObjs :: Set o1, forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> Set o1
domainObjs :: Set o1} -- ^ The objects in the domain of the object mapping are not the same as the objects of the source category.

                                        | WrongDomainMorphisms{forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> Set m1
srcMorphs :: Set m1, forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> Set m1
domainMorphs :: Set m1} -- ^ The morphisms in the domain of the morphism mapping are not the same as the morphisms of the source category.

                                        | WrongImageObjects{forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> Set o2
imageObjs :: Set o2, forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> Set o2
codomainObjs :: Set o2} -- ^ The objects in the image of the object mapping are not included in the objects of the codomain category.

                                        | WrongImageMorphisms{forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> Set m2
imageMorphs :: Set m2, forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> Set m2
codomainMorphs :: Set m2} -- ^ The morphisms in the image of the morphism mapping are not included in the morphisms of the codomain category.

                                        | TornMorphism{forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> m1
f :: m1, forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> m2
fImage :: m2} -- ^ A morphism /f/ is torn apart.

                                        | IdentityNotPreserved{forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> m1
originalId :: m1, forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> m2
imageId :: m2} -- ^ The image of an identity is not an identity.

                                        | CompositionNotPreserved{f :: m1, forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> m1
g :: m1, forall c1 m1 o1 c2 m2 o2. DiagramError c1 m1 o1 c2 m2 o2 -> m2
imageFG :: m2} -- ^ Composition is not preserved by the functor.

                               deriving (DiagramError c1 m1 o1 c2 m2 o2
-> DiagramError c1 m1 o1 c2 m2 o2 -> Bool
(DiagramError c1 m1 o1 c2 m2 o2
 -> DiagramError c1 m1 o1 c2 m2 o2 -> Bool)
-> (DiagramError c1 m1 o1 c2 m2 o2
    -> DiagramError c1 m1 o1 c2 m2 o2 -> Bool)
-> Eq (DiagramError c1 m1 o1 c2 m2 o2)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c1 m1 o1 c2 m2 o2.
(Eq o1, Eq o2, Eq m1, Eq m2) =>
DiagramError c1 m1 o1 c2 m2 o2
-> DiagramError c1 m1 o1 c2 m2 o2 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2.
(Eq o1, Eq o2, Eq m1, Eq m2) =>
DiagramError c1 m1 o1 c2 m2 o2
-> DiagramError c1 m1 o1 c2 m2 o2 -> Bool
== :: DiagramError c1 m1 o1 c2 m2 o2
-> DiagramError c1 m1 o1 c2 m2 o2 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2.
(Eq o1, Eq o2, Eq m1, Eq m2) =>
DiagramError c1 m1 o1 c2 m2 o2
-> DiagramError c1 m1 o1 c2 m2 o2 -> Bool
/= :: DiagramError c1 m1 o1 c2 m2 o2
-> DiagramError c1 m1 o1 c2 m2 o2 -> Bool
Eq, Int -> DiagramError c1 m1 o1 c2 m2 o2 -> ShowS
[DiagramError c1 m1 o1 c2 m2 o2] -> ShowS
DiagramError c1 m1 o1 c2 m2 o2 -> String
(Int -> DiagramError c1 m1 o1 c2 m2 o2 -> ShowS)
-> (DiagramError c1 m1 o1 c2 m2 o2 -> String)
-> ([DiagramError c1 m1 o1 c2 m2 o2] -> ShowS)
-> Show (DiagramError c1 m1 o1 c2 m2 o2)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2.
(Show o1, Show o2, Show m1, Show m2) =>
Int -> DiagramError c1 m1 o1 c2 m2 o2 -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show o1, Show o2, Show m1, Show m2) =>
[DiagramError c1 m1 o1 c2 m2 o2] -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show o1, Show o2, Show m1, Show m2) =>
DiagramError c1 m1 o1 c2 m2 o2 -> String
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2.
(Show o1, Show o2, Show m1, Show m2) =>
Int -> DiagramError c1 m1 o1 c2 m2 o2 -> ShowS
showsPrec :: Int -> DiagramError c1 m1 o1 c2 m2 o2 -> ShowS
$cshow :: forall c1 m1 o1 c2 m2 o2.
(Show o1, Show o2, Show m1, Show m2) =>
DiagramError c1 m1 o1 c2 m2 o2 -> String
show :: DiagramError c1 m1 o1 c2 m2 o2 -> String
$cshowList :: forall c1 m1 o1 c2 m2 o2.
(Show o1, Show o2, Show m1, Show m2) =>
[DiagramError c1 m1 o1 c2 m2 o2] -> ShowS
showList :: [DiagramError c1 m1 o1 c2 m2 o2] -> ShowS
Show)
                               
    -- | Check wether the properties of a 'Diagram' are respected where the target category is finite.

    checkFiniteDiagram :: (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 -> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
    checkFiniteDiagram :: 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 -> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
checkFiniteDiagram d :: Diagram c1 m1 o1 c2 m2 o2
d@Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=c1
s,tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=c2
t,omap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap=Map o1 o2
om,mmap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap=Map m1 m2
fm}
        | Map o1 o2 -> Set o1
forall k a. Map k a -> Set k
domain Map o1 o2
om Set o1 -> Set o1 -> Bool
forall a. Eq a => a -> a -> Bool
/= c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
s = DiagramError c1 m1 o1 c2 m2 o2
-> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just WrongDomainObjects{srcObjs :: Set o1
srcObjs = c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
s, domainObjs :: Set o1
domainObjs = Map o1 o2 -> Set o1
forall k a. Map k a -> Set k
domain Map o1 o2
om}
        | Map m1 m2 -> Set m1
forall k a. Map k a -> Set k
domain Map m1 m2
fm Set m1 -> Set m1 -> Bool
forall a. Eq a => a -> a -> Bool
/= c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c1
s = DiagramError c1 m1 o1 c2 m2 o2
-> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just WrongDomainMorphisms{srcMorphs :: Set m1
srcMorphs = c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c1
s, domainMorphs :: Set m1
domainMorphs = Map m1 m2 -> Set m1
forall k a. Map k a -> Set k
domain Map m1 m2
fm}
        | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map o1 o2 -> Set o2
forall k a. Eq k => Map k a -> Set a
image Map o1 o2
om Set o2 -> Set o2 -> Bool
forall a. Eq a => Set a -> Set a -> Bool
`isIncludedIn` c2 -> Set o2
forall c m o. FiniteCategory c m o => c -> Set o
ob c2
t = DiagramError c1 m1 o1 c2 m2 o2
-> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just WrongImageObjects{imageObjs :: Set o2
imageObjs = Map o1 o2 -> Set o2
forall k a. Eq k => Map k a -> Set a
image Map o1 o2
om, codomainObjs :: Set o2
codomainObjs = c2 -> Set o2
forall c m o. FiniteCategory c m o => c -> Set o
ob c2
t}
        | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map m1 m2 -> Set m2
forall k a. Eq k => Map k a -> Set a
image Map m1 m2
fm Set m2 -> Set m2 -> Bool
forall a. Eq a => Set a -> Set a -> Bool
`isIncludedIn` c2 -> Set m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c2
t = DiagramError c1 m1 o1 c2 m2 o2
-> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just WrongImageMorphisms{imageMorphs :: Set m2
imageMorphs = Map m1 m2 -> Set m2
forall k a. Eq k => Map k a -> Set a
image Map m1 m2
fm, codomainMorphs :: Set m2
codomainMorphs = c2 -> Set m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c2
t}
        | Bool -> Bool
not(Bool -> Bool) -> (Set m1 -> Bool) -> Set m1 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set m1 -> Bool
forall a. Set a -> Bool
Set.null) (Set m1 -> Bool) -> Set m1 -> Bool
forall a b. (a -> b) -> a -> b
$ Set m1
tear = DiagramError c1 m1 o1 c2 m2 o2
-> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just TornMorphism{f :: m1
f = Set m1 -> m1
forall a. Set a -> a
anElement Set m1
tear, fImage :: m2
fImage = Diagram c1 m1 o1 c2 m2 o2
d Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ (Set m1 -> m1
forall a. Set a -> a
anElement Set m1
tear)}
        | Bool -> Bool
not(Bool -> Bool) -> (Set o1 -> Bool) -> Set o1 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set o1 -> Bool
forall a. Set a -> Bool
Set.null) (Set o1 -> Bool) -> Set o1 -> Bool
forall a b. (a -> b) -> a -> b
$ Set o1
imId = DiagramError c1 m1 o1 c2 m2 o2
-> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just IdentityNotPreserved{originalId :: m1
originalId = c1 -> o1 -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c1
s (Set o1 -> o1
forall a. Set a -> a
anElement Set o1
imId), imageId :: m2
imageId = Diagram c1 m1 o1 c2 m2 o2
d Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ (c1 -> o1 -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c1
s (Set o1 -> o1
forall a. Set a -> a
anElement Set o1
imId))}
        | Bool -> Bool
not(Bool -> Bool) -> (Set (m1, m1) -> Bool) -> Set (m1, m1) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set (m1, m1) -> Bool
forall a. Set a -> Bool
Set.null) (Set (m1, m1) -> Bool) -> Set (m1, m1) -> Bool
forall a b. (a -> b) -> a -> b
$ Set (m1, m1)
errCompo = DiagramError c1 m1 o1 c2 m2 o2
-> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just CompositionNotPreserved{f :: m1
f = (m1, m1) -> m1
forall a b. (a, b) -> a
fst (Set (m1, m1) -> (m1, m1)
forall a. Set a -> a
anElement Set (m1, m1)
errCompo), g :: m1
g = (m1, m1) -> m1
forall a b. (a, b) -> b
snd (Set (m1, m1) -> (m1, m1)
forall a. Set a -> a
anElement Set (m1, m1)
errCompo), imageFG :: m2
imageFG = Diagram c1 m1 o1 c2 m2 o2
d Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ (((m1, m1) -> m1
forall a b. (a, b) -> b
snd (Set (m1, m1) -> (m1, m1)
forall a. Set a -> a
anElement Set (m1, m1)
errCompo)) m1 -> m1 -> m1
forall m o. Morphism m o => m -> m -> m
@ ((m1, m1) -> m1
forall a b. (a, b) -> a
fst (Set (m1, m1) -> (m1, m1)
forall a. Set a -> a
anElement Set (m1, m1)
errCompo)))}
        | Bool
otherwise = Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
        where
            tear :: Set m1
tear = [m1
arr | m1
arr <- Map m1 m2 -> Set m1
forall k a. Map k a -> Set k
domain Map m1 m2
fm, Map o1 o2
om Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| (m1 -> o1
forall m o. Morphism m o => m -> o
source m1
arr) o2 -> o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= m2 -> o2
forall m o. Morphism m o => m -> o
source (Map m1 m2
fm Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| m1
arr) Bool -> Bool -> Bool
|| Map o1 o2
om Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
arr) o2 -> o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= m2 -> o2
forall m o. Morphism m o => m -> o
target (Map m1 m2
fm Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| m1
arr)]
            imId :: Set o1
imId = [o1
a | o1
a <- c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
s, Map m1 m2
fm Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| (c1 -> o1 -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c1
s o1
a) m2 -> m2 -> Bool
forall a. Eq a => a -> a -> Bool
/= c2 -> o2 -> m2
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c2
t (Map o1 o2
om Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| o1
a)]
            errCompo :: Set (m1, m1)
errCompo = [(m1
f,m1
g) | m1
f <- (c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c1
s), m1
g <- (c1 -> o1 -> Set m1
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
arFrom c1
s (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
f)), Map m1 m2
fm Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| (m1
g m1 -> m1 -> m1
forall m o. Morphism m o => m -> m -> m
@ m1
f) m2 -> m2 -> Bool
forall a. Eq a => a -> a -> Bool
/= (Map m1 m2
fm Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| m1
g) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ (Map m1 m2
fm Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| m1
f)]
            
    -- | Check wether the properties of a 'Diagram' are respected where the target category is infinite.

    checkDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                           Category c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                      Diagram c1 m1 o1 c2 m2 o2 -> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
    checkDiagram :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
checkDiagram d :: Diagram c1 m1 o1 c2 m2 o2
d@Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=c1
s,tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=c2
t,omap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap=Map o1 o2
om,mmap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap=Map m1 m2
fm}
        | Map o1 o2 -> Set o1
forall k a. Map k a -> Set k
domain Map o1 o2
om Set o1 -> Set o1 -> Bool
forall a. Eq a => a -> a -> Bool
/= c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
s = DiagramError c1 m1 o1 c2 m2 o2
-> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just WrongDomainObjects{srcObjs :: Set o1
srcObjs = c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
s, domainObjs :: Set o1
domainObjs = Map o1 o2 -> Set o1
forall k a. Map k a -> Set k
domain Map o1 o2
om}
        | Map m1 m2 -> Set m1
forall k a. Map k a -> Set k
domain Map m1 m2
fm Set m1 -> Set m1 -> Bool
forall a. Eq a => a -> a -> Bool
/= c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c1
s = DiagramError c1 m1 o1 c2 m2 o2
-> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just WrongDomainMorphisms{srcMorphs :: Set m1
srcMorphs = c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c1
s, domainMorphs :: Set m1
domainMorphs = Map m1 m2 -> Set m1
forall k a. Map k a -> Set k
domain Map m1 m2
fm}
        | Bool -> Bool
not(Bool -> Bool) -> (Set m1 -> Bool) -> Set m1 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set m1 -> Bool
forall a. Set a -> Bool
Set.null) (Set m1 -> Bool) -> Set m1 -> Bool
forall a b. (a -> b) -> a -> b
$ Set m1
tear = DiagramError c1 m1 o1 c2 m2 o2
-> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just TornMorphism{f :: m1
f = Set m1 -> m1
forall a. Set a -> a
anElement Set m1
tear, fImage :: m2
fImage = Diagram c1 m1 o1 c2 m2 o2
d Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ (Set m1 -> m1
forall a. Set a -> a
anElement Set m1
tear)}
        | Bool -> Bool
not(Bool -> Bool) -> (Set o1 -> Bool) -> Set o1 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set o1 -> Bool
forall a. Set a -> Bool
Set.null) (Set o1 -> Bool) -> Set o1 -> Bool
forall a b. (a -> b) -> a -> b
$ Set o1
imId = DiagramError c1 m1 o1 c2 m2 o2
-> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just IdentityNotPreserved{originalId :: m1
originalId = c1 -> o1 -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c1
s (Set o1 -> o1
forall a. Set a -> a
anElement Set o1
imId), imageId :: m2
imageId = Diagram c1 m1 o1 c2 m2 o2
d Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ (c1 -> o1 -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c1
s (Set o1 -> o1
forall a. Set a -> a
anElement Set o1
imId))}
        | Bool -> Bool
not(Bool -> Bool) -> (Set (m1, m1) -> Bool) -> Set (m1, m1) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set (m1, m1) -> Bool
forall a. Set a -> Bool
Set.null) (Set (m1, m1) -> Bool) -> Set (m1, m1) -> Bool
forall a b. (a -> b) -> a -> b
$ Set (m1, m1)
errCompo = DiagramError c1 m1 o1 c2 m2 o2
-> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just CompositionNotPreserved{f :: m1
f = (m1, m1) -> m1
forall a b. (a, b) -> a
fst (Set (m1, m1) -> (m1, m1)
forall a. Set a -> a
anElement Set (m1, m1)
errCompo), g :: m1
g = (m1, m1) -> m1
forall a b. (a, b) -> b
snd (Set (m1, m1) -> (m1, m1)
forall a. Set a -> a
anElement Set (m1, m1)
errCompo), imageFG :: m2
imageFG = Diagram c1 m1 o1 c2 m2 o2
d Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ (((m1, m1) -> m1
forall a b. (a, b) -> b
snd (Set (m1, m1) -> (m1, m1)
forall a. Set a -> a
anElement Set (m1, m1)
errCompo)) m1 -> m1 -> m1
forall m o. Morphism m o => m -> m -> m
@ ((m1, m1) -> m1
forall a b. (a, b) -> a
fst (Set (m1, m1) -> (m1, m1)
forall a. Set a -> a
anElement Set (m1, m1)
errCompo)))}
        | Bool
otherwise = Maybe (DiagramError c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
        where
            tear :: Set m1
tear = [m1
arr | m1
arr <- Map m1 m2 -> Set m1
forall k a. Map k a -> Set k
domain Map m1 m2
fm, Map o1 o2
om Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| (m1 -> o1
forall m o. Morphism m o => m -> o
source m1
arr) o2 -> o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= m2 -> o2
forall m o. Morphism m o => m -> o
source (Map m1 m2
fm Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| m1
arr) Bool -> Bool -> Bool
|| Map o1 o2
om Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
arr) o2 -> o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= m2 -> o2
forall m o. Morphism m o => m -> o
target (Map m1 m2
fm Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| m1
arr)]
            imId :: Set o1
imId = [o1
a | o1
a <- c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
s, Map m1 m2
fm Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| (c1 -> o1 -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c1
s o1
a) m2 -> m2 -> Bool
forall a. Eq a => a -> a -> Bool
/= c2 -> o2 -> m2
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c2
t (Map o1 o2
om Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| o1
a)]
            errCompo :: Set (m1, m1)
errCompo = [(m1
f,m1
g) | m1
f <- (c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c1
s), m1
g <- (c1 -> o1 -> Set m1
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
arFrom c1
s (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
f)), Map m1 m2
fm Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| (m1
g m1 -> m1 -> m1
forall m o. Morphism m o => m -> m -> m
@ m1
f) m2 -> m2 -> Bool
forall a. Eq a => a -> a -> Bool
/= (Map m1 m2
fm Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| m1
g) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ (Map m1 m2
fm Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| m1
f)]
    
    -- | Smart constructor of 'Diagram'.

    diagram :: ( FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                 c1 -> c2 -> Map o1 o2 -> Map m1 m2 -> Either (DiagramError c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
    diagram :: 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
-> Map o1 o2
-> Map m1 m2
-> Either
     (DiagramError c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
diagram c1
c1 c2
c2 Map o1 o2
om Map m1 m2
mm 
        | Maybe (DiagramError c1 m1 o1 c2 m2 o2) -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe (DiagramError c1 m1 o1 c2 m2 o2)
check = Diagram c1 m1 o1 c2 m2 o2
-> Either
     (DiagramError c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
forall a b. b -> Either a b
Right Diagram c1 m1 o1 c2 m2 o2
diag
        | Bool
otherwise = DiagramError c1 m1 o1 c2 m2 o2
-> Either
     (DiagramError c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
forall a b. a -> Either a b
Left DiagramError c1 m1 o1 c2 m2 o2
err
        where
            diag :: Diagram c1 m1 o1 c2 m2 o2
diag = Diagram{src :: c1
src = c1
c1, tgt :: c2
tgt = c2
c2, omap :: Map o1 o2
omap = Map o1 o2
om, mmap :: Map m1 m2
mmap = Map m1 m2
mm}
            check :: Maybe (DiagramError c1 m1 o1 c2 m2 o2)
check = Diagram c1 m1 o1 c2 m2 o2 -> Maybe (DiagramError 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) =>
Diagram c1 m1 o1 c2 m2 o2 -> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
checkFiniteDiagram Diagram c1 m1 o1 c2 m2 o2
diag
            Just DiagramError c1 m1 o1 c2 m2 o2
err = Maybe (DiagramError c1 m1 o1 c2 m2 o2)
check
    
    -- | Complete a partial 'Diagram' by adding the mapping between identities and the mapping between composite morphisms using the decomposition of the indexing category.

    --

    -- Does not check the structure of the resulting 'Diagram', you can use 'checkFiniteDiagram' to check afterwards.

    completeDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                              Category c2 m2 o2, Morphism m2 o2) => 
        Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
    completeDiagram :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=c1
s,tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=c2
t,omap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap=Map o1 o2
om,mmap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap=Map m1 m2
mm} = Diagram{src :: c1
src=c1
s,tgt :: c2
tgt=c2
t,omap :: Map o1 o2
omap=Map o1 o2
om, mmap :: Map m1 m2
mmap=[Map m1 m2] -> Map m1 m2
forall k a. Eq k => [Map k a] -> Map k a
Map.unions [Map m1 m2
mm, Map m1 m2
mapId, Map m1 m2
mapCompo] }
        where
            mapId :: Map m1 m2
mapId = Set (m1, m2) -> Map m1 m2
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(c1 -> o1 -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c1
s o1
o, c2 -> o2 -> m2
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c2
t (Map o1 o2
om Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| o1
o)) | o1
o <- c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
s]
            mapCompo :: Map m1 m2
mapCompo = Set (m1, m2) -> Map m1 m2
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(m1
f, [m2] -> m2
forall m o. Morphism m o => [m] -> m
compose ([m2] -> m2) -> [m2] -> m2
forall a b. (a -> b) -> a -> b
$ (Map m1 m2
mm Map m1 m2 -> m1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!|) (m1 -> m2) -> [m1] -> [m2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c1 -> m1 -> [m1]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c1
s m1
f) | m1
f <- c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c1
s, c1 -> m1 -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m) =>
c -> m -> Bool
isComposite c1
s m1
f]
    
    
    -- | Pick one element of a list randomly.

    pickOne :: (RandomGen g) => [a] -> g -> (a,g)
    pickOne :: forall g a. RandomGen g => [a] -> g -> (a, g)
pickOne [] g
g = String -> (a, g)
forall a. HasCallStack => String -> a
error String
"pickOne in an empty list."
    pickOne [a]
l g
g = (([a]
l [a] -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!! Int
index),g
newGen) where
        (Int
index,g
newGen) = ((Int, Int) -> g -> (Int, g)
forall g a. (RandomGen g, UniformRange a) => (a, a) -> g -> (a, g)
uniformR (Int
0,([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
l)Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) g
g)
    
    -- | Choose a random diagram in the functor category of an index category and an image category.

    pickRandomDiagram :: (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,
                        RandomGen g) => c1 -> c2 -> g -> (Diagram c1 m1 o1 c2 m2 o2, g)
    pickRandomDiagram :: forall c1 m1 o1 c2 m2 o2 g.
(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,
 RandomGen g) =>
c1 -> c2 -> g -> (Diagram c1 m1 o1 c2 m2 o2, g)
pickRandomDiagram c1
index c2
cat g
gen = [Diagram c1 m1 o1 c2 m2 o2] -> g -> (Diagram c1 m1 o1 c2 m2 o2, g)
forall g a. RandomGen g => [a] -> g -> (a, g)
pickOne (Set (Diagram c1 m1 o1 c2 m2 o2) -> [Diagram c1 m1 o1 c2 m2 o2]
forall a. Eq a => Set a -> [a]
setToList(Set (Diagram c1 m1 o1 c2 m2 o2) -> [Diagram c1 m1 o1 c2 m2 o2])
-> (FunctorCategory c1 m1 o1 c2 m2 o2
    -> Set (Diagram c1 m1 o1 c2 m2 o2))
-> FunctorCategory c1 m1 o1 c2 m2 o2
-> [Diagram c1 m1 o1 c2 m2 o2]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.FunctorCategory c1 m1 o1 c2 m2 o2
-> Set (Diagram c1 m1 o1 c2 m2 o2)
forall c m o. FiniteCategory c m o => c -> Set o
ob (FunctorCategory 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]
forall a b. (a -> b) -> a -> b
$ c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory c1
index c2
cat) g
gen
    
    
    
    
    -- NaturalTransformation

    
    -- | A `NaturalTransformation` between two 'Diagram's from /C/ to /D/ is a mapping from objects of /C/ to morphisms of /D/ such that naturality is respected. /C/ must be a 'FiniteCategory' because we need its objects in the mapping of a 'NaturalTransformation'.

    --

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

    --

    -- prop> source F = source G

    -- prop> target F = target G

    -- prop> (eta =>$ target f) @ (F ->£ f) = (G ->£ f) @ (eta =>$ source f)

    --

    -- 'NaturalTransformation' is private, use the smart constructor 'naturalTransformation' to instantiate it.

    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, -- ^ The source functor (private, use 'source' instead).

                                                            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, -- ^ The target functor (private, use 'target' instead).

                                                            forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
components :: Map o1 m2 -- ^ The components

                                                        } deriving (NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool
(NaturalTransformation c1 m1 o1 c2 m2 o2
 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool)
-> Eq (NaturalTransformation 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, Eq o1, Eq o2, Eq m1, Eq m2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool
== :: NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool
/= :: NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool
Eq)
    
    instance (Show c1, Show m1, Show o1, Show c2, Show m2, Show o2) => Show (NaturalTransformation c1 m1 o1 c2 m2 o2) where
        show :: NaturalTransformation c1 m1 o1 c2 m2 o2 -> String
show NaturalTransformation c1 m1 o1 c2 m2 o2
nt = String
"(unsafeNaturalTransformation "String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Diagram c1 m1 o1 c2 m2 o2 -> String
forall a. Show a => a -> String
show(Diagram c1 m1 o1 c2 m2 o2 -> String)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.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 -> String)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> String
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Diagram c1 m1 o1 c2 m2 o2 -> String
forall a. Show a => a -> String
show(Diagram c1 m1 o1 c2 m2 o2 -> String)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.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 -> String)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> String
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Map o1 m2 -> String
forall a. Show a => a -> String
show(Map o1 m2 -> String)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
components (NaturalTransformation c1 m1 o1 c2 m2 o2 -> String)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> String
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
        
    instance (  PrettyPrint c1, PrettyPrint m1, PrettyPrint o1, Eq m1, Eq o1,
                PrettyPrint c2, PrettyPrint m2, PrettyPrint o2, Eq m2, Eq o2) => PrettyPrint (NaturalTransformation c1 m1 o1 c2 m2 o2) where
        pprint :: NaturalTransformation c1 m1 o1 c2 m2 o2 -> String
pprint NaturalTransformation c1 m1 o1 c2 m2 o2
nt = String
"NaturalTransformation(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Diagram c1 m1 o1 c2 m2 o2 -> String
forall a. PrettyPrint a => a -> String
pprint (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) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"->" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Diagram c1 m1 o1 c2 m2 o2 -> String
forall a. PrettyPrint a => a -> String
pprint (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) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ Map o1 m2 -> String
forall a. PrettyPrint a => a -> String
pprint (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
components NaturalTransformation c1 m1 o1 c2 m2 o2
nt) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
        
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                       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
        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
        @? :: NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Maybe (NaturalTransformation c1 m1 o1 c2 m2 o2)
(@?) NaturalTransformation c1 m1 o1 c2 m2 o2
nt2 NaturalTransformation c1 m1 o1 c2 m2 o2
nt1
            | NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m1 o1 c2 m2 o2
nt1 Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
== NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source NaturalTransformation c1 m1 o1 c2 m2 o2
nt2 Bool -> Bool -> Bool
&& (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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt1) c1 -> c1 -> Bool
forall a. Eq a => a -> a -> Bool
== (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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt2) Bool -> Bool -> Bool
&& (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 -> c2)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt1) c2 -> c2 -> Bool
forall a. Eq a => a -> a -> Bool
== (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 -> c2)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt2) = NaturalTransformation c1 m1 o1 c2 m2 o2
-> Maybe (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just NaturalTransformation{srcNT :: Diagram c1 m1 o1 c2 m2 o2
srcNT=NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source NaturalTransformation c1 m1 o1 c2 m2 o2
nt1, tgtNT :: Diagram c1 m1 o1 c2 m2 o2
tgtNT=NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m1 o1 c2 m2 o2
nt2, components :: Map o1 m2
components=Set (o1, m2) -> Map o1 m2
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(o1
o, (NaturalTransformation c1 m1 o1 c2 m2 o2
nt2 NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ o1
o) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ (NaturalTransformation c1 m1 o1 c2 m2 o2
nt1 NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ o1
o)) | o1
o <- c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set 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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt1)]}
            | Bool
otherwise = Maybe (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
    
    
    -- | Apply a 'NaturalTransformation' on an object of the source 'Diagram'.

    (=>$) :: (Eq o1) => NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
    =>$ :: forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
(=>$) NaturalTransformation c1 m1 o1 c2 m2 o2
nt o1
x = (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
components NaturalTransformation c1 m1 o1 c2 m2 o2
nt) Map o1 m2 -> o1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| o1
x
    
    -- | Compose horizontally 'NaturalTransformation's.

    (<=@<=) :: (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 m3 o3, Eq c3, Eq m3, Eq o3) => 
        NaturalTransformation c2 m2 o2 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    <=@<= :: forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(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 m3 o3, Eq c3, Eq m3, Eq o3) =>
NaturalTransformation c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
(<=@<=) NaturalTransformation c2 m2 o2 c3 m3 o3
nt2 NaturalTransformation c1 m1 o1 c2 m2 o2
nt1 = 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 m o. Morphism m o => m -> o
source NaturalTransformation c2 m2 o2 c3 m3 o3
nt2 Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
forall o2 m2 c2 c3 m3 o3 c1 m1 o1.
(Eq o2, Eq m2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source NaturalTransformation c1 m1 o1 c2 m2 o2
nt1, tgtNT :: Diagram c1 m1 o1 c3 m3 o3
tgtNT=NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
forall m o. Morphism m o => m -> o
target NaturalTransformation c2 m2 o2 c3 m3 o3
nt2 Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
forall o2 m2 c2 c3 m3 o3 c1 m1 o1.
(Eq o2, Eq m2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m1 o1 c2 m2 o2
nt1, components :: Map o1 m3
components = Set (o1, m3) -> Map o1 m3
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(o1
o, ((NaturalTransformation c2 m2 o2 c3 m3 o3
nt2 NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall m1 o1 c2 m2 o2 m3 o3 c3 c1.
(Morphism m1 o1, 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
<=@<- NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m1 o1 c2 m2 o2
nt1) NaturalTransformation c1 m1 o1 c3 m3 o3 -> o1 -> m3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ o1
o) m3 -> m3 -> m3
forall m o. Morphism m o => m -> m -> m
@ ((NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
forall m o. Morphism m o => m -> o
source NaturalTransformation c2 m2 o2 c3 m3 o3
nt2 Diagram c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c1 m1 o1 m2 o2 c2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
<-@<= NaturalTransformation c1 m1 o1 c2 m2 o2
nt1) NaturalTransformation c1 m1 o1 c3 m3 o3 -> o1 -> m3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ o1
o)) | o1
o <- c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set 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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt1)]}
    
    -- | Alias of ('<=@<=').

    horizontalComposition :: (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 m3 o3, Eq c3, Eq m3, Eq o3) =>  
        NaturalTransformation c2 m2 o2 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    horizontalComposition :: forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(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 m3 o3, Eq c3, Eq m3, Eq o3) =>
NaturalTransformation c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
horizontalComposition = NaturalTransformation c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(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 m3 o3, Eq c3, Eq m3, Eq o3) =>
NaturalTransformation c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
(<=@<=)
    
    -- | Left whiskering allows to compose a 'Diagram' with a 'NaturalTransformation'.

    (<=@<-) :: (                        Morphism m1 o1,
               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
    <=@<- :: forall m1 o1 c2 m2 o2 m3 o3 c3 c1.
(Morphism m1 o1, 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
(<=@<-) NaturalTransformation c2 m2 o2 c3 m3 o3
nt Diagram c1 m1 o1 c2 m2 o2
funct = 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 m o. Morphism m o => m -> o
source 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 o2 m2 c2 c3 m3 o3 c1 m1 o1.
(Eq o2, Eq m2) =>
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
funct,
                                                tgtNT :: Diagram c1 m1 o1 c3 m3 o3
tgtNT = (NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
forall m o. Morphism m o => m -> o
target 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 o2 m2 c2 c3 m3 o3 c1 m1 o1.
(Eq o2, Eq m2) =>
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
funct,
                                                components :: Map o1 m3
components = (NaturalTransformation c2 m2 o2 c3 m3 o3 -> Map o2 m3
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
components NaturalTransformation c2 m2 o2 c3 m3 o3
nt) Map o2 m3 -> Map o1 o2 -> Map o1 m3
forall b c a. Eq b => Map b c -> Map a b -> Map a c
|.| (Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
funct)
                                            }
    
    -- | Alias of ('<=@<-').

    leftWhiskering :: (                          Morphism m1 o1,
                        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
    leftWhiskering :: forall m1 o1 c2 m2 o2 m3 o3 c3 c1.
(Morphism m1 o1, 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
leftWhiskering = NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall m1 o1 c2 m2 o2 m3 o3 c3 c1.
(Morphism m1 o1, 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
(<=@<-)
    
    -- | Right whiskering allows to compose a 'NaturalTransformation' with a 'Diagram'.

    (<-@<=) :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                         Morphism m2 o2, Eq c2, Eq m2, Eq o2) => 
                Diagram c2 m2 o2 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    <-@<= :: forall c1 m1 o1 m2 o2 c2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
(<-@<=) Diagram c2 m2 o2 c3 m3 o3
funct NaturalTransformation c1 m1 o1 c2 m2 o2
nt = NaturalTransformation {  
                                                srcNT :: Diagram c1 m1 o1 c3 m3 o3
srcNT = Diagram c2 m2 o2 c3 m3 o3
funct Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
forall o2 m2 c2 c3 m3 o3 c1 m1 o1.
(Eq o2, Eq m2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source NaturalTransformation c1 m1 o1 c2 m2 o2
nt),
                                                tgtNT :: Diagram c1 m1 o1 c3 m3 o3
tgtNT = Diagram c2 m2 o2 c3 m3 o3
funct Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
forall o2 m2 c2 c3 m3 o3 c1 m1 o1.
(Eq o2, Eq m2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m1 o1 c2 m2 o2
nt),
                                                components :: Map o1 m3
components = (Diagram c2 m2 o2 c3 m3 o3 -> Map m2 m3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram c2 m2 o2 c3 m3 o3
funct) Map m2 m3 -> Map o1 m2 -> Map o1 m3
forall b c a. Eq b => Map b c -> Map a b -> Map a c
|.| (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
components NaturalTransformation c1 m1 o1 c2 m2 o2
nt)
                                             }
    
    -- | Alias of ('<-@<=').

    rightWhiskering :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                                 Morphism m2 o2, Eq c2, Eq m2, Eq o2) => 
        Diagram c2 m2 o2 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    rightWhiskering :: forall c1 m1 o1 m2 o2 c2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
rightWhiskering = Diagram c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c1 m1 o1 m2 o2 c2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
(<-@<=)
    
    -- | A datatype to represent a malformation of a 'NaturalTransformation'.

    data NaturalTransformationError c1 m1 o1 c2 m2 o2 = IncompatibleFunctorsSource{forall c1 m1 o1 c2 m2 o2.
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> c1
sourceCat :: c1, forall c1 m1 o1 c2 m2 o2.
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> c1
targetCat :: c1} -- ^ The source and target functors don't have the same source category.

                                                      | IncompatibleFunctorsTarget{forall c1 m1 o1 c2 m2 o2.
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> c2
sourceCat2 :: c2, forall c1 m1 o1 c2 m2 o2.
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> c2
targetCat2 :: c2} -- ^ The source and target functors don't have the same target category.

                                                      | NotTotal{forall c1 m1 o1 c2 m2 o2.
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> Set o1
domainNat :: Set o1, forall c1 m1 o1 c2 m2 o2.
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> Set o1
objectsCat :: Set o1} -- ^ The mapping from objects to morphisms is not total.

                                                      | NaturalityFail{forall c1 m1 o1 c2 m2 o2.
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> m1
originalMorphism :: m1} -- ^ A morphism does not close a commutative square.

                                                      deriving (NaturalTransformationError c1 m1 o1 c2 m2 o2
-> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> Bool
(NaturalTransformationError c1 m1 o1 c2 m2 o2
 -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> Bool)
-> (NaturalTransformationError c1 m1 o1 c2 m2 o2
    -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> Bool)
-> Eq (NaturalTransformationError 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, Eq o1, Eq m1) =>
NaturalTransformationError c1 m1 o1 c2 m2 o2
-> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2, Eq o1, Eq m1) =>
NaturalTransformationError c1 m1 o1 c2 m2 o2
-> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> Bool
== :: NaturalTransformationError c1 m1 o1 c2 m2 o2
-> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2, Eq o1, Eq m1) =>
NaturalTransformationError c1 m1 o1 c2 m2 o2
-> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> Bool
/= :: NaturalTransformationError c1 m1 o1 c2 m2 o2
-> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> Bool
Eq, Int -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> ShowS
[NaturalTransformationError c1 m1 o1 c2 m2 o2] -> ShowS
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> String
(Int -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> ShowS)
-> (NaturalTransformationError c1 m1 o1 c2 m2 o2 -> String)
-> ([NaturalTransformationError c1 m1 o1 c2 m2 o2] -> ShowS)
-> Show (NaturalTransformationError c1 m1 o1 c2 m2 o2)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show m1) =>
Int -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show m1) =>
[NaturalTransformationError c1 m1 o1 c2 m2 o2] -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show m1) =>
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> String
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show m1) =>
Int -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> ShowS
showsPrec :: Int -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> ShowS
$cshow :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show m1) =>
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> String
show :: NaturalTransformationError c1 m1 o1 c2 m2 o2 -> String
$cshowList :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show m1) =>
[NaturalTransformationError c1 m1 o1 c2 m2 o2] -> ShowS
showList :: [NaturalTransformationError c1 m1 o1 c2 m2 o2] -> ShowS
Show)
    
    
    -- | Check wether the structure of a 'NaturalTransformation' is respected.

    checkNaturalTransformation :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                                            Morphism m2 o2, Eq c2, Eq m2, Eq o2) => 
                        NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
    checkNaturalTransformation :: forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
checkNaturalTransformation NaturalTransformation c1 m1 o1 c2 m2 o2
nt
        | Bool
incompatibleFunctorsSource = NaturalTransformationError c1 m1 o1 c2 m2 o2
-> Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just IncompatibleFunctorsSource{sourceCat :: c1
sourceCat=(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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt), targetCat :: c1
targetCat=(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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt)}
        | Bool
incompatibleFunctorsTarget = NaturalTransformationError c1 m1 o1 c2 m2 o2
-> Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just IncompatibleFunctorsTarget{sourceCat2 :: c2
sourceCat2=(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 -> c2)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt), targetCat2 :: c2
targetCat2=(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 -> c2)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt)}
        | Bool
notTotal = NaturalTransformationError c1 m1 o1 c2 m2 o2
-> Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just NotTotal{domainNat :: Set o1
domainNat = (Map o1 m2 -> Set o1
forall k a. Map k a -> Set k
domain(Map o1 m2 -> Set o1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Set o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
components (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Set o1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Set o1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt), objectsCat :: Set o1
objectsCat = (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob(c1 -> Set o1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Set 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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Set o1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Set o1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt)}
        | (Bool -> Bool
not(Bool -> Bool) -> (Set m1 -> Bool) -> Set m1 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set m1 -> Bool
forall a. Set a -> Bool
Set.null)) Set m1
naturalityFail = NaturalTransformationError c1 m1 o1 c2 m2 o2
-> Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just NaturalityFail{originalMorphism :: m1
originalMorphism = Set m1 -> m1
forall a. Set a -> a
anElement Set m1
naturalityFail}
        | Bool
otherwise = Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
        where
            incompatibleFunctorsSource :: Bool
incompatibleFunctorsSource = (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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt) c1 -> c1 -> Bool
forall a. Eq a => a -> a -> Bool
/= (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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt)
            incompatibleFunctorsTarget :: Bool
incompatibleFunctorsTarget = (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 -> c2)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt) c2 -> c2 -> Bool
forall a. Eq a => a -> a -> Bool
/= (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 -> c2)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt)  
            notTotal :: Bool
notTotal = (Map o1 m2 -> Set o1
forall k a. Map k a -> Set k
domain(Map o1 m2 -> Set o1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Set o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
components (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Set o1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Set o1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt) Set o1 -> Set o1 -> Bool
forall a. Eq a => a -> a -> Bool
/= (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob(c1 -> Set o1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Set 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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Set o1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Set o1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt)
            naturalityFail :: Set m1
naturalityFail = [m1
f | m1
f <- (c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows(c1 -> Set m1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Set 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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Set m1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Set m1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt), (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m1 o1 c2 m2 o2
nt Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m1
f) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ (NaturalTransformation c1 m1 o1 c2 m2 o2
nt NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ (m1 -> o1
forall m o. Morphism m o => m -> o
source m1
f)) m2 -> m2 -> Bool
forall a. Eq a => a -> a -> Bool
/= (NaturalTransformation c1 m1 o1 c2 m2 o2
nt NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ (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
@ (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source NaturalTransformation c1 m1 o1 c2 m2 o2
nt Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m1
f)]
    
    -- | The smart constructor of 'NaturalTransformation'. Checks wether the structure is correct.

    naturalTransformation :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                                       Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
                            Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Map o1 m2 -> Either (NaturalTransformationError c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2)
    naturalTransformation :: forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> Either
     (NaturalTransformationError c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
naturalTransformation Diagram c1 m1 o1 c2 m2 o2
s Diagram c1 m1 o1 c2 m2 o2
t Map o1 m2
c
        | Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2) -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
check = NaturalTransformation c1 m1 o1 c2 m2 o2
-> Either
     (NaturalTransformationError c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall a b. b -> Either a b
Right NaturalTransformation c1 m1 o1 c2 m2 o2
nt
        | Bool
otherwise = NaturalTransformationError c1 m1 o1 c2 m2 o2
-> Either
     (NaturalTransformationError c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall a b. a -> Either a b
Left NaturalTransformationError c1 m1 o1 c2 m2 o2
err
        where
            nt :: NaturalTransformation c1 m1 o1 c2 m2 o2
nt = NaturalTransformation{srcNT :: Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
s,tgtNT :: Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
t,components :: Map o1 m2
components=Map o1 m2
c}
            check :: Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
check = NaturalTransformation c1 m1 o1 c2 m2 o2
-> Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
checkNaturalTransformation NaturalTransformation c1 m1 o1 c2 m2 o2
nt
            Just NaturalTransformationError c1 m1 o1 c2 m2 o2
err = Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
check
    
    -- | Unsafe constructor of 'NaturalTransformation' for performance purposes. It does not check the structure of the 'NaturalTransformation'.

    --

    -- Use this constructor only if the 'NaturalTransformation' is necessarily well formed.

    unsafeNaturalTransformation :: Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Map o1 m2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
    unsafeNaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation Diagram c1 m1 o1 c2 m2 o2
s Diagram c1 m1 o1 c2 m2 o2
t Map o1 m2
c = NaturalTransformation{srcNT :: Diagram c1 m1 o1 c2 m2 o2
srcNT = Diagram c1 m1 o1 c2 m2 o2
s, tgtNT :: Diagram c1 m1 o1 c2 m2 o2
tgtNT = Diagram c1 m1 o1 c2 m2 o2
t, components :: Map o1 m2
components = Map o1 m2
c}
    
    -- Functor Category

    
    
    -- | A 'FunctorCategory' /D/^/C/ where /C/ is a 'FiniteCategory' and /D/ is a 'Category' has 'Diagram's @F : C -> D@ as objects and 'NaturalTransformation's between them as morphisms. 'NaturalTransformation's compose vertically in this category.

    data FunctorCategory c1 m1 o1 c2 m2 o2 = FunctorCategory c1 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
$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
/= :: 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 -> String
(Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> ShowS)
-> (FunctorCategory c1 m1 o1 c2 m2 o2 -> String)
-> ([FunctorCategory c1 m1 o1 c2 m2 o2] -> ShowS)
-> Show (FunctorCategory c1 m1 o1 c2 m2 o2)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([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 -> String
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> ShowS
showsPrec :: Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> ShowS
$cshow :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
FunctorCategory c1 m1 o1 c2 m2 o2 -> String
show :: FunctorCategory c1 m1 o1 c2 m2 o2 -> String
$cshowList :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
[FunctorCategory c1 m1 o1 c2 m2 o2] -> ShowS
showList :: [FunctorCategory c1 m1 o1 c2 m2 o2] -> ShowS
Show)
    
    instance (PrettyPrint c1, PrettyPrint c2) => PrettyPrint (FunctorCategory c1 m1 o1 c2 m2 o2) where
        pprint :: FunctorCategory c1 m1 o1 c2 m2 o2 -> String
pprint (FunctorCategory c1
c c2
d) = String
"FunctorCategory(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ c1 -> String
forall a. PrettyPrint a => a -> String
pprint c1
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ c2 -> String
forall a. PrettyPrint a => a -> String
pprint c2
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
        
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                    Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
        Category (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) where
        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
c c2
d) Diagram c1 m1 o1 c2 m2 o2
funct
            | 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
funct c1 -> c1 -> Bool
forall a. Eq a => a -> a -> Bool
== c1
c Bool -> Bool -> Bool
&& 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
funct c2 -> c2 -> Bool
forall a. Eq a => a -> a -> Bool
== c2
d = NaturalTransformation{srcNT :: Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
funct, tgtNT :: Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
funct, components :: Map o1 m2
components=Set (o1, m2) -> Map o1 m2
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(o1
o, c2 -> o2 -> m2
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c2
d (Diagram c1 m1 o1 c2 m2 o2
funct Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
o))| o1
o <- (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob(c1 -> Set o1)
-> (Diagram c1 m1 o1 c2 m2 o2 -> c1)
-> Diagram c1 m1 o1 c2 m2 o2
-> Set 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 -> Set o1)
-> Diagram c1 m1 o1 c2 m2 o2 -> Set o1
forall a b. (a -> b) -> a -> b
$ Diagram c1 m1 o1 c2 m2 o2
funct)]}
            | Bool
otherwise = String -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall a. HasCallStack => String -> a
error String
"Math.Categories.FunctorCategory.identity: functor not in the functor category."
        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
-> Set (NaturalTransformation c1 m1 o1 c2 m2 o2)
ar (FunctorCategory c1
c c2
d) Diagram c1 m1 o1 c2 m2 o2
s Diagram c1 m1 o1 c2 m2 o2
t
            | 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 c1 -> c1 -> Bool
forall a. Eq a => a -> a -> Bool
== 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
t Bool -> Bool -> Bool
&& 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
s c2 -> c2 -> Bool
forall a. Eq a => a -> a -> Bool
== 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
t = (Set (NaturalTransformationError c1 m1 o1 c2 m2 o2),
 Set (NaturalTransformation c1 m1 o1 c2 m2 o2))
-> Set (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall a b. (a, b) -> b
snd((Set (NaturalTransformationError c1 m1 o1 c2 m2 o2),
  Set (NaturalTransformation c1 m1 o1 c2 m2 o2))
 -> Set (NaturalTransformation c1 m1 o1 c2 m2 o2))
-> (Set
      (Either
         (NaturalTransformationError c1 m1 o1 c2 m2 o2)
         (NaturalTransformation c1 m1 o1 c2 m2 o2))
    -> (Set (NaturalTransformationError c1 m1 o1 c2 m2 o2),
        Set (NaturalTransformation c1 m1 o1 c2 m2 o2)))
-> Set
     (Either
        (NaturalTransformationError c1 m1 o1 c2 m2 o2)
        (NaturalTransformation c1 m1 o1 c2 m2 o2))
-> Set (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set
  (Either
     (NaturalTransformationError c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2))
-> (Set (NaturalTransformationError c1 m1 o1 c2 m2 o2),
    Set (NaturalTransformation c1 m1 o1 c2 m2 o2))
forall a b. Set (Either a b) -> (Set a, Set b)
Set.catEither) (Set
   (Either
      (NaturalTransformationError c1 m1 o1 c2 m2 o2)
      (NaturalTransformation c1 m1 o1 c2 m2 o2))
 -> Set (NaturalTransformation c1 m1 o1 c2 m2 o2))
-> Set
     (Either
        (NaturalTransformationError c1 m1 o1 c2 m2 o2)
        (NaturalTransformation c1 m1 o1 c2 m2 o2))
-> Set (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall a b. (a -> b) -> a -> b
$ [Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> Either
     (NaturalTransformationError c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> Either
     (NaturalTransformationError c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
naturalTransformation Diagram c1 m1 o1 c2 m2 o2
s Diagram c1 m1 o1 c2 m2 o2
t Map o1 m2
mapCompo | Map o1 m2
mapCompo <- Set (Map o1 m2)
mapComponent]
            | Bool
otherwise = String -> Set (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall a. HasCallStack => String -> a
error String
"Math.Categories.FunctorCategory.ar: incompatible functors"
            where
                mapComponent :: Set (Map o1 m2)
mapComponent = [(o1, m2)] -> Map o1 m2
forall k v. AssociationList k v -> Map k v
weakMap ([(o1, m2)] -> Map o1 m2) -> Set [(o1, m2)] -> Set (Map o1 m2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Set (o1, m2)] -> Set [(o1, m2)]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets [(\m2
x -> (o1
o,m2
x)) (m2 -> (o1, m2)) -> Set m2 -> Set (o1, m2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c2 -> o2 -> o2 -> Set m2
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set 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
s) (Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
s Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| o1
o) (Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
t Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| o1
o)) | o1
o <- (Set o1 -> [o1]
forall a. Eq a => Set a -> [a]
setToList (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob(c1 -> Set o1)
-> (Diagram c1 m1 o1 c2 m2 o2 -> c1)
-> Diagram c1 m1 o1 c2 m2 o2
-> Set 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 -> Set o1)
-> Diagram c1 m1 o1 c2 m2 o2 -> Set o1
forall a b. (a -> b) -> a -> b
$ Diagram c1 m1 o1 c2 m2 o2
s))]
                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
                
                
    
    -- | A  'FunctorCategory' where the target category is finite allows to enumerate all 'Diagram's thus making it a 'FiniteCategory'.

    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) =>
        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
-> Set (Diagram c1 m1 o1 c2 m2 o2)
ob (FunctorCategory c1
s c2
t) = (Set (DiagramError c1 m1 o1 c2 m2 o2),
 Set (Diagram c1 m1 o1 c2 m2 o2))
-> Set (Diagram c1 m1 o1 c2 m2 o2)
forall a b. (a, b) -> b
snd((Set (DiagramError c1 m1 o1 c2 m2 o2),
  Set (Diagram c1 m1 o1 c2 m2 o2))
 -> Set (Diagram c1 m1 o1 c2 m2 o2))
-> (Set
      (Either
         (DiagramError c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2))
    -> (Set (DiagramError c1 m1 o1 c2 m2 o2),
        Set (Diagram c1 m1 o1 c2 m2 o2)))
-> Set
     (Either
        (DiagramError c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2))
-> Set (Diagram c1 m1 o1 c2 m2 o2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set
  (Either
     (DiagramError c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2))
-> (Set (DiagramError c1 m1 o1 c2 m2 o2),
    Set (Diagram c1 m1 o1 c2 m2 o2))
forall a b. Set (Either a b) -> (Set a, Set b)
Set.catEither) (Set
   (Either
      (DiagramError c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2))
 -> Set (Diagram c1 m1 o1 c2 m2 o2))
-> Set
     (Either
        (DiagramError c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2))
-> Set (Diagram c1 m1 o1 c2 m2 o2)
forall a b. (a -> b) -> a -> b
$ [c1
-> c2
-> Map o1 o2
-> Map m1 m2
-> Either
     (DiagramError c1 m1 o1 c2 m2 o2) (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
-> Map o1 o2
-> Map m1 m2
-> Either
     (DiagramError c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
diagram c1
s c2
t Map o1 o2
appO Map m1 m2
appF | Map o1 o2
appO <- Set (Map o1 o2)
appObj, Map m1 m2
appF <- ((([Map m1 m2] -> Map m1 m2) -> Set [Map m1 m2] -> Set (Map m1 m2)
forall a b. (a -> b) -> Set a -> Set b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Map m1 m2] -> Map m1 m2) -> Set [Map m1 m2] -> Set (Map m1 m2))
-> ([Map m1 m2] -> Map m1 m2) -> Set [Map m1 m2] -> Set (Map m1 m2)
forall a b. (a -> b) -> a -> b
$ ([Map m1 m2] -> Map m1 m2
forall k a. Eq k => [Map k a] -> Map k a
Map.unions))(Set [Map m1 m2] -> Set (Map m1 m2))
-> ([Set (Map m1 m2)] -> Set [Map m1 m2])
-> [Set (Map m1 m2)]
-> Set (Map m1 m2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[Set (Map m1 m2)] -> Set [Map m1 m2]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets) [o1 -> o1 -> Map o1 o2 -> Set (Map m1 m2)
twoObjToMaps o1
a o1
b Map o1 o2
appO| o1
a <- (Set o1 -> [o1]
forall a. Eq a => Set a -> [a]
setToList (Set o1 -> [o1]) -> Set o1 -> [o1]
forall a b. (a -> b) -> a -> b
$ c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
s), o1
b <- (Set o1 -> [o1]
forall a. Eq a => Set a -> [a]
setToList (Set o1 -> [o1]) -> Set o1 -> [o1]
forall a b. (a -> b) -> a -> b
$ c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
s)]]
            where
                appObj :: Set (Map o1 o2)
appObj = Set o1 -> Set o2 -> Set (Map o1 o2)
forall a b. (Eq a, Eq b) => Set a -> Set b -> Set (Map a b)
Map.enumerateMaps (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
s) (c2 -> Set o2
forall c m o. FiniteCategory c m o => c -> Set o
ob c2
t)
                twoObjToMaps :: o1 -> o1 -> Map o1 o2 -> Set (Map m1 m2)
twoObjToMaps o1
a o1
b Map o1 o2
appO = Set m1 -> Set m2 -> Set (Map m1 m2)
forall a b. (Eq a, Eq b) => Set a -> Set b -> Set (Map a b)
Map.enumerateMaps (c1 -> o1 -> o1 -> Set m1
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c1
s o1
a o1
b) (c2 -> o2 -> o2 -> Set m2
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c2
t (Map o1 o2
appO Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| o1
a) (Map o1 o2
appO Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| o1
b))

    
    -- | A 'FunctorCategory' /D/^/C/ precomposed by a functor @F : B -> C@ where /B/ and /C/ are 'FiniteCategory' and /D/ is a 'Category'.

    --

    -- It has 'Diagram's @G o F : B -> D@ as objects and 'NaturalTransformation's between them as morphisms. 'NaturalTransformation's compose vertically in this category.

    data PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 = PrecomposedFunctorCategory (Diagram c1 m1 o1 c2 m2 o2) c3 deriving (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
(PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> Eq (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2, Eq c3) =>
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2, Eq c3) =>
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
== :: PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2, Eq c3) =>
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
/= :: PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
Eq, Int
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
[PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int
 -> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS)
-> (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> String)
-> ([PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3]
    -> ShowS)
-> Show (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3) =>
Int
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3) =>
[PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3) =>
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3) =>
Int
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
showsPrec :: Int
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
$cshow :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3) =>
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
show :: PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cshowList :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3) =>
[PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
showList :: [PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
Show)
    
    instance   (PrettyPrint c1, PrettyPrint m1, PrettyPrint o1, Eq m1, Eq o1,
                PrettyPrint c2, PrettyPrint m2, PrettyPrint o2, Eq m2, Eq o2,
                PrettyPrint c3) => PrettyPrint (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) where
        pprint :: PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprint (PrecomposedFunctorCategory Diagram c1 m1 o1 c2 m2 o2
diag c3
d) = String
"PrecomposedFunctorCategory(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Diagram c1 m1 o1 c2 m2 o2 -> String
forall a. PrettyPrint a => a -> String
pprint Diagram c1 m1 o1 c2 m2 o2
diag String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ c3 -> String
forall a. PrettyPrint a => a -> String
pprint c3
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
        
    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,
                    Category c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        Category (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (NaturalTransformation c1 m1 o1 c3 m3 o3) (Diagram c1 m1 o1 c3 m3 o3) where
        identity :: Morphism
  (NaturalTransformation c1 m1 o1 c3 m3 o3)
  (Diagram c1 m1 o1 c3 m3 o3) =>
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
identity (PrecomposedFunctorCategory Diagram c1 m1 o1 c2 m2 o2
diag c3
c3) = FunctorCategory c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (c1 -> c3 -> FunctorCategory c1 m1 o1 c3 m3 o3
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
c3)
        ar :: Morphism
  (NaturalTransformation c1 m1 o1 c3 m3 o3)
  (Diagram c1 m1 o1 c3 m3 o3) =>
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Set (NaturalTransformation c1 m1 o1 c3 m3 o3)
ar (PrecomposedFunctorCategory Diagram c1 m1 o1 c2 m2 o2
diag c3
c3) = FunctorCategory c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Set (NaturalTransformation c1 m1 o1 c3 m3 o3)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar (c1 -> c3 -> FunctorCategory c1 m1 o1 c3 m3 o3
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
c3)
                
                
    
    -- | A 'PrecomposedFunctorCategory' where the target category is finite allows to enumerate all 'Diagram's thus making it a 'FiniteCategory'.

    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,
              FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        FiniteCategory (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (NaturalTransformation c1 m1 o1 c3 m3 o3) (Diagram c1 m1 o1 c3 m3 o3) where
        ob :: PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Set (Diagram c1 m1 o1 c3 m3 o3)
ob (PrecomposedFunctorCategory Diagram c1 m1 o1 c2 m2 o2
diag c3
c3) = (Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
forall o2 m2 c2 c3 m3 o3 c1 m1 o1.
(Eq o2, Eq m2) =>
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) (Diagram c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c3 m3 o3)
-> Set (Diagram c2 m2 o2 c3 m3 o3)
-> Set (Diagram c1 m1 o1 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (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 (c2 -> c3 -> FunctorCategory c2 m2 o2 c3 m3 o3
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
c3))
        
        
    -- | A 'FunctorCategory' /D/^/C/ postcomposed by a functor @F : D -> E@ where /C/ is a 'FiniteCategory' and /D/  and /E/ are 'Category'. 

    --

    -- It has 'Diagram's @ F o G : C -> E@ as objects and 'NaturalTransformation's between them as morphisms. 'NaturalTransformation's compose vertically in this category.

    data PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 = PostcomposedFunctorCategory (Diagram c2 m2 o2 c3 m3 o3) c1 deriving (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
(PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> Eq (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c2, Eq c3, Eq o2, Eq o3, Eq m2, Eq m3, Eq c1) =>
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c2, Eq c3, Eq o2, Eq o3, Eq m2, Eq m3, Eq c1) =>
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
== :: PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c2, Eq c3, Eq o2, Eq o3, Eq m2, Eq m3, Eq c1) =>
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
/= :: PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
Eq, Int
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
[PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int
 -> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS)
-> (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> String)
-> ([PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3]
    -> ShowS)
-> Show (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show c3, Show o2, Show o3, Show m2, Show m3, Show c1) =>
Int
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show c3, Show o2, Show o3, Show m2, Show m3, Show c1) =>
[PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show c3, Show o2, Show o3, Show m2, Show m3, Show c1) =>
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show c3, Show o2, Show o3, Show m2, Show m3, Show c1) =>
Int
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
showsPrec :: Int
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
$cshow :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show c3, Show o2, Show o3, Show m2, Show m3, Show c1) =>
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
show :: PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cshowList :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show c3, Show o2, Show o3, Show m2, Show m3, Show c1) =>
[PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
showList :: [PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
Show)
    
    instance   (PrettyPrint c1,
                PrettyPrint c2, PrettyPrint m2, PrettyPrint o2, Eq m2, Eq o2,
                PrettyPrint c3, PrettyPrint m3, PrettyPrint o3, Eq m3, Eq o3) => PrettyPrint (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) where
        pprint :: PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprint (PostcomposedFunctorCategory Diagram c2 m2 o2 c3 m3 o3
diag c1
d) = String
"PostcomposedFunctorCategory(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Diagram c2 m2 o2 c3 m3 o3 -> String
forall a. PrettyPrint a => a -> String
pprint Diagram c2 m2 o2 c3 m3 o3
diag String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ c1 -> String
forall a. PrettyPrint a => a -> String
pprint c1
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
        
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                    Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
                    Category c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        Category (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (NaturalTransformation c1 m1 o1 c3 m3 o3) (Diagram c1 m1 o1 c3 m3 o3) where
        identity :: Morphism
  (NaturalTransformation c1 m1 o1 c3 m3 o3)
  (Diagram c1 m1 o1 c3 m3 o3) =>
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
identity (PostcomposedFunctorCategory Diagram c2 m2 o2 c3 m3 o3
diag c1
c1) = FunctorCategory c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (c1 -> c3 -> FunctorCategory c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory c1
c1 (Diagram c2 m2 o2 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c2 m2 o2 c3 m3 o3
diag))
        ar :: Morphism
  (NaturalTransformation c1 m1 o1 c3 m3 o3)
  (Diagram c1 m1 o1 c3 m3 o3) =>
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Set (NaturalTransformation c1 m1 o1 c3 m3 o3)
ar (PostcomposedFunctorCategory Diagram c2 m2 o2 c3 m3 o3
diag c1
c1) = FunctorCategory c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Set (NaturalTransformation c1 m1 o1 c3 m3 o3)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar (c1 -> c3 -> FunctorCategory c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory c1
c1 (Diagram c2 m2 o2 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c2 m2 o2 c3 m3 o3
diag))
                
                
    
    -- | A 'PostcomposedFunctorCategory' where the target category is finite allows to enumerate all 'Diagram's thus making it a 'FiniteCategory'.

    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,
              FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        FiniteCategory (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (NaturalTransformation c1 m1 o1 c3 m3 o3) (Diagram c1 m1 o1 c3 m3 o3) where
        ob :: PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Set (Diagram c1 m1 o1 c3 m3 o3)
ob (PostcomposedFunctorCategory Diagram c2 m2 o2 c3 m3 o3
diag c1
c1) = (Diagram c2 m2 o2 c3 m3 o3
diag Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
forall o2 m2 c2 c3 m3 o3 c1 m1 o1.
(Eq o2, Eq m2) =>
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 -> Diagram c1 m1 o1 c3 m3 o3)
-> Set (Diagram c1 m1 o1 c2 m2 o2)
-> Set (Diagram c1 m1 o1 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FunctorCategory c1 m1 o1 c2 m2 o2
-> Set (Diagram c1 m1 o1 c2 m2 o2)
forall c m o. FiniteCategory c m o => c -> Set o
ob (c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory c1
c1 (Diagram c2 m2 o2 c3 m3 o3 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c2 m2 o2 c3 m3 o3
diag))) 
              
    -- | The insertion functor from the 'FullSubcategory' to the original category.

    insertionFunctor1 :: (Category c m o, Morphism m o, Eq o) => FullSubcategory c m o -> Diagram (FullSubcategory c m o) m o c m o
    insertionFunctor1 :: forall c m o.
(Category c m o, Morphism m o, Eq o) =>
FullSubcategory c m o -> Diagram (FullSubcategory c m o) m o c m o
insertionFunctor1 sc :: FullSubcategory c m o
sc@(FullSubcategory c
c Set o
s) = Diagram{src :: FullSubcategory c m o
src=FullSubcategory c m o
sc,tgt :: c
tgt=c
c,omap :: Map o o
omap=(o -> o) -> Set o -> Map o o
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction o -> o
forall a. a -> a
id Set o
s, mmap :: Map m m
mmap=(m -> m) -> Set m -> Map m m
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction m -> m
forall a. a -> a
id (FullSubcategory c m o -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows FullSubcategory c m o
sc)}
    
    -- | The insertion functor from the 'InheritedFullSubcategory' to the original category.

    insertionFunctor2 :: (Category c m o, Morphism m o, Eq o) => InheritedFullSubcategory c m o -> Diagram (InheritedFullSubcategory c m o) m o c m o
    insertionFunctor2 :: forall c m o.
(Category c m o, Morphism m o, Eq o) =>
InheritedFullSubcategory c m o
-> Diagram (InheritedFullSubcategory c m o) m o c m o
insertionFunctor2 sc :: InheritedFullSubcategory c m o
sc@(InheritedFullSubcategory c
c Set o
s) = Diagram{src :: InheritedFullSubcategory c m o
src=InheritedFullSubcategory c m o
sc,tgt :: c
tgt=c
c,omap :: Map o o
omap=(o -> o) -> Set o -> Map o o
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction o -> o
forall a. a -> a
id Set o
s, mmap :: Map m m
mmap=(m -> m) -> Set m -> Map m m
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction m -> m
forall a. a -> a
id (InheritedFullSubcategory c m o -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows InheritedFullSubcategory c m o
sc)}