{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}

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

The opposite of a category is a category with reversed arrows.
-}

module OppositeCategory.OppositeCategory
(
    OppositeMorphism(..),
    OppositeCategory(..),
    opOpMorph,
    opOp
)
where
    import FiniteCategory.FiniteCategory
    import IO.PrettyPrint
    
    -- | Morphism in an opposite category.

    data OppositeMorphism m o = OpMorph m deriving (OppositeMorphism m o -> OppositeMorphism m o -> Bool
(OppositeMorphism m o -> OppositeMorphism m o -> Bool)
-> (OppositeMorphism m o -> OppositeMorphism m o -> Bool)
-> Eq (OppositeMorphism m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall m o.
Eq m =>
OppositeMorphism m o -> OppositeMorphism m o -> Bool
/= :: OppositeMorphism m o -> OppositeMorphism m o -> Bool
$c/= :: forall m o.
Eq m =>
OppositeMorphism m o -> OppositeMorphism m o -> Bool
== :: OppositeMorphism m o -> OppositeMorphism m o -> Bool
$c== :: forall m o.
Eq m =>
OppositeMorphism m o -> OppositeMorphism m o -> Bool
Eq, Int -> OppositeMorphism m o -> ShowS
[OppositeMorphism m o] -> ShowS
OppositeMorphism m o -> String
(Int -> OppositeMorphism m o -> ShowS)
-> (OppositeMorphism m o -> String)
-> ([OppositeMorphism m o] -> ShowS)
-> Show (OppositeMorphism m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall m o. Show m => Int -> OppositeMorphism m o -> ShowS
forall m o. Show m => [OppositeMorphism m o] -> ShowS
forall m o. Show m => OppositeMorphism m o -> String
showList :: [OppositeMorphism m o] -> ShowS
$cshowList :: forall m o. Show m => [OppositeMorphism m o] -> ShowS
show :: OppositeMorphism m o -> String
$cshow :: forall m o. Show m => OppositeMorphism m o -> String
showsPrec :: Int -> OppositeMorphism m o -> ShowS
$cshowsPrec :: forall m o. Show m => Int -> OppositeMorphism m o -> ShowS
Show, Eq (OppositeMorphism m o)
Eq (OppositeMorphism m o)
-> (OppositeMorphism m o -> OppositeMorphism m o -> Ordering)
-> (OppositeMorphism m o -> OppositeMorphism m o -> Bool)
-> (OppositeMorphism m o -> OppositeMorphism m o -> Bool)
-> (OppositeMorphism m o -> OppositeMorphism m o -> Bool)
-> (OppositeMorphism m o -> OppositeMorphism m o -> Bool)
-> (OppositeMorphism m o
    -> OppositeMorphism m o -> OppositeMorphism m o)
-> (OppositeMorphism m o
    -> OppositeMorphism m o -> OppositeMorphism m o)
-> Ord (OppositeMorphism m o)
OppositeMorphism m o -> OppositeMorphism m o -> Bool
OppositeMorphism m o -> OppositeMorphism m o -> Ordering
OppositeMorphism m o
-> OppositeMorphism m o -> OppositeMorphism m o
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 {m} {o}. Ord m => Eq (OppositeMorphism m o)
forall m o.
Ord m =>
OppositeMorphism m o -> OppositeMorphism m o -> Bool
forall m o.
Ord m =>
OppositeMorphism m o -> OppositeMorphism m o -> Ordering
forall m o.
Ord m =>
OppositeMorphism m o
-> OppositeMorphism m o -> OppositeMorphism m o
min :: OppositeMorphism m o
-> OppositeMorphism m o -> OppositeMorphism m o
$cmin :: forall m o.
Ord m =>
OppositeMorphism m o
-> OppositeMorphism m o -> OppositeMorphism m o
max :: OppositeMorphism m o
-> OppositeMorphism m o -> OppositeMorphism m o
$cmax :: forall m o.
Ord m =>
OppositeMorphism m o
-> OppositeMorphism m o -> OppositeMorphism m o
>= :: OppositeMorphism m o -> OppositeMorphism m o -> Bool
$c>= :: forall m o.
Ord m =>
OppositeMorphism m o -> OppositeMorphism m o -> Bool
> :: OppositeMorphism m o -> OppositeMorphism m o -> Bool
$c> :: forall m o.
Ord m =>
OppositeMorphism m o -> OppositeMorphism m o -> Bool
<= :: OppositeMorphism m o -> OppositeMorphism m o -> Bool
$c<= :: forall m o.
Ord m =>
OppositeMorphism m o -> OppositeMorphism m o -> Bool
< :: OppositeMorphism m o -> OppositeMorphism m o -> Bool
$c< :: forall m o.
Ord m =>
OppositeMorphism m o -> OppositeMorphism m o -> Bool
compare :: OppositeMorphism m o -> OppositeMorphism m o -> Ordering
$ccompare :: forall m o.
Ord m =>
OppositeMorphism m o -> OppositeMorphism m o -> Ordering
Ord)
    
    -- | Transforms back an opposite morphism into the original morphism.

    opOpMorph :: OppositeMorphism m o -> m
    opOpMorph :: forall m o. OppositeMorphism m o -> m
opOpMorph (OpMorph m
m) = m
m
    
    instance (Morphism m o) => Morphism (OppositeMorphism m o) o where
        source :: OppositeMorphism m o -> o
source (OpMorph m
m) = m -> o
forall m o. Morphism m o => m -> o
target m
m
        target :: OppositeMorphism m o -> o
target (OpMorph m
m) = m -> o
forall m o. Morphism m o => m -> o
source m
m
        @ :: OppositeMorphism m o
-> OppositeMorphism m o -> OppositeMorphism m o
(@) (OpMorph m
g) (OpMorph m
f) = m -> OppositeMorphism m o
forall m o. m -> OppositeMorphism m o
OpMorph (m -> OppositeMorphism m o) -> m -> OppositeMorphism m o
forall a b. (a -> b) -> a -> b
$ m
f m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
g
        
    instance (PrettyPrintable m) => PrettyPrintable (OppositeMorphism m o) where
        pprint :: OppositeMorphism m o -> String
pprint (OpMorph m
m) = String
"Op "String -> ShowS
forall a. [a] -> [a] -> [a]
++(m -> String
forall a. PrettyPrintable a => a -> String
pprint m
m)
        
    -- | Opposite category of a given category.

    data OppositeCategory c m o = Op c deriving (OppositeCategory c m o -> OppositeCategory c m o -> Bool
(OppositeCategory c m o -> OppositeCategory c m o -> Bool)
-> (OppositeCategory c m o -> OppositeCategory c m o -> Bool)
-> Eq (OppositeCategory c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o.
Eq c =>
OppositeCategory c m o -> OppositeCategory c m o -> Bool
/= :: OppositeCategory c m o -> OppositeCategory c m o -> Bool
$c/= :: forall c m o.
Eq c =>
OppositeCategory c m o -> OppositeCategory c m o -> Bool
== :: OppositeCategory c m o -> OppositeCategory c m o -> Bool
$c== :: forall c m o.
Eq c =>
OppositeCategory c m o -> OppositeCategory c m o -> Bool
Eq, Int -> OppositeCategory c m o -> ShowS
[OppositeCategory c m o] -> ShowS
OppositeCategory c m o -> String
(Int -> OppositeCategory c m o -> ShowS)
-> (OppositeCategory c m o -> String)
-> ([OppositeCategory c m o] -> ShowS)
-> Show (OppositeCategory c m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c m o. Show c => Int -> OppositeCategory c m o -> ShowS
forall c m o. Show c => [OppositeCategory c m o] -> ShowS
forall c m o. Show c => OppositeCategory c m o -> String
showList :: [OppositeCategory c m o] -> ShowS
$cshowList :: forall c m o. Show c => [OppositeCategory c m o] -> ShowS
show :: OppositeCategory c m o -> String
$cshow :: forall c m o. Show c => OppositeCategory c m o -> String
showsPrec :: Int -> OppositeCategory c m o -> ShowS
$cshowsPrec :: forall c m o. Show c => Int -> OppositeCategory c m o -> ShowS
Show, Eq (OppositeCategory c m o)
Eq (OppositeCategory c m o)
-> (OppositeCategory c m o -> OppositeCategory c m o -> Ordering)
-> (OppositeCategory c m o -> OppositeCategory c m o -> Bool)
-> (OppositeCategory c m o -> OppositeCategory c m o -> Bool)
-> (OppositeCategory c m o -> OppositeCategory c m o -> Bool)
-> (OppositeCategory c m o -> OppositeCategory c m o -> Bool)
-> (OppositeCategory c m o
    -> OppositeCategory c m o -> OppositeCategory c m o)
-> (OppositeCategory c m o
    -> OppositeCategory c m o -> OppositeCategory c m o)
-> Ord (OppositeCategory c m o)
OppositeCategory c m o -> OppositeCategory c m o -> Bool
OppositeCategory c m o -> OppositeCategory c m o -> Ordering
OppositeCategory c m o
-> OppositeCategory c m o -> OppositeCategory c m o
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 {c} {m} {o}. Ord c => Eq (OppositeCategory c m o)
forall c m o.
Ord c =>
OppositeCategory c m o -> OppositeCategory c m o -> Bool
forall c m o.
Ord c =>
OppositeCategory c m o -> OppositeCategory c m o -> Ordering
forall c m o.
Ord c =>
OppositeCategory c m o
-> OppositeCategory c m o -> OppositeCategory c m o
min :: OppositeCategory c m o
-> OppositeCategory c m o -> OppositeCategory c m o
$cmin :: forall c m o.
Ord c =>
OppositeCategory c m o
-> OppositeCategory c m o -> OppositeCategory c m o
max :: OppositeCategory c m o
-> OppositeCategory c m o -> OppositeCategory c m o
$cmax :: forall c m o.
Ord c =>
OppositeCategory c m o
-> OppositeCategory c m o -> OppositeCategory c m o
>= :: OppositeCategory c m o -> OppositeCategory c m o -> Bool
$c>= :: forall c m o.
Ord c =>
OppositeCategory c m o -> OppositeCategory c m o -> Bool
> :: OppositeCategory c m o -> OppositeCategory c m o -> Bool
$c> :: forall c m o.
Ord c =>
OppositeCategory c m o -> OppositeCategory c m o -> Bool
<= :: OppositeCategory c m o -> OppositeCategory c m o -> Bool
$c<= :: forall c m o.
Ord c =>
OppositeCategory c m o -> OppositeCategory c m o -> Bool
< :: OppositeCategory c m o -> OppositeCategory c m o -> Bool
$c< :: forall c m o.
Ord c =>
OppositeCategory c m o -> OppositeCategory c m o -> Bool
compare :: OppositeCategory c m o -> OppositeCategory c m o -> Ordering
$ccompare :: forall c m o.
Ord c =>
OppositeCategory c m o -> OppositeCategory c m o -> Ordering
Ord)
    
    -- | Transforms an opposite category into the original category.

    opOp :: OppositeCategory c m o -> c
    opOp :: forall c m o. OppositeCategory c m o -> c
opOp (Op c
c) = c
c
    
    instance (FiniteCategory c m o, Morphism m o) => FiniteCategory (OppositeCategory c m o) (OppositeMorphism m o) o where
        ob :: OppositeCategory c m o -> [o]
ob (Op c
c) = c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c
        identity :: Morphism (OppositeMorphism m o) o =>
OppositeCategory c m o -> o -> OppositeMorphism m o
identity (Op c
c) o
o = m -> OppositeMorphism m o
forall m o. m -> OppositeMorphism m o
OpMorph (m -> OppositeMorphism m o) -> m -> OppositeMorphism m o
forall a b. (a -> b) -> a -> b
$ c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
c o
o
        ar :: Morphism (OppositeMorphism m o) o =>
OppositeCategory c m o -> o -> o -> [OppositeMorphism m o]
ar (Op c
c) o
s o
t = m -> OppositeMorphism m o
forall m o. m -> OppositeMorphism m o
OpMorph (m -> OppositeMorphism m o) -> [m] -> [OppositeMorphism m o]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c o
t o
s
    
    instance (GeneratedFiniteCategory c m o, Morphism m o) => GeneratedFiniteCategory (OppositeCategory c m o) (OppositeMorphism m o) o where
        genAr :: Morphism (OppositeMorphism m o) o =>
OppositeCategory c m o -> o -> o -> [OppositeMorphism m o]
genAr (Op c
c) o
s o
t = m -> OppositeMorphism m o
forall m o. m -> OppositeMorphism m o
OpMorph (m -> OppositeMorphism m o) -> [m] -> [OppositeMorphism m o]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> o -> o -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
genAr c
c o
t o
s
        decompose :: Morphism (OppositeMorphism m o) o =>
OppositeCategory c m o
-> OppositeMorphism m o -> [OppositeMorphism m o]
decompose (Op c
c) (OpMorph m
m) = m -> OppositeMorphism m o
forall m o. m -> OppositeMorphism m o
OpMorph (m -> OppositeMorphism m o) -> [m] -> [OppositeMorphism m o]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> m -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
decompose c
c m
m
        
    instance (PrettyPrintable c) => PrettyPrintable (OppositeCategory c m o) where
        pprint :: OppositeCategory c m o -> String
pprint (Op c
cat) = String
"Op "String -> ShowS
forall a. [a] -> [a] -> [a]
++(c -> String
forall a. PrettyPrintable a => a -> String
pprint c
cat)