{-# LANGUAGE MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : Product category of two categories.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Product category of two categories.
-}
module ProductCategory.ProductCategory
(
firstObject,
firstMorphism,
firstCategory,
secondObject,
secondMorphism,
secondCategory,
ProductObject(..),
ProductMorphism(..),
ProductCategory(..),
)
where
    import FiniteCategory.FiniteCategory
    import Utils.CartesianProduct
    import IO.PrettyPrint
    
    -- | Object in a product category.

    data ProductObject o1 o2 = ProductObject o1 o2 deriving (ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
(ProductObject o1 o2 -> ProductObject o1 o2 -> Bool)
-> (ProductObject o1 o2 -> ProductObject o1 o2 -> Bool)
-> Eq (ProductObject o1 o2)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall o1 o2.
(Eq o1, Eq o2) =>
ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
/= :: ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
$c/= :: forall o1 o2.
(Eq o1, Eq o2) =>
ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
== :: ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
$c== :: forall o1 o2.
(Eq o1, Eq o2) =>
ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
Eq, Int -> ProductObject o1 o2 -> ShowS
[ProductObject o1 o2] -> ShowS
ProductObject o1 o2 -> String
(Int -> ProductObject o1 o2 -> ShowS)
-> (ProductObject o1 o2 -> String)
-> ([ProductObject o1 o2] -> ShowS)
-> Show (ProductObject o1 o2)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall o1 o2.
(Show o1, Show o2) =>
Int -> ProductObject o1 o2 -> ShowS
forall o1 o2. (Show o1, Show o2) => [ProductObject o1 o2] -> ShowS
forall o1 o2. (Show o1, Show o2) => ProductObject o1 o2 -> String
showList :: [ProductObject o1 o2] -> ShowS
$cshowList :: forall o1 o2. (Show o1, Show o2) => [ProductObject o1 o2] -> ShowS
show :: ProductObject o1 o2 -> String
$cshow :: forall o1 o2. (Show o1, Show o2) => ProductObject o1 o2 -> String
showsPrec :: Int -> ProductObject o1 o2 -> ShowS
$cshowsPrec :: forall o1 o2.
(Show o1, Show o2) =>
Int -> ProductObject o1 o2 -> ShowS
Show, Eq (ProductObject o1 o2)
Eq (ProductObject o1 o2)
-> (ProductObject o1 o2 -> ProductObject o1 o2 -> Ordering)
-> (ProductObject o1 o2 -> ProductObject o1 o2 -> Bool)
-> (ProductObject o1 o2 -> ProductObject o1 o2 -> Bool)
-> (ProductObject o1 o2 -> ProductObject o1 o2 -> Bool)
-> (ProductObject o1 o2 -> ProductObject o1 o2 -> Bool)
-> (ProductObject o1 o2
    -> ProductObject o1 o2 -> ProductObject o1 o2)
-> (ProductObject o1 o2
    -> ProductObject o1 o2 -> ProductObject o1 o2)
-> Ord (ProductObject o1 o2)
ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
ProductObject o1 o2 -> ProductObject o1 o2 -> Ordering
ProductObject o1 o2 -> ProductObject o1 o2 -> ProductObject o1 o2
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {o1} {o2}. (Ord o1, Ord o2) => Eq (ProductObject o1 o2)
forall o1 o2.
(Ord o1, Ord o2) =>
ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
forall o1 o2.
(Ord o1, Ord o2) =>
ProductObject o1 o2 -> ProductObject o1 o2 -> Ordering
forall o1 o2.
(Ord o1, Ord o2) =>
ProductObject o1 o2 -> ProductObject o1 o2 -> ProductObject o1 o2
min :: ProductObject o1 o2 -> ProductObject o1 o2 -> ProductObject o1 o2
$cmin :: forall o1 o2.
(Ord o1, Ord o2) =>
ProductObject o1 o2 -> ProductObject o1 o2 -> ProductObject o1 o2
max :: ProductObject o1 o2 -> ProductObject o1 o2 -> ProductObject o1 o2
$cmax :: forall o1 o2.
(Ord o1, Ord o2) =>
ProductObject o1 o2 -> ProductObject o1 o2 -> ProductObject o1 o2
>= :: ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
$c>= :: forall o1 o2.
(Ord o1, Ord o2) =>
ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
> :: ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
$c> :: forall o1 o2.
(Ord o1, Ord o2) =>
ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
<= :: ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
$c<= :: forall o1 o2.
(Ord o1, Ord o2) =>
ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
< :: ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
$c< :: forall o1 o2.
(Ord o1, Ord o2) =>
ProductObject o1 o2 -> ProductObject o1 o2 -> Bool
compare :: ProductObject o1 o2 -> ProductObject o1 o2 -> Ordering
$ccompare :: forall o1 o2.
(Ord o1, Ord o2) =>
ProductObject o1 o2 -> ProductObject o1 o2 -> Ordering
Ord)
    
    -- | Returns the first object of a product object.

    firstObject :: ProductObject o1 o2 -> o1
    firstObject :: forall o1 o2. ProductObject o1 o2 -> o1
firstObject (ProductObject o1
o1 o2
_) = o1
o1
    
    -- | Returns the second object of a product object.

    secondObject :: ProductObject o1 o2 -> o2
    secondObject :: forall o1 o2. ProductObject o1 o2 -> o2
secondObject (ProductObject o1
_ o2
o2) = o2
o2
    
    -- | Morphism in a product category.

    data ProductMorphism m1 o1 m2 o2 = ProductMorphism m1 m2 deriving (ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
(ProductMorphism m1 o1 m2 o2
 -> ProductMorphism m1 o1 m2 o2 -> Bool)
-> (ProductMorphism m1 o1 m2 o2
    -> ProductMorphism m1 o1 m2 o2 -> Bool)
-> Eq (ProductMorphism m1 o1 m2 o2)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall m1 o1 m2 o2.
(Eq m1, Eq m2) =>
ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
/= :: ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
$c/= :: forall m1 o1 m2 o2.
(Eq m1, Eq m2) =>
ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
== :: ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
$c== :: forall m1 o1 m2 o2.
(Eq m1, Eq m2) =>
ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
Eq, Int -> ProductMorphism m1 o1 m2 o2 -> ShowS
[ProductMorphism m1 o1 m2 o2] -> ShowS
ProductMorphism m1 o1 m2 o2 -> String
(Int -> ProductMorphism m1 o1 m2 o2 -> ShowS)
-> (ProductMorphism m1 o1 m2 o2 -> String)
-> ([ProductMorphism m1 o1 m2 o2] -> ShowS)
-> Show (ProductMorphism m1 o1 m2 o2)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall m1 o1 m2 o2.
(Show m1, Show m2) =>
Int -> ProductMorphism m1 o1 m2 o2 -> ShowS
forall m1 o1 m2 o2.
(Show m1, Show m2) =>
[ProductMorphism m1 o1 m2 o2] -> ShowS
forall m1 o1 m2 o2.
(Show m1, Show m2) =>
ProductMorphism m1 o1 m2 o2 -> String
showList :: [ProductMorphism m1 o1 m2 o2] -> ShowS
$cshowList :: forall m1 o1 m2 o2.
(Show m1, Show m2) =>
[ProductMorphism m1 o1 m2 o2] -> ShowS
show :: ProductMorphism m1 o1 m2 o2 -> String
$cshow :: forall m1 o1 m2 o2.
(Show m1, Show m2) =>
ProductMorphism m1 o1 m2 o2 -> String
showsPrec :: Int -> ProductMorphism m1 o1 m2 o2 -> ShowS
$cshowsPrec :: forall m1 o1 m2 o2.
(Show m1, Show m2) =>
Int -> ProductMorphism m1 o1 m2 o2 -> ShowS
Show, Eq (ProductMorphism m1 o1 m2 o2)
Eq (ProductMorphism m1 o1 m2 o2)
-> (ProductMorphism m1 o1 m2 o2
    -> ProductMorphism m1 o1 m2 o2 -> Ordering)
-> (ProductMorphism m1 o1 m2 o2
    -> ProductMorphism m1 o1 m2 o2 -> Bool)
-> (ProductMorphism m1 o1 m2 o2
    -> ProductMorphism m1 o1 m2 o2 -> Bool)
-> (ProductMorphism m1 o1 m2 o2
    -> ProductMorphism m1 o1 m2 o2 -> Bool)
-> (ProductMorphism m1 o1 m2 o2
    -> ProductMorphism m1 o1 m2 o2 -> Bool)
-> (ProductMorphism m1 o1 m2 o2
    -> ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2)
-> (ProductMorphism m1 o1 m2 o2
    -> ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2)
-> Ord (ProductMorphism m1 o1 m2 o2)
ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
ProductMorphism m1 o1 m2 o2
-> ProductMorphism m1 o1 m2 o2 -> Ordering
ProductMorphism m1 o1 m2 o2
-> ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {m1} {o1} {m2} {o2}.
(Ord m1, Ord m2) =>
Eq (ProductMorphism m1 o1 m2 o2)
forall m1 o1 m2 o2.
(Ord m1, Ord m2) =>
ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
forall m1 o1 m2 o2.
(Ord m1, Ord m2) =>
ProductMorphism m1 o1 m2 o2
-> ProductMorphism m1 o1 m2 o2 -> Ordering
forall m1 o1 m2 o2.
(Ord m1, Ord m2) =>
ProductMorphism m1 o1 m2 o2
-> ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2
min :: ProductMorphism m1 o1 m2 o2
-> ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2
$cmin :: forall m1 o1 m2 o2.
(Ord m1, Ord m2) =>
ProductMorphism m1 o1 m2 o2
-> ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2
max :: ProductMorphism m1 o1 m2 o2
-> ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2
$cmax :: forall m1 o1 m2 o2.
(Ord m1, Ord m2) =>
ProductMorphism m1 o1 m2 o2
-> ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2
>= :: ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
$c>= :: forall m1 o1 m2 o2.
(Ord m1, Ord m2) =>
ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
> :: ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
$c> :: forall m1 o1 m2 o2.
(Ord m1, Ord m2) =>
ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
<= :: ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
$c<= :: forall m1 o1 m2 o2.
(Ord m1, Ord m2) =>
ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
< :: ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
$c< :: forall m1 o1 m2 o2.
(Ord m1, Ord m2) =>
ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2 -> Bool
compare :: ProductMorphism m1 o1 m2 o2
-> ProductMorphism m1 o1 m2 o2 -> Ordering
$ccompare :: forall m1 o1 m2 o2.
(Ord m1, Ord m2) =>
ProductMorphism m1 o1 m2 o2
-> ProductMorphism m1 o1 m2 o2 -> Ordering
Ord)
    
    -- | Returns the first morphism of a product morphism.

    firstMorphism :: ProductMorphism m1 o1 m2 o2 -> m1
    firstMorphism :: forall m1 o1 m2 o2. ProductMorphism m1 o1 m2 o2 -> m1
firstMorphism (ProductMorphism m1
m1 m2
_) = m1
m1
    
    -- | Returns the second morphism of a product morphism.

    secondMorphism :: ProductMorphism m1 o1 m2 o2 -> m2
    secondMorphism :: forall m1 o1 m2 o2. ProductMorphism m1 o1 m2 o2 -> m2
secondMorphism (ProductMorphism m1
_ m2
m2) = m2
m2
    
    -- | Product category of two categories.

    data ProductCategory c1 m1 o1 c2 m2 o2 = ProductCategory c1 c2 deriving (ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
(ProductCategory c1 m1 o1 c2 m2 o2
 -> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool)
-> (ProductCategory c1 m1 o1 c2 m2 o2
    -> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool)
-> Eq (ProductCategory 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) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
/= :: ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
== :: ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
Eq, Int -> ProductCategory c1 m1 o1 c2 m2 o2 -> ShowS
[ProductCategory c1 m1 o1 c2 m2 o2] -> ShowS
ProductCategory c1 m1 o1 c2 m2 o2 -> String
(Int -> ProductCategory c1 m1 o1 c2 m2 o2 -> ShowS)
-> (ProductCategory c1 m1 o1 c2 m2 o2 -> String)
-> ([ProductCategory c1 m1 o1 c2 m2 o2] -> ShowS)
-> Show (ProductCategory 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 -> ProductCategory c1 m1 o1 c2 m2 o2 -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
[ProductCategory c1 m1 o1 c2 m2 o2] -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
ProductCategory c1 m1 o1 c2 m2 o2 -> String
showList :: [ProductCategory c1 m1 o1 c2 m2 o2] -> ShowS
$cshowList :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
[ProductCategory c1 m1 o1 c2 m2 o2] -> ShowS
show :: ProductCategory c1 m1 o1 c2 m2 o2 -> String
$cshow :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
ProductCategory c1 m1 o1 c2 m2 o2 -> String
showsPrec :: Int -> ProductCategory c1 m1 o1 c2 m2 o2 -> ShowS
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2) =>
Int -> ProductCategory c1 m1 o1 c2 m2 o2 -> ShowS
Show, Eq (ProductCategory c1 m1 o1 c2 m2 o2)
Eq (ProductCategory c1 m1 o1 c2 m2 o2)
-> (ProductCategory c1 m1 o1 c2 m2 o2
    -> ProductCategory c1 m1 o1 c2 m2 o2 -> Ordering)
-> (ProductCategory c1 m1 o1 c2 m2 o2
    -> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool)
-> (ProductCategory c1 m1 o1 c2 m2 o2
    -> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool)
-> (ProductCategory c1 m1 o1 c2 m2 o2
    -> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool)
-> (ProductCategory c1 m1 o1 c2 m2 o2
    -> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool)
-> (ProductCategory c1 m1 o1 c2 m2 o2
    -> ProductCategory c1 m1 o1 c2 m2 o2
    -> ProductCategory c1 m1 o1 c2 m2 o2)
-> (ProductCategory c1 m1 o1 c2 m2 o2
    -> ProductCategory c1 m1 o1 c2 m2 o2
    -> ProductCategory c1 m1 o1 c2 m2 o2)
-> Ord (ProductCategory c1 m1 o1 c2 m2 o2)
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Ordering
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {c1} {m1} {o1} {c2} {m2} {o2}.
(Ord c1, Ord c2) =>
Eq (ProductCategory c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 c2 m2 o2.
(Ord c1, Ord c2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
forall c1 m1 o1 c2 m2 o2.
(Ord c1, Ord c2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Ordering
forall c1 m1 o1 c2 m2 o2.
(Ord c1, Ord c2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2
min :: ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2
$cmin :: forall c1 m1 o1 c2 m2 o2.
(Ord c1, Ord c2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2
max :: ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2
$cmax :: forall c1 m1 o1 c2 m2 o2.
(Ord c1, Ord c2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2
>= :: ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
$c>= :: forall c1 m1 o1 c2 m2 o2.
(Ord c1, Ord c2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
> :: ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
$c> :: forall c1 m1 o1 c2 m2 o2.
(Ord c1, Ord c2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
<= :: ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
$c<= :: forall c1 m1 o1 c2 m2 o2.
(Ord c1, Ord c2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
< :: ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
$c< :: forall c1 m1 o1 c2 m2 o2.
(Ord c1, Ord c2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Bool
compare :: ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Ordering
$ccompare :: forall c1 m1 o1 c2 m2 o2.
(Ord c1, Ord c2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductCategory c1 m1 o1 c2 m2 o2 -> Ordering
Ord)

    -- | Returns the first category of a product category.

    firstCategory :: ProductCategory c1 m1 o1 c2 m2 o2 -> c1
    firstCategory :: forall c1 m1 o1 c2 m2 o2. ProductCategory c1 m1 o1 c2 m2 o2 -> c1
firstCategory (ProductCategory c1
c1 c2
_) = c1
c1
    
    -- | Returns the second category of a product category.

    secondCategory :: ProductCategory c1 m1 o1 c2 m2 o2 -> c2
    secondCategory :: forall c1 m1 o1 c2 m2 o2. ProductCategory c1 m1 o1 c2 m2 o2 -> c2
secondCategory (ProductCategory c1
_ c2
c2) = c2
c2

    instance (Morphism m1 o1, Morphism m2 o2) => Morphism (ProductMorphism m1 o1 m2 o2) (ProductObject o1 o2) where
        source :: ProductMorphism m1 o1 m2 o2 -> ProductObject o1 o2
source (ProductMorphism m1
m1 m2
m2) = o1 -> o2 -> ProductObject o1 o2
forall o1 o2. o1 -> o2 -> ProductObject o1 o2
ProductObject (m1 -> o1
forall m o. Morphism m o => m -> o
source m1
m1) (m2 -> o2
forall m o. Morphism m o => m -> o
source m2
m2)
        target :: ProductMorphism m1 o1 m2 o2 -> ProductObject o1 o2
target (ProductMorphism m1
m1 m2
m2) = o1 -> o2 -> ProductObject o1 o2
forall o1 o2. o1 -> o2 -> ProductObject o1 o2
ProductObject (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
m1) (m2 -> o2
forall m o. Morphism m o => m -> o
target m2
m2)
        (ProductMorphism m1
g1 m2
g2) @ :: ProductMorphism m1 o1 m2 o2
-> ProductMorphism m1 o1 m2 o2 -> ProductMorphism m1 o1 m2 o2
@ (ProductMorphism m1
f1 m2
f2) = m1 -> m2 -> ProductMorphism m1 o1 m2 o2
forall m1 o1 m2 o2. m1 -> m2 -> ProductMorphism m1 o1 m2 o2
ProductMorphism (m1
g1 m1 -> m1 -> m1
forall m o. Morphism m o => m -> m -> m
@ m1
f1) (m2
g2 m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ m2
f2)
                                                
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2) =>
              FiniteCategory (ProductCategory c1 m1 o1 c2 m2 o2) (ProductMorphism m1 o1 m2 o2) (ProductObject o1 o2) where
        ob :: ProductCategory c1 m1 o1 c2 m2 o2 -> [ProductObject o1 o2]
ob (ProductCategory c1
c1 c2
c2) = [o1 -> o2 -> ProductObject o1 o2
forall o1 o2. o1 -> o2 -> ProductObject o1 o2
ProductObject o1
a o2
b | o1
a <- (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob c1
c1), o2
b <- (c2 -> [o2]
forall c m o. FiniteCategory c m o => c -> [o]
ob c2
c2)]
        identity :: Morphism (ProductMorphism m1 o1 m2 o2) (ProductObject o1 o2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductObject o1 o2 -> ProductMorphism m1 o1 m2 o2
identity (ProductCategory c1
c1 c2
c2) (ProductObject o1
a o2
b) = m1 -> m2 -> ProductMorphism m1 o1 m2 o2
forall m1 o1 m2 o2. m1 -> m2 -> ProductMorphism m1 o1 m2 o2
ProductMorphism (c1 -> o1 -> m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c1
c1 o1
a) (c2 -> o2 -> m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c2
c2 o2
b)
        ar :: Morphism (ProductMorphism m1 o1 m2 o2) (ProductObject o1 o2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductObject o1 o2
-> ProductObject o1 o2
-> [ProductMorphism m1 o1 m2 o2]
ar (ProductCategory c1
c1 c2
c2) (ProductObject o1
s1 o2
s2) (ProductObject o1
t1 o2
t2) = [m1 -> m2 -> ProductMorphism m1 o1 m2 o2
forall m1 o1 m2 o2. m1 -> m2 -> ProductMorphism m1 o1 m2 o2
ProductMorphism m1
m1 m2
m2 | m1
m1 <- c1 -> o1 -> o1 -> [m1]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c1
c1 o1
s1 o1
t1, m2
m2 <- c2 -> o2 -> o2 -> [m2]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c2
c2 o2
s2 o2
t2]
        
    instance (GeneratedFiniteCategory c1 m1 o1, Morphism m1 o1,
              GeneratedFiniteCategory c2 m2 o2, Morphism m2 o2) =>
              GeneratedFiniteCategory (ProductCategory c1 m1 o1 c2 m2 o2) (ProductMorphism m1 o1 m2 o2) (ProductObject o1 o2) where
        genAr :: Morphism (ProductMorphism m1 o1 m2 o2) (ProductObject o1 o2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductObject o1 o2
-> ProductObject o1 o2
-> [ProductMorphism m1 o1 m2 o2]
genAr (ProductCategory c1
c1 c2
c2) (ProductObject o1
s1 o2
s2) (ProductObject o1
t1 o2
t2) = [m1 -> m2 -> ProductMorphism m1 o1 m2 o2
forall m1 o1 m2 o2. m1 -> m2 -> ProductMorphism m1 o1 m2 o2
ProductMorphism m1
m1 m2
m2 | m1
m1 <- c1 -> o1 -> o1 -> [m1]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
genAr c1
c1 o1
s1 o1
t1, m2
m2 <- c2 -> o2 -> o2 -> [m2]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
genAr c2
c2 o2
s2 o2
t2]
        decompose :: Morphism (ProductMorphism m1 o1 m2 o2) (ProductObject o1 o2) =>
ProductCategory c1 m1 o1 c2 m2 o2
-> ProductMorphism m1 o1 m2 o2 -> [ProductMorphism m1 o1 m2 o2]
decompose (ProductCategory c1
c1 c2
c2) (ProductMorphism m1
m1 m2
m2) = [m1 -> m2 -> ProductMorphism m1 o1 m2 o2
forall m1 o1 m2 o2. m1 -> m2 -> ProductMorphism m1 o1 m2 o2
ProductMorphism m1
d1 m2
d2 | m1
d1 <- [m1]
decompoExtended1, m2
d2 <- [m2]
decompoExtended2]
            where
                decompo1 :: [m1]
decompo1 = c1 -> m1 -> [m1]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
decompose c1
c1 m1
m1
                decompo2 :: [m2]
decompo2 = c2 -> m2 -> [m2]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
decompose c2
c2 m2
m2
                decompoExtended1 :: [m1]
decompoExtended1 = if (([m1] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [m1]
decompo1) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< ([m2] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [m2]
decompo2)) then (Int -> m1 -> [m1]
forall a. Int -> a -> [a]
replicate (([m2] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [m2]
decompo2)Int -> Int -> Int
forall a. Num a => a -> a -> a
-([m1] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [m1]
decompo1)) (c1 -> o1 -> m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c1
c1 (m1 -> o1
forall m o. Morphism m o => m -> o
target ([m1] -> m1
forall a. [a] -> a
head [m1]
decompo1))))[m1] -> [m1] -> [m1]
forall a. [a] -> [a] -> [a]
++[m1]
decompo1 else [m1]
decompo1
                decompoExtended2 :: [m2]
decompoExtended2 = if (([m2] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [m2]
decompo2) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< ([m1] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [m1]
decompo1)) then (Int -> m2 -> [m2]
forall a. Int -> a -> [a]
replicate (([m1] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [m1]
decompo1)Int -> Int -> Int
forall a. Num a => a -> a -> a
-([m2] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [m2]
decompo2)) (c2 -> o2 -> m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c2
c2 (m2 -> o2
forall m o. Morphism m o => m -> o
target ([m2] -> m2
forall a. [a] -> a
head [m2]
decompo2))))[m2] -> [m2] -> [m2]
forall a. [a] -> [a] -> [a]
++[m2]
decompo2 else [m2]
decompo2
                
    instance (PrettyPrintable o1, PrettyPrintable o2) => PrettyPrintable (ProductObject o1 o2) where
        pprint :: ProductObject o1 o2 -> String
pprint (ProductObject o1
a o2
b) = String
"<"String -> ShowS
forall a. [a] -> [a] -> [a]
++(o1 -> String
forall a. PrettyPrintable a => a -> String
pprint o1
a)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
","String -> ShowS
forall a. [a] -> [a] -> [a]
++(o2 -> String
forall a. PrettyPrintable a => a -> String
pprint o2
b)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
">"
        
    
    instance (PrettyPrintable m1, PrettyPrintable m2) => PrettyPrintable (ProductMorphism m1 o1 m2 o2) where
        pprint :: ProductMorphism m1 o1 m2 o2 -> String
pprint (ProductMorphism m1
f m2
g) = String
"<"String -> ShowS
forall a. [a] -> [a] -> [a]
++(m1 -> String
forall a. PrettyPrintable a => a -> String
pprint m1
f)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
","String -> ShowS
forall a. [a] -> [a] -> [a]
++(m2 -> String
forall a. PrettyPrintable a => a -> String
pprint m2
g)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
">"