{-# LANGUAGE UndecidableInstances, FlexibleInstances, MultiParamTypeClasses #-}
module Math.FiniteCategories.Subcategory
(
Subcategory,
unsafeSubcategory,
subcategory,
originalCategory,
embeddingToSubcategory,
fullDiagram,
fullNaturalTransformation,
InheritedSubcategory,
unsafeInheritedSubcategory,
inheritedSubcategory,
originalCategory2,
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
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)
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
")"
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
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
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
instance (PrettyPrint c, PrettyPrint m, PrettyPrint o, Eq o, Eq m) => PrettyPrint (Subcategory c m o) where
pprint :: Subcategory c m o -> String
pprint (Subcategory c
c Set o
o Set m
m) = String
"FullSubcategory("String -> ShowS
forall a. [a] -> [a] -> [a]
++ c -> String
forall a. PrettyPrint a => a -> String
pprint c
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
","String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set o -> String
forall a. PrettyPrint a => a -> String
pprint Set o
o String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set m -> String
forall a. PrettyPrint a => a -> String
pprint Set m
m String -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"
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)
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
")"
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
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
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
instance (PrettyPrint c, PrettyPrint m, PrettyPrint o, Eq o, Eq m) => PrettyPrint (InheritedSubcategory c m o) where
pprint :: InheritedSubcategory c m o -> String
pprint (InheritedSubcategory c
c Set o
o Set m
m) = String
"InheritedFullSubcategory("String -> ShowS
forall a. [a] -> [a] -> [a]
++ c -> String
forall a. PrettyPrint a => a -> String
pprint c
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
","String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set o -> String
forall a. PrettyPrint a => a -> String
pprint Set o
o String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set m -> String
forall a. PrettyPrint a => a -> String
pprint Set m
m String -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"
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))
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))
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}
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}
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)}
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)}