{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE UndecidableInstances  #-}

{-| Module  : FiniteCategories
Description : A 'Subcategory' of a category /C/ is a category /D/ whose objects are objects in /C/ and whose morphisms are morphisms in /C/ with the same identities and composition of morphisms.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A 'Subcategory' of a category /C/ is a category /D/ whose objects are objects in /C/ and whose morphisms are morphisms in /C/ with the same identities and composition of morphisms.

We have to forget the generating set of morphisms of the original 'Category' as the generators are not always inheritable (see for example the full subcategory of __'Square'__ containing the objects A and D).

If the generators are inheritable, you can use the constructor 'InheritedSubcategory' to inherit the generators of the original 'Category'.
-}

module Math.FiniteCategories.Subcategory
(
    -- * Subcategory

    Subcategory,
    -- ** Smart constructors

    unsafeSubcategory,
    subcategory,
    -- ** Getter

    originalCategory,
    -- ** Interaction with 'Diagram'

    embeddingToSubcategory,
    fullDiagram,
    fullNaturalTransformation,
    -- * InheritedSubcategory

    InheritedSubcategory,
    -- ** Smart constructors

    unsafeInheritedSubcategory,
    inheritedSubcategory,
    -- ** Getter

    originalCategory2,
    -- ** Interaction with 'Diagram'

    embeddingToInheritedSubcategory,
    fullDiagram2,
    fullNaturalTransformation2,
)
where
    import              Math.FiniteCategory
    import              Math.FiniteCategoryError
    import              Math.Categories.FunctorCategory
    import              Math.IO.PrettyPrint
    
    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              GHC.Generics
    
    -- | A 'Subcategory' needs an original category, a set of objects and a set of morphisms selected in the category.

    --

    -- The generators are forgotten, use 'InheritedSubcategory' if the generators are inheritable.

    --

    -- 'Subcategory' is private because the subset of morphisms might not yield a valid 'FiniteCategory' if a composite morphism does not belong in the subset.

    --

    -- Use the smart constructor 'subcategory' instead.

    data Subcategory c m o = Subcategory c (Set o) (Set m) deriving (Subcategory c m o -> Subcategory c m o -> Bool
(Subcategory c m o -> Subcategory c m o -> Bool)
-> (Subcategory c m o -> Subcategory c m o -> Bool)
-> Eq (Subcategory c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o.
(Eq c, Eq o, Eq m) =>
Subcategory c m o -> Subcategory c m o -> Bool
$c== :: forall c m o.
(Eq c, Eq o, Eq m) =>
Subcategory c m o -> Subcategory c m o -> Bool
== :: Subcategory c m o -> Subcategory c m o -> Bool
$c/= :: forall c m o.
(Eq c, Eq o, Eq m) =>
Subcategory c m o -> Subcategory c m o -> Bool
/= :: Subcategory c m o -> Subcategory c m o -> Bool
Eq, (forall x. Subcategory c m o -> Rep (Subcategory c m o) x)
-> (forall x. Rep (Subcategory c m o) x -> Subcategory c m o)
-> Generic (Subcategory c m o)
forall x. Rep (Subcategory c m o) x -> Subcategory c m o
forall x. Subcategory c m o -> Rep (Subcategory c m o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c m o x. Rep (Subcategory c m o) x -> Subcategory c m o
forall c m o x. Subcategory c m o -> Rep (Subcategory c m o) x
$cfrom :: forall c m o x. Subcategory c m o -> Rep (Subcategory c m o) x
from :: forall x. Subcategory c m o -> Rep (Subcategory c m o) x
$cto :: forall c m o x. Rep (Subcategory c m o) x -> Subcategory c m o
to :: forall x. Rep (Subcategory c m o) x -> Subcategory c m o
Generic, Int -> Int -> String -> Subcategory c m o -> String
Int -> Subcategory c m o -> String
(Int -> Subcategory c m o -> String)
-> (Int -> Int -> String -> Subcategory c m o -> String)
-> (Int -> Subcategory c m o -> String)
-> PrettyPrint (Subcategory c m o)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int -> Int -> String -> Subcategory c m o -> String
forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int -> Subcategory c m o -> String
$cpprint :: forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int -> Subcategory c m o -> String
pprint :: Int -> Subcategory c m o -> String
$cpprintWithIndentations :: forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int -> Int -> String -> Subcategory c m o -> String
pprintWithIndentations :: Int -> Int -> String -> Subcategory c m o -> String
$cpprintIndent :: forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int -> Subcategory c m o -> String
pprintIndent :: Int -> Subcategory c m o -> String
PrettyPrint, Subcategory c m o -> Subcategory c m o
(Subcategory c m o -> Subcategory c m o)
-> Simplifiable (Subcategory c m o)
forall a. (a -> a) -> Simplifiable a
forall c m o.
(Simplifiable c, Simplifiable o, Simplifiable m, Eq o, Eq m) =>
Subcategory c m o -> Subcategory c m o
$csimplify :: forall c m o.
(Simplifiable c, Simplifiable o, Simplifiable m, Eq o, Eq m) =>
Subcategory c m o -> Subcategory c m o
simplify :: Subcategory c m o -> Subcategory c m o
Simplifiable)
    
    instance (Show c, Show m, Show o) => Show (Subcategory c m o) where
        show :: Subcategory c m o -> String
show (Subcategory c
c Set o
os Set m
ms) = String
"(unsafeSubcategory "String -> ShowS
forall a. [a] -> [a] -> [a]
++c -> String
forall a. Show a => a -> String
show c
cString -> ShowS
forall a. [a] -> [a] -> [a]
++String
" "String -> ShowS
forall a. [a] -> [a] -> [a]
++Set o -> String
forall a. Show a => a -> String
show Set o
osString -> ShowS
forall a. [a] -> [a] -> [a]
++String
" "String -> ShowS
forall a. [a] -> [a] -> [a]
++Set m -> String
forall a. Show a => a -> String
show Set m
msString -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"
    
    -- | Unsafe version of 'subcategory' which does not check the structure of the 'Subcategory' constructed.

    unsafeSubcategory :: c -> (Set o) -> (Set m) -> Subcategory c m o
    unsafeSubcategory :: forall c o m. c -> Set o -> Set m -> Subcategory c m o
unsafeSubcategory c
c Set o
os Set m
ms = c -> Set o -> Set m -> Subcategory c m o
forall c m o. c -> Set o -> Set m -> Subcategory c m o
Subcategory c
c Set o
os Set m
ms
    
    -- | Smart constructor of 'Subcategory'.

    --

    -- If the 'Subcategory' constructed is valid, return 'Right' the subcategory, otherwise return Left a 'FiniteCategoryError'.

    subcategory :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> (Set o) -> (Set m) -> Either (FiniteCategoryError m o) (Subcategory c m o)
    subcategory :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c
-> Set o
-> Set m
-> Either (FiniteCategoryError m o) (Subcategory c m o)
subcategory c
c Set o
ms Set m
os
        | Maybe (FiniteCategoryError m o) -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe (FiniteCategoryError m o)
check = Subcategory c m o
-> Either (FiniteCategoryError m o) (Subcategory c m o)
forall a b. b -> Either a b
Right Subcategory c m o
r
        | Bool
otherwise = FiniteCategoryError m o
-> Either (FiniteCategoryError m o) (Subcategory c m o)
forall a b. a -> Either a b
Left FiniteCategoryError m o
err
        where
            r :: Subcategory c m o
r = c -> Set o -> Set m -> Subcategory c m o
forall c m o. c -> Set o -> Set m -> Subcategory c m o
Subcategory c
c Set o
ms Set m
os
            check :: Maybe (FiniteCategoryError m o)
check = Subcategory c m o -> Maybe (FiniteCategoryError m o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Maybe (FiniteCategoryError m o)
checkFiniteCategory Subcategory c m o
r
            Just FiniteCategoryError m o
err = Maybe (FiniteCategoryError m o)
check
            
    -- | Return the original category the 'Subcategory' was taken from.

    originalCategory :: Subcategory c m o -> c
    originalCategory :: forall c m o. Subcategory c m o -> c
originalCategory (Subcategory c
c Set o
_ Set m
_) = c
c
    
    instance (Category c m o, Eq o, Eq m) => Category (Subcategory c m o) m o where
        identity :: Morphism m o => Subcategory c m o -> o -> m
identity (Subcategory c
c Set o
objs Set m
_) o
o
            | o
o o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs = c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c o
o
            | Bool
otherwise = String -> m
forall a. HasCallStack => String -> a
error String
"Math.FiniteCategories.Subcategory.identity: object not in the subcategory"
        ar :: Morphism m o => Subcategory c m o -> o -> o -> Set m
ar (Subcategory c
c Set o
objs Set m
morphs) o
s o
t
            | o
s o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs Bool -> Bool -> Bool
&& o
t o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs = (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (m -> Set m -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set m
morphs) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
s o
t
            | Bool
otherwise = String -> Set m
forall a. HasCallStack => String -> a
error String
"Math.FiniteCategories.Subcategory.ar: source or target not in the subcategory"
    
    instance (Category c m o, Eq o, Eq m) => FiniteCategory (Subcategory c m o) m o where
        ob :: Subcategory c m o -> Set o
ob (Subcategory c
_ Set o
o Set m
_) = Set o
o
        
        
        
    -- | An 'InheritedSubcategory' needs an original category, a set of objects and a set of morphisms selected in the category.

    --

    -- The generators are inherited.

    --

    -- 'InheritedSubcategory' is private because the subset of morphisms might not yield a valid 'FiniteCategory' if a composite morphism does not belong in the subset.

    --

    -- Use the smart constructor 'inheritedSubcategory' instead.

    data InheritedSubcategory c m o = InheritedSubcategory c (Set o) (Set m) deriving (InheritedSubcategory c m o -> InheritedSubcategory c m o -> Bool
(InheritedSubcategory c m o -> InheritedSubcategory c m o -> Bool)
-> (InheritedSubcategory c m o
    -> InheritedSubcategory c m o -> Bool)
-> Eq (InheritedSubcategory c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o.
(Eq c, Eq o, Eq m) =>
InheritedSubcategory c m o -> InheritedSubcategory c m o -> Bool
$c== :: forall c m o.
(Eq c, Eq o, Eq m) =>
InheritedSubcategory c m o -> InheritedSubcategory c m o -> Bool
== :: InheritedSubcategory c m o -> InheritedSubcategory c m o -> Bool
$c/= :: forall c m o.
(Eq c, Eq o, Eq m) =>
InheritedSubcategory c m o -> InheritedSubcategory c m o -> Bool
/= :: InheritedSubcategory c m o -> InheritedSubcategory c m o -> Bool
Eq, (forall x.
 InheritedSubcategory c m o -> Rep (InheritedSubcategory c m o) x)
-> (forall x.
    Rep (InheritedSubcategory c m o) x -> InheritedSubcategory c m o)
-> Generic (InheritedSubcategory c m o)
forall x.
Rep (InheritedSubcategory c m o) x -> InheritedSubcategory c m o
forall x.
InheritedSubcategory c m o -> Rep (InheritedSubcategory c m o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c m o x.
Rep (InheritedSubcategory c m o) x -> InheritedSubcategory c m o
forall c m o x.
InheritedSubcategory c m o -> Rep (InheritedSubcategory c m o) x
$cfrom :: forall c m o x.
InheritedSubcategory c m o -> Rep (InheritedSubcategory c m o) x
from :: forall x.
InheritedSubcategory c m o -> Rep (InheritedSubcategory c m o) x
$cto :: forall c m o x.
Rep (InheritedSubcategory c m o) x -> InheritedSubcategory c m o
to :: forall x.
Rep (InheritedSubcategory c m o) x -> InheritedSubcategory c m o
Generic, Int -> Int -> String -> InheritedSubcategory c m o -> String
Int -> InheritedSubcategory c m o -> String
(Int -> InheritedSubcategory c m o -> String)
-> (Int -> Int -> String -> InheritedSubcategory c m o -> String)
-> (Int -> InheritedSubcategory c m o -> String)
-> PrettyPrint (InheritedSubcategory c m o)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int -> Int -> String -> InheritedSubcategory c m o -> String
forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int -> InheritedSubcategory c m o -> String
$cpprint :: forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int -> InheritedSubcategory c m o -> String
pprint :: Int -> InheritedSubcategory c m o -> String
$cpprintWithIndentations :: forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int -> Int -> String -> InheritedSubcategory c m o -> String
pprintWithIndentations :: Int -> Int -> String -> InheritedSubcategory c m o -> String
$cpprintIndent :: forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int -> InheritedSubcategory c m o -> String
pprintIndent :: Int -> InheritedSubcategory c m o -> String
PrettyPrint, InheritedSubcategory c m o -> InheritedSubcategory c m o
(InheritedSubcategory c m o -> InheritedSubcategory c m o)
-> Simplifiable (InheritedSubcategory c m o)
forall a. (a -> a) -> Simplifiable a
forall c m o.
(Simplifiable c, Simplifiable o, Simplifiable m, Eq o, Eq m) =>
InheritedSubcategory c m o -> InheritedSubcategory c m o
$csimplify :: forall c m o.
(Simplifiable c, Simplifiable o, Simplifiable m, Eq o, Eq m) =>
InheritedSubcategory c m o -> InheritedSubcategory c m o
simplify :: InheritedSubcategory c m o -> InheritedSubcategory c m o
Simplifiable)
    
    instance (Show c, Show m, Show o) => Show (InheritedSubcategory c m o) where
        show :: InheritedSubcategory c m o -> String
show (InheritedSubcategory c
c Set o
os Set m
ms) = String
"(unsafeInheritedSubcategory "String -> ShowS
forall a. [a] -> [a] -> [a]
++c -> String
forall a. Show a => a -> String
show c
cString -> ShowS
forall a. [a] -> [a] -> [a]
++String
" "String -> ShowS
forall a. [a] -> [a] -> [a]
++Set o -> String
forall a. Show a => a -> String
show Set o
osString -> ShowS
forall a. [a] -> [a] -> [a]
++String
" "String -> ShowS
forall a. [a] -> [a] -> [a]
++Set m -> String
forall a. Show a => a -> String
show Set m
msString -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"
    
    -- | Unsafe version of 'inheritedSubcategory' which does not check the structure of the 'InheritedSubcategory' constructed.

    unsafeInheritedSubcategory :: c -> (Set o) -> (Set m) -> InheritedSubcategory c m o
    unsafeInheritedSubcategory :: forall c o m. c -> Set o -> Set m -> InheritedSubcategory c m o
unsafeInheritedSubcategory c
c Set o
os Set m
ms = c -> Set o -> Set m -> InheritedSubcategory c m o
forall c m o. c -> Set o -> Set m -> InheritedSubcategory c m o
InheritedSubcategory c
c Set o
os Set m
ms
    
    -- | Smart constructor of 'InheritedSubcategory'.

    --

    -- If the 'InheritedSubcategory' constructed is valid, return 'Right' the subcategory, otherwise return Left a 'FiniteCategoryError'.

    inheritedSubcategory :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> (Set o) -> (Set m) -> Either (FiniteCategoryError m o) (InheritedSubcategory c m o)
    inheritedSubcategory :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c
-> Set o
-> Set m
-> Either (FiniteCategoryError m o) (InheritedSubcategory c m o)
inheritedSubcategory c
c Set o
ms Set m
os
        | Maybe (FiniteCategoryError m o) -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe (FiniteCategoryError m o)
check = InheritedSubcategory c m o
-> Either (FiniteCategoryError m o) (InheritedSubcategory c m o)
forall a b. b -> Either a b
Right InheritedSubcategory c m o
r
        | Bool
otherwise = FiniteCategoryError m o
-> Either (FiniteCategoryError m o) (InheritedSubcategory c m o)
forall a b. a -> Either a b
Left FiniteCategoryError m o
err
        where
            r :: InheritedSubcategory c m o
r = c -> Set o -> Set m -> InheritedSubcategory c m o
forall c m o. c -> Set o -> Set m -> InheritedSubcategory c m o
InheritedSubcategory c
c Set o
ms Set m
os
            check :: Maybe (FiniteCategoryError m o)
check = InheritedSubcategory c m o -> Maybe (FiniteCategoryError m o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Maybe (FiniteCategoryError m o)
checkFiniteCategory InheritedSubcategory c m o
r
            Just FiniteCategoryError m o
err = Maybe (FiniteCategoryError m o)
check
            
    -- | Return the original category the 'InheritedSubcategory' was taken from.

    originalCategory2 :: InheritedSubcategory c m o -> c
    originalCategory2 :: forall c m o. InheritedSubcategory c m o -> c
originalCategory2 (InheritedSubcategory c
c Set o
_ Set m
_) = c
c
    
    instance (Category c m o, Eq o, Eq m) => Category (InheritedSubcategory c m o) m o where
        identity :: Morphism m o => InheritedSubcategory c m o -> o -> m
identity (InheritedSubcategory c
c Set o
objs Set m
_) o
o
            | o
o o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs = c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c o
o
            | Bool
otherwise = String -> m
forall a. HasCallStack => String -> a
error String
"Math.FiniteCategories.InheritedSubcategory.identity: object not in the subcategory"
        ar :: Morphism m o => InheritedSubcategory c m o -> o -> o -> Set m
ar (InheritedSubcategory c
c Set o
objs Set m
morphs) o
s o
t
            | o
s o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs Bool -> Bool -> Bool
&& o
t o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs = (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (m -> Set m -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set m
morphs) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
s o
t
            | Bool
otherwise = String -> Set m
forall a. HasCallStack => String -> a
error String
"Math.FiniteCategories.InheritedSubcategory.ar: source or target not in the subcategory"
        genAr :: Morphism m o => InheritedSubcategory c m o -> o -> o -> Set m
genAr (InheritedSubcategory c
c Set o
objs Set m
morphs) o
s o
t
            | o
s o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs Bool -> Bool -> Bool
&& o
t o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs = (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (m -> Set m -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set m
morphs) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr c
c o
s o
t
            | Bool
otherwise = String -> Set m
forall a. HasCallStack => String -> a
error String
"Math.FiniteCategories.InheritedSubcategory.genAr: source or target not in the subcategory"
        decompose :: Morphism m o => InheritedSubcategory c m o -> m -> [m]
decompose (InheritedSubcategory c
c Set o
_ Set m
morphs) m
m
            | m
m m -> Set m -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set m
morphs = c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
c m
m
            | Bool
otherwise = String -> [m]
forall a. HasCallStack => String -> a
error String
"Math.FiniteCategories.InheritedSubcategory.decompose: morphism not in the subcategory"
    
    instance (Category c m o, Eq o, Eq m) => FiniteCategory (InheritedSubcategory c m o) m o where
        ob :: InheritedSubcategory c m o -> Set o
ob (InheritedSubcategory c
_ Set o
o Set m
_) = Set o
o
            
    
    -- | Return the image 'Subcategory' of an embedding.

    --

    -- An embedding is a faithful 'Diagram' injective on objects.

    --

    -- Does not check that the 'Diagram' is an embedding.

    embeddingToSubcategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => Diagram c1 m1 o1 c2 m2 o2 -> Subcategory c2 m2 o2
    embeddingToSubcategory :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) =>
Diagram c1 m1 o1 c2 m2 o2 -> Subcategory c2 m2 o2
embeddingToSubcategory Diagram c1 m1 o1 c2 m2 o2
diag = c2 -> Set o2 -> Set m2 -> Subcategory c2 m2 o2
forall c m o. c -> Set o -> Set m -> Subcategory c m o
Subcategory (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) (Map o1 o2 -> Set o2
forall k a. Eq k => Map k a -> Set a
image (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)) (Map m1 m2 -> Set m2
forall k a. Eq k => Map k a -> Set a
image (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))
    
    -- | Return the image 'InheritedSubcategory' of an embedding.

    --

    -- An embedding is a faithful 'Diagram' injective on objects.

    --

    -- Does not check that the 'Diagram' is an embedding.

    embeddingToInheritedSubcategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => Diagram c1 m1 o1 c2 m2 o2 -> InheritedSubcategory c2 m2 o2
    embeddingToInheritedSubcategory :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) =>
Diagram c1 m1 o1 c2 m2 o2 -> InheritedSubcategory c2 m2 o2
embeddingToInheritedSubcategory Diagram c1 m1 o1 c2 m2 o2
diag = c2 -> Set o2 -> Set m2 -> InheritedSubcategory c2 m2 o2
forall c m o. c -> Set o -> Set m -> InheritedSubcategory c m o
InheritedSubcategory (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) (Map o1 o2 -> Set o2
forall k a. Eq k => Map k a -> Set a
image (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)) (Map m1 m2 -> Set m2
forall k a. Eq k => Map k a -> Set a
image (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))
    
    -- | Extracts a full and faithful diagram out of a faithful 'Diagram' injective on objects.

    --

    -- Does not check that the 'Diagram' is an embedding.

    fullDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => 
                    Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
    fullDiagram :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
fullDiagram Diagram c1 m1 o1 c2 m2 o2
diag = 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
diag, tgt :: Subcategory c2 m2 o2
tgt = Diagram c1 m1 o1 c2 m2 o2 -> Subcategory c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) =>
Diagram c1 m1 o1 c2 m2 o2 -> Subcategory c2 m2 o2
embeddingToSubcategory Diagram c1 m1 o1 c2 m2 o2
diag, omap :: Map o1 o2
omap = 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 m1 m2
mmap = 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}
    
    -- | Extracts a full and faithful diagram out of a faithful 'Diagram' injective on objects. The target subcategory is inherited (see 'InheritedFullSubcategory').

    --

    -- Does not check that the 'Diagram' is an embedding.

    fullDiagram2 :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => 
                    Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2
    fullDiagram2 :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2
fullDiagram2 Diagram c1 m1 o1 c2 m2 o2
diag = 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
diag, tgt :: InheritedSubcategory c2 m2 o2
tgt = Diagram c1 m1 o1 c2 m2 o2 -> InheritedSubcategory c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) =>
Diagram c1 m1 o1 c2 m2 o2 -> InheritedSubcategory c2 m2 o2
embeddingToInheritedSubcategory Diagram c1 m1 o1 c2 m2 o2
diag, omap :: Map o1 o2
omap = 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 m1 m2
mmap = 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}
    
    -- | Extracts full and faithful diagrams out of the source and target 'Diagram's of a 'NaturalTransformation'. The 'Diagram's should be a faithful and injective on objects.

    --

    -- Does not check that the 'Diagram's are embeddings.

    fullNaturalTransformation :: (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) => 
                    NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
    fullNaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
(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) =>
NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
fullNaturalTransformation NaturalTransformation c1 m1 o1 c2 m2 o2
nat = Diagram c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
-> Diagram c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
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 (Subcategory c2 m2 o2) m2 o2
sourceDiag Diagram c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
targetDiag (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
nat)
        where
            targetCat :: Subcategory c2 m2 o2
targetCat = c2 -> Set o2 -> Set m2 -> Subcategory c2 m2 o2
forall c m o. c -> Set o -> Set m -> Subcategory c m o
Subcategory (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (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
nat)) ((Map o1 o2 -> Set o2
forall k a. Eq k => Map k a -> Set a
image (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 (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
nat))) Set o2 -> Set o2 -> Set o2
forall a. Set a -> Set a -> Set a
||| (Map o1 o2 -> Set o2
forall k a. Eq k => Map k a -> Set a
image (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 (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
nat)))) ((Map m1 m2 -> Set m2
forall k a. Eq k => Map k a -> Set a
image (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 (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
nat))) Set m2 -> Set m2 -> Set m2
forall a. Set a -> Set a -> Set a
||| (Map m1 m2 -> Set m2
forall k a. Eq k => Map k a -> Set a
image (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 (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
nat))) Set m2 -> Set m2 -> Set m2
forall a. Set a -> Set a -> Set a
||| (Map o1 m2 -> Set m2
forall k a. Eq k => Map k a -> Set a
image (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
nat)))
            sourceDiag :: Diagram c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
sourceDiag = 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 (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
nat), tgt :: Subcategory c2 m2 o2
tgt=Subcategory c2 m2 o2
targetCat, omap :: Map o1 o2
omap=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 (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
nat), mmap :: Map m1 m2
mmap=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 (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
nat)}
            targetDiag :: Diagram c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
targetDiag = 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 (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
nat), tgt :: Subcategory c2 m2 o2
tgt=Subcategory c2 m2 o2
targetCat, omap :: Map o1 o2
omap=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 (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
nat), mmap :: Map m1 m2
mmap=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 (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
nat)}
            
    -- | Extracts full and faithful diagrams out of the source and target 'Diagram's of a 'NaturalTransformation'. The 'Diagram's should be a faithful and injective on objects. The target subcategory is inherited (see 'InheritedFullSubcategory').

    --

    -- Does not check that the 'Diagram's are embeddings.

    fullNaturalTransformation2 :: (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) => 
                    NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2
    fullNaturalTransformation2 :: forall c1 m1 o1 c2 m2 o2.
(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) =>
NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation
     c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2
fullNaturalTransformation2 NaturalTransformation c1 m1 o1 c2 m2 o2
nat = Diagram c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2
-> Diagram c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2
-> Map o1 m2
-> NaturalTransformation
     c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2
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 (InheritedSubcategory c2 m2 o2) m2 o2
sourceDiag Diagram c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2
targetDiag (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
nat)
        where
            targetCat :: InheritedSubcategory c2 m2 o2
targetCat = c2 -> Set o2 -> Set m2 -> InheritedSubcategory c2 m2 o2
forall c m o. c -> Set o -> Set m -> InheritedSubcategory c m o
InheritedSubcategory (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (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
nat)) ((Map o1 o2 -> Set o2
forall k a. Eq k => Map k a -> Set a
image (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 (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
nat))) Set o2 -> Set o2 -> Set o2
forall a. Set a -> Set a -> Set a
||| (Map o1 o2 -> Set o2
forall k a. Eq k => Map k a -> Set a
image (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 (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
nat)))) ((Map m1 m2 -> Set m2
forall k a. Eq k => Map k a -> Set a
image (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 (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
nat))) Set m2 -> Set m2 -> Set m2
forall a. Set a -> Set a -> Set a
||| (Map m1 m2 -> Set m2
forall k a. Eq k => Map k a -> Set a
image (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 (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
nat))) Set m2 -> Set m2 -> Set m2
forall a. Set a -> Set a -> Set a
||| (Map o1 m2 -> Set m2
forall k a. Eq k => Map k a -> Set a
image (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
nat)))
            sourceDiag :: Diagram c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2
sourceDiag = 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 (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
nat), tgt :: InheritedSubcategory c2 m2 o2
tgt=InheritedSubcategory c2 m2 o2
targetCat, omap :: Map o1 o2
omap=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 (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
nat), mmap :: Map m1 m2
mmap=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 (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
nat)}
            targetDiag :: Diagram c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2
targetDiag = 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 (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
nat), tgt :: InheritedSubcategory c2 m2 o2
tgt=InheritedSubcategory c2 m2 o2
targetCat, omap :: Map o1 o2
omap=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 (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
nat), mmap :: Map m1 m2
mmap=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 (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
nat)}