{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE MonadComprehensions  #-}
{-# LANGUAGE MultiParamTypeClasses  #-}

{-| 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. See 'FinCat' for a homogeneous ones.

'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. Also note that a 'Diagram' does not need to contain the mapping of all morphisms from the source category, it may only contain a mapping for the generating morphisms of the source category. 

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,
    finiteDiagram,
    -- ** Operators

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

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

    insertionFunctor1,
    insertionFunctor2,
    -- ** Diagram construction helper

    completeDiagram,
    pickRandomDiagram,
    -- ** Other diagram functions

    inverseDiagram,
    unsafeInverseDiagram,
    -- * Natural transformation

    NaturalTransformation,
    -- ** Getter

    components,
    -- ** Check structure

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

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

    indexingCategory,
    -- * 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              Data.Simplifiable
    
    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)
    
    import              GHC.Generics
    
    
    -- | 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 constructors 'diagram' or 'finiteDiagram' which check the structure of the 'Diagram' at construction. See also the useful function 'completeDiagram'.

    --

    -- You can omit the mapping of generated morphisms of the source category.

    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, generated morphisms can be omitted.

                                              } deriving (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, (forall x.
 Diagram c1 m1 o1 c2 m2 o2 -> Rep (Diagram c1 m1 o1 c2 m2 o2) x)
-> (forall x.
    Rep (Diagram c1 m1 o1 c2 m2 o2) x -> Diagram c1 m1 o1 c2 m2 o2)
-> Generic (Diagram c1 m1 o1 c2 m2 o2)
forall x.
Rep (Diagram c1 m1 o1 c2 m2 o2) x -> Diagram c1 m1 o1 c2 m2 o2
forall x.
Diagram c1 m1 o1 c2 m2 o2 -> Rep (Diagram c1 m1 o1 c2 m2 o2) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c1 m1 o1 c2 m2 o2 x.
Rep (Diagram c1 m1 o1 c2 m2 o2) x -> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2 x.
Diagram c1 m1 o1 c2 m2 o2 -> Rep (Diagram c1 m1 o1 c2 m2 o2) x
$cfrom :: forall c1 m1 o1 c2 m2 o2 x.
Diagram c1 m1 o1 c2 m2 o2 -> Rep (Diagram c1 m1 o1 c2 m2 o2) x
from :: forall x.
Diagram c1 m1 o1 c2 m2 o2 -> Rep (Diagram c1 m1 o1 c2 m2 o2) x
$cto :: forall c1 m1 o1 c2 m2 o2 x.
Rep (Diagram c1 m1 o1 c2 m2 o2) x -> Diagram c1 m1 o1 c2 m2 o2
to :: forall x.
Rep (Diagram c1 m1 o1 c2 m2 o2) x -> Diagram c1 m1 o1 c2 m2 o2
Generic, Int -> Int -> String -> Diagram c1 m1 o1 c2 m2 o2 -> String
Int -> Diagram c1 m1 o1 c2 m2 o2 -> String
(Int -> Diagram c1 m1 o1 c2 m2 o2 -> String)
-> (Int -> Int -> String -> Diagram c1 m1 o1 c2 m2 o2 -> String)
-> (Int -> Diagram c1 m1 o1 c2 m2 o2 -> String)
-> PrettyPrint (Diagram c1 m1 o1 c2 m2 o2)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
 PrettyPrint m1, PrettyPrint m2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Int -> Int -> String -> Diagram c1 m1 o1 c2 m2 o2 -> String
forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
 PrettyPrint m1, PrettyPrint m2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Int -> Diagram c1 m1 o1 c2 m2 o2 -> String
$cpprint :: forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
 PrettyPrint m1, PrettyPrint m2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Int -> Diagram c1 m1 o1 c2 m2 o2 -> String
pprint :: Int -> Diagram c1 m1 o1 c2 m2 o2 -> String
$cpprintWithIndentations :: forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
 PrettyPrint m1, PrettyPrint m2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Int -> Int -> String -> Diagram c1 m1 o1 c2 m2 o2 -> String
pprintWithIndentations :: Int -> Int -> String -> Diagram c1 m1 o1 c2 m2 o2 -> String
$cpprintIndent :: forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
 PrettyPrint m1, PrettyPrint m2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Int -> Diagram c1 m1 o1 c2 m2 o2 -> String
pprintIndent :: Int -> Diagram c1 m1 o1 c2 m2 o2 -> String
PrettyPrint, Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
(Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Simplifiable (Diagram c1 m1 o1 c2 m2 o2)
forall a. (a -> a) -> Simplifiable a
forall c1 m1 o1 c2 m2 o2.
(Simplifiable c1, Simplifiable c2, Simplifiable o1,
 Simplifiable o2, Simplifiable m1, Simplifiable m2, Eq o1, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
$csimplify :: forall c1 m1 o1 c2 m2 o2.
(Simplifiable c1, Simplifiable c2, Simplifiable o1,
 Simplifiable o2, Simplifiable m1, Simplifiable m2, Eq o1, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
simplify :: Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
Simplifiable)
    
    instance (Eq c1, Eq m1, Eq o1, Eq c2, Eq m2, Eq o2, FiniteCategory c1 m1 o1, Morphism m1 o1) => Eq (Diagram c1 m1 o1 c2 m2 o2) where
        Diagram c1 m1 o1 c2 m2 o2
d1 == :: Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
== Diagram c1 m1 o1 c2 m2 o2
d2 = 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
d1 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
d2 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
d1 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
d2 Bool -> Bool -> Bool
&& 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
d1 Map o1 o2 -> Map o1 o2 -> Bool
forall a. Eq a => a -> a -> Bool
== 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
d2 Bool -> Bool -> Bool
&& Map m1 m2 -> Set m1 -> Map m1 m2
forall k a. Eq k => Map k a -> Set k -> Map k a
Map.restrictKeys (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
d1) (c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows (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
d1)) Map m1 m2 -> Map m1 m2 -> Bool
forall a. Eq a => a -> a -> Bool
== Map m1 m2 -> Set m1 -> Map m1 m2
forall k a. Eq k => Map k a -> Set k -> Map k a
Map.restrictKeys (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
d2) (c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows (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
d2))     
    
    -- | 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.

    (->£) :: (Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) => Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
    ->£ :: forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
(->£) Diagram c1 m1 o1 c2 m2 o2
f m1
x
        | Maybe m2 -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe m2
mapped = [m2] -> m2
forall m o. Morphism m o => [m] -> m
compose ([m2] -> m2) -> [m2] -> m2
forall a b. (a -> b) -> a -> b
$ (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 -> 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 (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) m1
x
        | Bool
otherwise = m2
y
        where
            mapped :: Maybe m2
mapped = 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 -> Maybe m2
forall k v. Eq k => Map k v -> k -> Maybe v
|?| m1
x
            Just m2
y = Maybe m2
mapped
    
    -- | Compose two 'Diagram's.

    (<-@<-) :: (Category c1 m1 o1, Morphism m1 o1, Eq m1,
                Category c2 m2 o2, Morphism m2 o2, Eq o2, Eq m2,
                Morphism m3 o3) => Diagram c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
    <-@<- :: forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, Category c2 m2 o2,
 Morphism m2 o2, Eq o2, Eq m2, Morphism m3 o3) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
(<-@<-) Diagram 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 = Map m1 m3
mm}
        where
            mm :: Map m1 m3
mm = Set (m1, m3) -> Map m1 m3
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(m1
x, Diagram c2 m2 o2 c3 m3 o3
g Diagram c2 m2 o2 c3 m3 o3 -> m2 -> m3
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ (Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m1
x)) | m1
x <- Map m1 m2 -> Set m1
forall k v. Map k v -> Set k
keys' (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, (forall x.
 DiagramError c1 m1 o1 c2 m2 o2
 -> Rep (DiagramError c1 m1 o1 c2 m2 o2) x)
-> (forall x.
    Rep (DiagramError c1 m1 o1 c2 m2 o2) x
    -> DiagramError c1 m1 o1 c2 m2 o2)
-> Generic (DiagramError c1 m1 o1 c2 m2 o2)
forall x.
Rep (DiagramError c1 m1 o1 c2 m2 o2) x
-> DiagramError c1 m1 o1 c2 m2 o2
forall x.
DiagramError c1 m1 o1 c2 m2 o2
-> Rep (DiagramError c1 m1 o1 c2 m2 o2) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c1 m1 o1 c2 m2 o2 x.
Rep (DiagramError c1 m1 o1 c2 m2 o2) x
-> DiagramError c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2 x.
DiagramError c1 m1 o1 c2 m2 o2
-> Rep (DiagramError c1 m1 o1 c2 m2 o2) x
$cfrom :: forall c1 m1 o1 c2 m2 o2 x.
DiagramError c1 m1 o1 c2 m2 o2
-> Rep (DiagramError c1 m1 o1 c2 m2 o2) x
from :: forall x.
DiagramError c1 m1 o1 c2 m2 o2
-> Rep (DiagramError c1 m1 o1 c2 m2 o2) x
$cto :: forall c1 m1 o1 c2 m2 o2 x.
Rep (DiagramError c1 m1 o1 c2 m2 o2) x
-> DiagramError c1 m1 o1 c2 m2 o2
to :: forall x.
Rep (DiagramError c1 m1 o1 c2 m2 o2) x
-> DiagramError c1 m1 o1 c2 m2 o2
Generic, DiagramError c1 m1 o1 c2 m2 o2 -> DiagramError c1 m1 o1 c2 m2 o2
(DiagramError c1 m1 o1 c2 m2 o2 -> DiagramError c1 m1 o1 c2 m2 o2)
-> Simplifiable (DiagramError c1 m1 o1 c2 m2 o2)
forall a. (a -> a) -> Simplifiable a
forall c1 m1 o1 c2 m2 o2.
(Simplifiable o1, Simplifiable m1, Simplifiable o2,
 Simplifiable m2, Eq o1, Eq m1, Eq o2, Eq m2) =>
DiagramError c1 m1 o1 c2 m2 o2 -> DiagramError c1 m1 o1 c2 m2 o2
$csimplify :: forall c1 m1 o1 c2 m2 o2.
(Simplifiable o1, Simplifiable m1, Simplifiable o2,
 Simplifiable m2, Eq o1, Eq m1, Eq o2, Eq m2) =>
DiagramError c1 m1 o1 c2 m2 o2 -> DiagramError c1 m1 o1 c2 m2 o2
simplify :: DiagramError c1 m1 o1 c2 m2 o2 -> DiagramError c1 m1 o1 c2 m2 o2
Simplifiable, Int -> Int -> String -> DiagramError c1 m1 o1 c2 m2 o2 -> String
Int -> DiagramError c1 m1 o1 c2 m2 o2 -> String
(Int -> DiagramError c1 m1 o1 c2 m2 o2 -> String)
-> (Int
    -> Int -> String -> DiagramError c1 m1 o1 c2 m2 o2 -> String)
-> (Int -> DiagramError c1 m1 o1 c2 m2 o2 -> String)
-> PrettyPrint (DiagramError c1 m1 o1 c2 m2 o2)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c1 m1 o1 c2 m2 o2.
(PrettyPrint o1, PrettyPrint m1, PrettyPrint o2, PrettyPrint m2,
 Eq o1, Eq m1, Eq o2, Eq m2) =>
Int -> Int -> String -> DiagramError c1 m1 o1 c2 m2 o2 -> String
forall c1 m1 o1 c2 m2 o2.
(PrettyPrint o1, PrettyPrint m1, PrettyPrint o2, PrettyPrint m2,
 Eq o1, Eq m1, Eq o2, Eq m2) =>
Int -> DiagramError c1 m1 o1 c2 m2 o2 -> String
$cpprint :: forall c1 m1 o1 c2 m2 o2.
(PrettyPrint o1, PrettyPrint m1, PrettyPrint o2, PrettyPrint m2,
 Eq o1, Eq m1, Eq o2, Eq m2) =>
Int -> DiagramError c1 m1 o1 c2 m2 o2 -> String
pprint :: Int -> DiagramError c1 m1 o1 c2 m2 o2 -> String
$cpprintWithIndentations :: forall c1 m1 o1 c2 m2 o2.
(PrettyPrint o1, PrettyPrint m1, PrettyPrint o2, PrettyPrint m2,
 Eq o1, Eq m1, Eq o2, Eq m2) =>
Int -> Int -> String -> DiagramError c1 m1 o1 c2 m2 o2 -> String
pprintWithIndentations :: Int -> Int -> String -> DiagramError c1 m1 o1 c2 m2 o2 -> String
$cpprintIndent :: forall c1 m1 o1 c2 m2 o2.
(PrettyPrint o1, PrettyPrint m1, PrettyPrint o2, PrettyPrint m2,
 Eq o1, Eq m1, Eq o2, Eq m2) =>
Int -> DiagramError c1 m1 o1 c2 m2 o2 -> String
pprintIndent :: Int -> DiagramError c1 m1 o1 c2 m2 o2 -> String
PrettyPrint)
                               
    -- | Check wether the properties of a 'Diagram' are respected where the source and target category are 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 v. Map k v -> 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 v. Map k v -> Set k
domain Map o1 o2
om}
        | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows c1
s) Set m1 -> Set m1 -> Bool
forall a. Eq a => Set a -> Set a -> Bool
`isIncludedIn` (Map m1 m2 -> Set m1
forall k v. Map k v -> Set k
domain Map m1 m2
fm) = 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 v. Map k v -> 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 c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism 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 c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism 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 c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism 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 v. Map k v -> 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
genArrows c1
s), m1
g <- (c1 -> o1 -> Set m1
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
genArFrom c1
s (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
f)), Bool -> Bool
not (Maybe m2 -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Maybe m2 -> Bool) -> Maybe m2 -> Bool
forall a b. (a -> b) -> a -> b
$ Map m1 m2
fm Map m1 m2 -> m1 -> Maybe m2
forall k v. Eq k => Map k v -> k -> Maybe v
|?| (m1
g m1 -> m1 -> m1
forall m o. Morphism m o => m -> m -> m
@ m1
f)) Bool -> Bool -> Bool
&& 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 source or 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 v. Map k v -> 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 v. Map k v -> Set k
domain Map o1 o2
om}
        | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows c1
s) Set m1 -> Set m1 -> Bool
forall a. Eq a => Set a -> Set a -> Bool
`isIncludedIn` (Map m1 m2 -> Set m1
forall k v. Map k v -> Set k
domain Map m1 m2
fm) = 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 v. Map k v -> 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 c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism 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 c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism 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
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 v. Map k v -> 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)]
    
    -- | Return the inverse of a finite 'Diagram' if possible, return a 'DiagramError' otherwise. Note that this function fails almost all the time if the mapping of morphisms contains generators only (it would only work if all the generators are in the image of the diagram).

    inverseDiagram :: (FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
                       FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => 
        Diagram c1 m1 o1 c2 m2 o2 -> Either (DiagramError c2 m2 o2 c1 m1 o1) (Diagram c2 m2 o2 c1 m1 o1)
    inverseDiagram :: forall c2 m2 o2 c1 m1 o1.
(FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
 FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) =>
Diagram c1 m1 o1 c2 m2 o2
-> Either
     (DiagramError c2 m2 o2 c1 m1 o1) (Diagram c2 m2 o2 c1 m1 o1)
inverseDiagram Diagram c1 m1 o1 c2 m2 o2
diag
        | Maybe (DiagramError c2 m2 o2 c1 m1 o1) -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe (DiagramError c2 m2 o2 c1 m1 o1)
err = Diagram c2 m2 o2 c1 m1 o1
-> Either
     (DiagramError c2 m2 o2 c1 m1 o1) (Diagram c2 m2 o2 c1 m1 o1)
forall a b. b -> Either a b
Right Diagram c2 m2 o2 c1 m1 o1
pseudoInverseDiag
        | Bool
otherwise = DiagramError c2 m2 o2 c1 m1 o1
-> Either
     (DiagramError c2 m2 o2 c1 m1 o1) (Diagram c2 m2 o2 c1 m1 o1)
forall a b. a -> Either a b
Left (DiagramError c2 m2 o2 c1 m1 o1
 -> Either
      (DiagramError c2 m2 o2 c1 m1 o1) (Diagram c2 m2 o2 c1 m1 o1))
-> DiagramError c2 m2 o2 c1 m1 o1
-> Either
     (DiagramError c2 m2 o2 c1 m1 o1) (Diagram c2 m2 o2 c1 m1 o1)
forall a b. (a -> b) -> a -> b
$ Maybe (DiagramError c2 m2 o2 c1 m1 o1)
-> DiagramError c2 m2 o2 c1 m1 o1
forall {a}. Maybe a -> a
fromJust Maybe (DiagramError c2 m2 o2 c1 m1 o1)
err
        where
            pseudoInverseDiag :: Diagram c2 m2 o2 c1 m1 o1
pseudoInverseDiag = Diagram{src :: c2
src = 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, tgt :: c1
tgt = 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, omap :: Map o2 o1
omap = Map o1 o2 -> Map o2 o1
forall k v. Map k v -> Map v k
pseudoInverse (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
diag), mmap :: Map m2 m1
mmap = Map m1 m2 -> Map m2 m1
forall k v. Map k v -> Map v k
pseudoInverse (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
diag)}
            err :: Maybe (DiagramError c2 m2 o2 c1 m1 o1)
err = Diagram c2 m2 o2 c1 m1 o1 -> Maybe (DiagramError c2 m2 o2 c1 m1 o1)
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 c2 m2 o2 c1 m1 o1
pseudoInverseDiag
            fromJust :: Maybe a -> a
fromJust (Just a
x) = a
x
    
    -- | Return the inverse of a 'Diagram' without checking the structure of the returned 'Diagram'. See 'inverseDiagram' for the safe version. Note that this function fails almost all the time if the mapping of morphisms contains generators only (it would only work if all the generators are in the image of the diagram).

    unsafeInverseDiagram :: Diagram c1 m1 o1 c2 m2 o2 -> Diagram c2 m2 o2 c1 m1 o1
    unsafeInverseDiagram :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c2 m2 o2 c1 m1 o1
unsafeInverseDiagram Diagram c1 m1 o1 c2 m2 o2
diag = Diagram{src :: c2
src = 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, tgt :: c1
tgt = 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, omap :: Map o2 o1
omap = Map o1 o2 -> Map o2 o1
forall k v. Map k v -> Map v k
pseudoInverse (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
diag), mmap :: Map m2 m1
mmap = Map m1 m2 -> Map m2 m1
forall k v. Map k v -> Map v k
pseudoInverse (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
diag)}
    
    -- | Smart constructor of a finite 'Diagram'.

    finiteDiagram :: ( 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)
    finiteDiagram :: 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)
finiteDiagram 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
       
    -- | Smart constructor of a 'Diagram'. See 'finiteDiagram' for constructing finite 'Diagram's.

    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,
 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 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 mapping on objects from mapping of arrows and mapping on identities.

    --

    -- Does not check the structure of the resulting 'Diagram', you can use 'checkFiniteDiagram' or 'checkDiagram' 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
newMapObj, 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] }
        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
newMapObj 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, o1
o o1 -> Set o1 -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` (Map o1 o2 -> Set o1
forall k v. Map k v -> Set k
keys' Map o1 o2
newMapObj)]
            mapSrc :: Map o1 o2
mapSrc = AssociationList o1 o2 -> Map o1 o2
forall k v. AssociationList k v -> Map k v
weakMap [(m1 -> o1
forall m o. Morphism m o => m -> o
source m1
f1, m2 -> o2
forall m o. Morphism m o => m -> o
source m2
f2) | (m1
f1,m2
f2) <- (Map m1 m2 -> AssociationList m1 m2
forall k v. Eq k => Map k v -> AssociationList k v
Map.mapToList Map m1 m2
mm)]
            mapTgt :: Map o1 o2
mapTgt= AssociationList o1 o2 -> Map o1 o2
forall k v. AssociationList k v -> Map k v
weakMap [(m1 -> o1
forall m o. Morphism m o => m -> o
target m1
f1, m2 -> o2
forall m o. Morphism m o => m -> o
target m2
f2) | (m1
f1,m2
f2) <- (Map m1 m2 -> AssociationList m1 m2
forall k v. Eq k => Map k v -> AssociationList k v
Map.mapToList Map m1 m2
mm)]
            newMapObj :: Map o1 o2
newMapObj = [Map o1 o2] -> Map o1 o2
forall k a. Eq k => [Map k a] -> Map k a
Map.unions [Map o1 o2
om, Map o1 o2
mapSrc, Map o1 o2
mapTgt]
    
    
    -- | 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 m1, Eq o1, Eq c2, Eq m2, Eq o2, FiniteCategory c1 m1 o1,
 Morphism m1 o1) =>
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 m1, Eq o1, Eq c2, Eq m2, Eq o2, FiniteCategory c1 m1 o1,
 Morphism m1 o1) =>
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 m1, Eq o1, Eq c2, Eq m2, Eq o2, FiniteCategory c1 m1 o1,
 Morphism m1 o1) =>
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, (forall x.
 NaturalTransformation c1 m1 o1 c2 m2 o2
 -> Rep (NaturalTransformation c1 m1 o1 c2 m2 o2) x)
-> (forall x.
    Rep (NaturalTransformation c1 m1 o1 c2 m2 o2) x
    -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Generic (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall x.
Rep (NaturalTransformation c1 m1 o1 c2 m2 o2) x
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall x.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Rep (NaturalTransformation c1 m1 o1 c2 m2 o2) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c1 m1 o1 c2 m2 o2 x.
Rep (NaturalTransformation c1 m1 o1 c2 m2 o2) x
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2 x.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Rep (NaturalTransformation c1 m1 o1 c2 m2 o2) x
$cfrom :: forall c1 m1 o1 c2 m2 o2 x.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Rep (NaturalTransformation c1 m1 o1 c2 m2 o2) x
from :: forall x.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Rep (NaturalTransformation c1 m1 o1 c2 m2 o2) x
$cto :: forall c1 m1 o1 c2 m2 o2 x.
Rep (NaturalTransformation c1 m1 o1 c2 m2 o2) x
-> NaturalTransformation c1 m1 o1 c2 m2 o2
to :: forall x.
Rep (NaturalTransformation c1 m1 o1 c2 m2 o2) x
-> NaturalTransformation c1 m1 o1 c2 m2 o2
Generic, Int
-> Int
-> String
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> String
Int -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> String
(Int -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> String)
-> (Int
    -> Int
    -> String
    -> NaturalTransformation c1 m1 o1 c2 m2 o2
    -> String)
-> (Int -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> String)
-> PrettyPrint (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
 PrettyPrint m1, PrettyPrint m2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Int
-> Int
-> String
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> String
forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
 PrettyPrint m1, PrettyPrint m2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Int -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> String
$cpprint :: forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
 PrettyPrint m1, PrettyPrint m2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Int -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> String
pprint :: Int -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> String
$cpprintWithIndentations :: forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
 PrettyPrint m1, PrettyPrint m2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Int
-> Int
-> String
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> String
pprintWithIndentations :: Int
-> Int
-> String
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> String
$cpprintIndent :: forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
 PrettyPrint m1, PrettyPrint m2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Int -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> String
pprintIndent :: Int -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> String
PrettyPrint, NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
(NaturalTransformation c1 m1 o1 c2 m2 o2
 -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Simplifiable (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall a. (a -> a) -> Simplifiable a
forall c1 m1 o1 c2 m2 o2.
(Simplifiable c1, Simplifiable c2, Simplifiable o1,
 Simplifiable o2, Simplifiable m1, Simplifiable m2, Eq o1, Eq m1) =>
NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
$csimplify :: forall c1 m1 o1 c2 m2 o2.
(Simplifiable c1, Simplifiable c2, Simplifiable o1,
 Simplifiable o2, Simplifiable m1, Simplifiable m2, Eq o1, Eq m1) =>
NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
simplify :: NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
Simplifiable)
    
    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 (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                       Morphism m2 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
-> NaturalTransformation c1 m1 o1 c2 m2 o2
(@) NaturalTransformation c1 m1 o1 c2 m2 o2
nt2 NaturalTransformation c1 m1 o1 c2 m2 o2
nt1 = 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)]}
    
    
    -- | 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 c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, Category c2 m2 o2,
 Morphism m2 o2, Eq o2, Eq m2, Morphism m3 o3) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- 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 c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, Category c2 m2 o2,
 Morphism m2 o2, Eq o2, Eq m2, Morphism m3 o3) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- 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 c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, Eq c2, Eq m2, Eq o2, Morphism m3 o3, Eq c3, Eq m3,
 Eq o3) =>
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
<=@<- 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 c2 m2 o2 m3 o3 c3.
(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,
 Morphism m3 o3) =>
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'.

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

    (<-@<=) :: (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,
                                         Morphism m3 o3) => 
                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 c2 m2 o2 m3 o3 c3.
(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,
 Morphism m3 o3) =>
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 c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, Category c2 m2 o2,
 Morphism m2 o2, Eq o2, Eq m2, Morphism m3 o3) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- (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 c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, Category c2 m2 o2,
 Morphism m2 o2, Eq o2, Eq m2, Morphism m3 o3) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- (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,
                              Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
                                                 Morphism m3 o3) => 
        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 c2 m2 o2 m3 o3 c3.
(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,
 Morphism m3 o3) =>
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 c2 m2 o2 m3 o3 c3.
(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,
 Morphism m3 o3) =>
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.

                                                      | WrongComponentSource{forall c1 m1 o1 c2 m2 o2.
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> m2
faultyComponent1 :: m2, forall c1 m1 o1 c2 m2 o2.
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> o1
correctSource :: o1} -- ^ The source of a component is not the image of the indexing object by the source functor. 

                                                      | WrongComponentTarget{forall c1 m1 o1 c2 m2 o2.
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> m2
faultyComponent2 :: m2, forall c1 m1 o1 c2 m2 o2.
NaturalTransformationError c1 m1 o1 c2 m2 o2 -> o1
correctTarget :: o1} -- ^ The target of a component is not the image of the indexing object by the target functor. 

                                                      | 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 m2, 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 m2, 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 m2, 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 m2, 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 m2, Show o1, Show m1) =>
[NaturalTransformationError c1 m1 o1 c2 m2 o2] -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show m2, 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 m2, 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 m2, 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 m2, Show o1, Show m1) =>
[NaturalTransformationError c1 m1 o1 c2 m2 o2] -> ShowS
showList :: [NaturalTransformationError c1 m1 o1 c2 m2 o2] -> ShowS
Show, (forall x.
 NaturalTransformationError c1 m1 o1 c2 m2 o2
 -> Rep (NaturalTransformationError c1 m1 o1 c2 m2 o2) x)
-> (forall x.
    Rep (NaturalTransformationError c1 m1 o1 c2 m2 o2) x
    -> NaturalTransformationError c1 m1 o1 c2 m2 o2)
-> Generic (NaturalTransformationError c1 m1 o1 c2 m2 o2)
forall x.
Rep (NaturalTransformationError c1 m1 o1 c2 m2 o2) x
-> NaturalTransformationError c1 m1 o1 c2 m2 o2
forall x.
NaturalTransformationError c1 m1 o1 c2 m2 o2
-> Rep (NaturalTransformationError c1 m1 o1 c2 m2 o2) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c1 m1 o1 c2 m2 o2 x.
Rep (NaturalTransformationError c1 m1 o1 c2 m2 o2) x
-> NaturalTransformationError c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2 x.
NaturalTransformationError c1 m1 o1 c2 m2 o2
-> Rep (NaturalTransformationError c1 m1 o1 c2 m2 o2) x
$cfrom :: forall c1 m1 o1 c2 m2 o2 x.
NaturalTransformationError c1 m1 o1 c2 m2 o2
-> Rep (NaturalTransformationError c1 m1 o1 c2 m2 o2) x
from :: forall x.
NaturalTransformationError c1 m1 o1 c2 m2 o2
-> Rep (NaturalTransformationError c1 m1 o1 c2 m2 o2) x
$cto :: forall c1 m1 o1 c2 m2 o2 x.
Rep (NaturalTransformationError c1 m1 o1 c2 m2 o2) x
-> NaturalTransformationError c1 m1 o1 c2 m2 o2
to :: forall x.
Rep (NaturalTransformationError c1 m1 o1 c2 m2 o2) x
-> NaturalTransformationError c1 m1 o1 c2 m2 o2
Generic, Int
-> Int
-> String
-> NaturalTransformationError c1 m1 o1 c2 m2 o2
-> String
Int -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> String
(Int -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> String)
-> (Int
    -> Int
    -> String
    -> NaturalTransformationError c1 m1 o1 c2 m2 o2
    -> String)
-> (Int -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> String)
-> PrettyPrint (NaturalTransformationError c1 m1 o1 c2 m2 o2)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c1 m1 o1 c2 m2 o2.
(Eq o1, PrettyPrint c1, PrettyPrint c2, PrettyPrint m2,
 PrettyPrint o1, PrettyPrint m1) =>
Int
-> Int
-> String
-> NaturalTransformationError c1 m1 o1 c2 m2 o2
-> String
forall c1 m1 o1 c2 m2 o2.
(Eq o1, PrettyPrint c1, PrettyPrint c2, PrettyPrint m2,
 PrettyPrint o1, PrettyPrint m1) =>
Int -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> String
$cpprint :: forall c1 m1 o1 c2 m2 o2.
(Eq o1, PrettyPrint c1, PrettyPrint c2, PrettyPrint m2,
 PrettyPrint o1, PrettyPrint m1) =>
Int -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> String
pprint :: Int -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> String
$cpprintWithIndentations :: forall c1 m1 o1 c2 m2 o2.
(Eq o1, PrettyPrint c1, PrettyPrint c2, PrettyPrint m2,
 PrettyPrint o1, PrettyPrint m1) =>
Int
-> Int
-> String
-> NaturalTransformationError c1 m1 o1 c2 m2 o2
-> String
pprintWithIndentations :: Int
-> Int
-> String
-> NaturalTransformationError c1 m1 o1 c2 m2 o2
-> String
$cpprintIndent :: forall c1 m1 o1 c2 m2 o2.
(Eq o1, PrettyPrint c1, PrettyPrint c2, PrettyPrint m2,
 PrettyPrint o1, PrettyPrint m1) =>
Int -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> String
pprintIndent :: Int -> NaturalTransformationError c1 m1 o1 c2 m2 o2 -> String
PrettyPrint, NaturalTransformationError c1 m1 o1 c2 m2 o2
-> NaturalTransformationError c1 m1 o1 c2 m2 o2
(NaturalTransformationError c1 m1 o1 c2 m2 o2
 -> NaturalTransformationError c1 m1 o1 c2 m2 o2)
-> Simplifiable (NaturalTransformationError c1 m1 o1 c2 m2 o2)
forall a. (a -> a) -> Simplifiable a
forall c1 m1 o1 c2 m2 o2.
(Eq o1, Simplifiable c1, Simplifiable c2, Simplifiable m2,
 Simplifiable o1, Simplifiable m1) =>
NaturalTransformationError c1 m1 o1 c2 m2 o2
-> NaturalTransformationError c1 m1 o1 c2 m2 o2
$csimplify :: forall c1 m1 o1 c2 m2 o2.
(Eq o1, Simplifiable c1, Simplifiable c2, Simplifiable m2,
 Simplifiable o1, Simplifiable m1) =>
NaturalTransformationError c1 m1 o1 c2 m2 o2
-> NaturalTransformationError c1 m1 o1 c2 m2 o2
simplify :: NaturalTransformationError c1 m1 o1 c2 m2 o2
-> NaturalTransformationError c1 m1 o1 c2 m2 o2
Simplifiable)
    
    
    -- | 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 v. Map k v -> 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 (m2, o1) -> Bool) -> Set (m2, o1) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set (m2, o1) -> Bool
forall a. Set a -> Bool
Set.null)) Set (m2, o1)
wrongSource = NaturalTransformationError c1 m1 o1 c2 m2 o2
-> Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just WrongComponentSource{faultyComponent1 :: m2
faultyComponent1 = (m2, o1) -> m2
forall a b. (a, b) -> a
fst ((m2, o1) -> m2) -> (m2, o1) -> m2
forall a b. (a -> b) -> a -> b
$ Set (m2, o1) -> (m2, o1)
forall a. Set a -> a
anElement Set (m2, o1)
wrongSource, correctSource :: o1
correctSource = (m2, o1) -> o1
forall a b. (a, b) -> b
snd ((m2, o1) -> o1) -> (m2, o1) -> o1
forall a b. (a -> b) -> a -> b
$ Set (m2, o1) -> (m2, o1)
forall a. Set a -> a
anElement Set (m2, o1)
wrongSource}
        | (Bool -> Bool
not(Bool -> Bool) -> (Set (m2, o1) -> Bool) -> Set (m2, o1) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set (m2, o1) -> Bool
forall a. Set a -> Bool
Set.null)) Set (m2, o1)
wrongTarget = NaturalTransformationError c1 m1 o1 c2 m2 o2
-> Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just WrongComponentTarget{faultyComponent2 :: m2
faultyComponent2 = (m2, o1) -> m2
forall a b. (a, b) -> a
fst ((m2, o1) -> m2) -> (m2, o1) -> m2
forall a b. (a -> b) -> a -> b
$ Set (m2, o1) -> (m2, o1)
forall a. Set a -> a
anElement Set (m2, o1)
wrongTarget, correctTarget :: o1
correctTarget = (m2, o1) -> o1
forall a b. (a, b) -> b
snd ((m2, o1) -> o1) -> (m2, o1) -> o1
forall a b. (a -> b) -> a -> b
$ Set (m2, o1) -> (m2, o1)
forall a. Set a -> a
anElement Set (m2, o1)
wrongTarget}
        | (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 v. Map k v -> 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)
            wrongSource :: Set (m2, o1)
wrongSource = [((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
=>$ o1
i),o1
i) | o1
i <- (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), (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 -> o1 -> o2
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
i o2 -> o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= m2 -> o2
forall m o. Morphism m o => m -> o
source (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
=>$ o1
i)]
            wrongTarget :: Set (m2, o1)
wrongTarget = [((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
=>$ o1
i),o1
i) | o1
i <- (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), (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 -> o1 -> o2
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
i o2 -> o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= m2 -> o2
forall m o. Morphism m o => m -> o
target (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
=>$ o1
i)]
            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 c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism 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 c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism 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}
    
    indexingCategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2) => NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
    indexingCategory :: forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
indexingCategory = 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
    
    -- 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, (forall x.
 FunctorCategory c1 m1 o1 c2 m2 o2
 -> Rep (FunctorCategory c1 m1 o1 c2 m2 o2) x)
-> (forall x.
    Rep (FunctorCategory c1 m1 o1 c2 m2 o2) x
    -> FunctorCategory c1 m1 o1 c2 m2 o2)
-> Generic (FunctorCategory c1 m1 o1 c2 m2 o2)
forall x.
Rep (FunctorCategory c1 m1 o1 c2 m2 o2) x
-> FunctorCategory c1 m1 o1 c2 m2 o2
forall x.
FunctorCategory c1 m1 o1 c2 m2 o2
-> Rep (FunctorCategory c1 m1 o1 c2 m2 o2) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c1 m1 o1 c2 m2 o2 x.
Rep (FunctorCategory c1 m1 o1 c2 m2 o2) x
-> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2 x.
FunctorCategory c1 m1 o1 c2 m2 o2
-> Rep (FunctorCategory c1 m1 o1 c2 m2 o2) x
$cfrom :: forall c1 m1 o1 c2 m2 o2 x.
FunctorCategory c1 m1 o1 c2 m2 o2
-> Rep (FunctorCategory c1 m1 o1 c2 m2 o2) x
from :: forall x.
FunctorCategory c1 m1 o1 c2 m2 o2
-> Rep (FunctorCategory c1 m1 o1 c2 m2 o2) x
$cto :: forall c1 m1 o1 c2 m2 o2 x.
Rep (FunctorCategory c1 m1 o1 c2 m2 o2) x
-> FunctorCategory c1 m1 o1 c2 m2 o2
to :: forall x.
Rep (FunctorCategory c1 m1 o1 c2 m2 o2) x
-> FunctorCategory c1 m1 o1 c2 m2 o2
Generic, Int -> Int -> String -> FunctorCategory c1 m1 o1 c2 m2 o2 -> String
Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> String
(Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> String)
-> (Int
    -> Int -> String -> FunctorCategory c1 m1 o1 c2 m2 o2 -> String)
-> (Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> String)
-> PrettyPrint (FunctorCategory c1 m1 o1 c2 m2 o2)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2) =>
Int -> Int -> String -> FunctorCategory c1 m1 o1 c2 m2 o2 -> String
forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2) =>
Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> String
$cpprint :: forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2) =>
Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> String
pprint :: Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> String
$cpprintWithIndentations :: forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2) =>
Int -> Int -> String -> FunctorCategory c1 m1 o1 c2 m2 o2 -> String
pprintWithIndentations :: Int -> Int -> String -> FunctorCategory c1 m1 o1 c2 m2 o2 -> String
$cpprintIndent :: forall c1 m1 o1 c2 m2 o2.
(PrettyPrint c1, PrettyPrint c2) =>
Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> String
pprintIndent :: Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> String
PrettyPrint, FunctorCategory c1 m1 o1 c2 m2 o2
-> FunctorCategory c1 m1 o1 c2 m2 o2
(FunctorCategory c1 m1 o1 c2 m2 o2
 -> FunctorCategory c1 m1 o1 c2 m2 o2)
-> Simplifiable (FunctorCategory c1 m1 o1 c2 m2 o2)
forall a. (a -> a) -> Simplifiable a
forall c1 m1 o1 c2 m2 o2.
(Simplifiable c1, Simplifiable c2) =>
FunctorCategory c1 m1 o1 c2 m2 o2
-> FunctorCategory c1 m1 o1 c2 m2 o2
$csimplify :: forall c1 m1 o1 c2 m2 o2.
(Simplifiable c1, Simplifiable c2) =>
FunctorCategory c1 m1 o1 c2 m2 o2
-> FunctorCategory c1 m1 o1 c2 m2 o2
simplify :: FunctorCategory c1 m1 o1 c2 m2 o2
-> FunctorCategory c1 m1 o1 c2 m2 o2
Simplifiable)
        
    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.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Eq c2, Eq m2, Eq o2, 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.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Eq c2, Eq m2, Eq o2, 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.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Eq c2, Eq m2, Eq o2, 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, (forall x.
 PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> Rep (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x)
-> (forall x.
    Rep (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
    -> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Generic (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall x.
Rep (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
forall x.
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cfrom :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
from :: forall x.
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cto :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
to :: forall x.
Rep (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
Generic, Int
-> Int
-> String
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
Int
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int
 -> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> (Int
    -> Int
    -> String
    -> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> String)
-> (Int
    -> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> PrettyPrint
     (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o1, Eq o2, Eq m1, Eq m2, PrettyPrint c1, PrettyPrint c2,
 PrettyPrint o1, PrettyPrint o2, PrettyPrint m1, PrettyPrint m2,
 PrettyPrint c3) =>
Int
-> Int
-> String
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o1, Eq o2, Eq m1, Eq m2, PrettyPrint c1, PrettyPrint c2,
 PrettyPrint o1, PrettyPrint o2, PrettyPrint m1, PrettyPrint m2,
 PrettyPrint c3) =>
Int
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprint :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o1, Eq o2, Eq m1, Eq m2, PrettyPrint c1, PrettyPrint c2,
 PrettyPrint o1, PrettyPrint o2, PrettyPrint m1, PrettyPrint m2,
 PrettyPrint c3) =>
Int
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprint :: Int
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprintWithIndentations :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o1, Eq o2, Eq m1, Eq m2, PrettyPrint c1, PrettyPrint c2,
 PrettyPrint o1, PrettyPrint o2, PrettyPrint m1, PrettyPrint m2,
 PrettyPrint c3) =>
Int
-> Int
-> String
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
pprintWithIndentations :: Int
-> Int
-> String
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
$cpprintIndent :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o1, Eq o2, Eq m1, Eq m2, PrettyPrint c1, PrettyPrint c2,
 PrettyPrint o1, PrettyPrint o2, PrettyPrint m1, PrettyPrint m2,
 PrettyPrint c3) =>
Int
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprintIndent :: Int
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
PrettyPrint, PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
(PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Simplifiable
     (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a) -> Simplifiable a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o1, Eq m1, Simplifiable c1, Simplifiable c2, Simplifiable o1,
 Simplifiable o2, Simplifiable m1, Simplifiable m2,
 Simplifiable c3) =>
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
$csimplify :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o1, Eq m1, Simplifiable c1, Simplifiable c2, Simplifiable o1,
 Simplifiable o2, Simplifiable m1, Simplifiable m2,
 Simplifiable c3) =>
PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
simplify :: PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
Simplifiable)
        
    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 c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, Category c2 m2 o2,
 Morphism m2 o2, Eq o2, Eq m2, Morphism m3 o3) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- Diagram c1 m1 o1 c2 m2 o2
diag) (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.
(FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
 Eq c3, Eq m3, Eq o3, 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.
(FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
 Eq c3, Eq m3, Eq o3, 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.
(FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
 Eq c3, Eq m3, Eq o3, 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, (forall x.
 PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> Rep (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x)
-> (forall x.
    Rep (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
    -> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Generic (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall x.
Rep (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
forall x.
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cfrom :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
from :: forall x.
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cto :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
to :: forall x.
Rep (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
Generic, Int
-> Int
-> String
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
Int
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int
 -> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> String)
-> (Int
    -> Int
    -> String
    -> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> String)
-> (Int
    -> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> String)
-> PrettyPrint
     (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o2, Eq o3, Eq m2, Eq m3, PrettyPrint c2, PrettyPrint c3,
 PrettyPrint o2, PrettyPrint o3, PrettyPrint m2, PrettyPrint m3,
 PrettyPrint c1) =>
Int
-> Int
-> String
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o2, Eq o3, Eq m2, Eq m3, PrettyPrint c2, PrettyPrint c3,
 PrettyPrint o2, PrettyPrint o3, PrettyPrint m2, PrettyPrint m3,
 PrettyPrint c1) =>
Int
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprint :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o2, Eq o3, Eq m2, Eq m3, PrettyPrint c2, PrettyPrint c3,
 PrettyPrint o2, PrettyPrint o3, PrettyPrint m2, PrettyPrint m3,
 PrettyPrint c1) =>
Int
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprint :: Int
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprintWithIndentations :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o2, Eq o3, Eq m2, Eq m3, PrettyPrint c2, PrettyPrint c3,
 PrettyPrint o2, PrettyPrint o3, PrettyPrint m2, PrettyPrint m3,
 PrettyPrint c1) =>
Int
-> Int
-> String
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
pprintWithIndentations :: Int
-> Int
-> String
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
$cpprintIndent :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o2, Eq o3, Eq m2, Eq m3, PrettyPrint c2, PrettyPrint c3,
 PrettyPrint o2, PrettyPrint o3, PrettyPrint m2, PrettyPrint m3,
 PrettyPrint c1) =>
Int
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprintIndent :: Int
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
PrettyPrint, PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
(PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Simplifiable
     (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a) -> Simplifiable a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o2, Eq m2, Simplifiable c2, Simplifiable c3, Simplifiable o2,
 Simplifiable o3, Simplifiable m2, Simplifiable m3,
 Simplifiable c1) =>
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
$csimplify :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o2, Eq m2, Simplifiable c2, Simplifiable c3, Simplifiable o2,
 Simplifiable o3, Simplifiable m2, Simplifiable m3,
 Simplifiable c1) =>
PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
simplify :: PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
Simplifiable)
        
    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 c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, Category c2 m2 o2,
 Morphism m2 o2, Eq o2, Eq m2, Morphism m3 o3) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<-) (Diagram c1 m1 o1 c2 m2 o2 -> 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)}