{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}

{-| Module  : FiniteCategories
Description : Each 'Category' has an opposite one where morphisms are reversed.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Each 'Category' has an opposite one where morphisms are reversed.
-}

module Math.Categories.Opposite
(
    OpMorphism(..),
    opOpMorphism,
    Op(..),
    opOp,
)
where
    import          Math.Category
    import          Math.FiniteCategory
    import          Math.IO.PrettyPrint
    
    import          Data.WeakSet.Safe
    
    -- | An 'OpMorphism' is a morphism where source and target are reversed.

    data OpMorphism m = OpMorphism m deriving (OpMorphism m -> OpMorphism m -> Bool
(OpMorphism m -> OpMorphism m -> Bool)
-> (OpMorphism m -> OpMorphism m -> Bool) -> Eq (OpMorphism m)
forall m. Eq m => OpMorphism m -> OpMorphism m -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall m. Eq m => OpMorphism m -> OpMorphism m -> Bool
== :: OpMorphism m -> OpMorphism m -> Bool
$c/= :: forall m. Eq m => OpMorphism m -> OpMorphism m -> Bool
/= :: OpMorphism m -> OpMorphism m -> Bool
Eq, Int -> OpMorphism m -> ShowS
[OpMorphism m] -> ShowS
OpMorphism m -> String
(Int -> OpMorphism m -> ShowS)
-> (OpMorphism m -> String)
-> ([OpMorphism m] -> ShowS)
-> Show (OpMorphism m)
forall m. Show m => Int -> OpMorphism m -> ShowS
forall m. Show m => [OpMorphism m] -> ShowS
forall m. Show m => OpMorphism m -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall m. Show m => Int -> OpMorphism m -> ShowS
showsPrec :: Int -> OpMorphism m -> ShowS
$cshow :: forall m. Show m => OpMorphism m -> String
show :: OpMorphism m -> String
$cshowList :: forall m. Show m => [OpMorphism m] -> ShowS
showList :: [OpMorphism m] -> ShowS
Show)
    
    -- | Return the original morphism given an 'OpMorphism'.

    opOpMorphism :: OpMorphism m -> m
    opOpMorphism :: forall m. OpMorphism m -> m
opOpMorphism (OpMorphism m
m) = m
m
    
    instance (Morphism m o) => Morphism (OpMorphism m) o where
        source :: OpMorphism m -> o
source (OpMorphism m
m) = m -> o
forall m o. Morphism m o => m -> o
target m
m
        target :: OpMorphism m -> o
target (OpMorphism m
m) = m -> o
forall m o. Morphism m o => m -> o
source m
m
        @? :: OpMorphism m -> OpMorphism m -> Maybe (OpMorphism m)
(@?) (OpMorphism m
m2) (OpMorphism m
m1) = m -> OpMorphism m
forall m. m -> OpMorphism m
OpMorphism (m -> OpMorphism m) -> Maybe m -> Maybe (OpMorphism m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m
m1 m -> m -> Maybe m
forall m o. Morphism m o => m -> m -> Maybe m
@? m
m2
    
    -- | The 'Op' operator gives the opposite of a 'Category'.

    data Op c = Op c deriving (Op c -> Op c -> Bool
(Op c -> Op c -> Bool) -> (Op c -> Op c -> Bool) -> Eq (Op c)
forall c. Eq c => Op c -> Op c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall c. Eq c => Op c -> Op c -> Bool
== :: Op c -> Op c -> Bool
$c/= :: forall c. Eq c => Op c -> Op c -> Bool
/= :: Op c -> Op c -> Bool
Eq, Int -> Op c -> ShowS
[Op c] -> ShowS
Op c -> String
(Int -> Op c -> ShowS)
-> (Op c -> String) -> ([Op c] -> ShowS) -> Show (Op c)
forall c. Show c => Int -> Op c -> ShowS
forall c. Show c => [Op c] -> ShowS
forall c. Show c => Op c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall c. Show c => Int -> Op c -> ShowS
showsPrec :: Int -> Op c -> ShowS
$cshow :: forall c. Show c => Op c -> String
show :: Op c -> String
$cshowList :: forall c. Show c => [Op c] -> ShowS
showList :: [Op c] -> ShowS
Show)
    
    -- | Return the original category given an 'Op' category.

    opOp :: Op c -> c
    opOp :: forall c. Op c -> c
opOp (Op c
c) = c
c
    
    instance (Category c m o, Morphism m o) => Category (Op c) (OpMorphism m) o where
        identity :: Morphism (OpMorphism m) o => Op c -> o -> OpMorphism m
identity (Op c
c) o
o = m -> OpMorphism m
forall m. m -> OpMorphism m
OpMorphism (m -> OpMorphism m) -> m -> OpMorphism m
forall a b. (a -> b) -> a -> b
$ c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c o
o
        ar :: Morphism (OpMorphism m) o => Op c -> o -> o -> Set (OpMorphism m)
ar (Op c
c) o
x o
y = m -> OpMorphism m
forall m. m -> OpMorphism m
OpMorphism (m -> OpMorphism m) -> Set m -> Set (OpMorphism m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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
y o
x
        genAr :: Morphism (OpMorphism m) o => Op c -> o -> o -> Set (OpMorphism m)
genAr (Op c
c) o
x o
y = m -> OpMorphism m
forall m. m -> OpMorphism m
OpMorphism (m -> OpMorphism m) -> Set m -> Set (OpMorphism m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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
y o
x
        decompose :: Morphism (OpMorphism m) o => Op c -> OpMorphism m -> [OpMorphism m]
decompose (Op c
c) (OpMorphism m
m) = m -> OpMorphism m
forall m. m -> OpMorphism m
OpMorphism (m -> OpMorphism m) -> [m] -> [OpMorphism m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m] -> [m]
forall a. [a] -> [a]
reverse (c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
c m
m)
    
    instance (FiniteCategory c m o, Morphism m o) => FiniteCategory (Op c) (OpMorphism m) o where
        ob :: Op c -> Set o
ob (Op c
c) = c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c
    
    instance (PrettyPrint m) => PrettyPrint (OpMorphism m) where
        pprint :: OpMorphism m -> String
pprint (OpMorphism m
m) = String
"Op("String -> ShowS
forall a. [a] -> [a] -> [a]
++ m -> String
forall a. PrettyPrint a => a -> String
pprint m
m String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
    
    instance (PrettyPrint c) => PrettyPrint (Op c) where
        pprint :: Op c -> String
pprint (Op c
x) = String
"Op("String -> ShowS
forall a. [a] -> [a] -> [a]
++ c -> String
forall a. PrettyPrint a => a -> String
pprint c
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"