Opposite.hs

{-# 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 (Eq, Show)
    
    -- | Return the original morphism given an 'OpMorphism'.
    opOpMorphism :: OpMorphism m -> m
    opOpMorphism (OpMorphism m) = m
    
    instance (Morphism m o) => Morphism (OpMorphism m) o where
        source (OpMorphism m) = target m
        target (OpMorphism m) = source m
        (@?) (OpMorphism m2) (OpMorphism m1) = OpMorphism <$> m1 @? m2
    
    -- | The 'Op' operator gives the opposite of a 'Category'.
    data Op c = Op c deriving (Eq, Show)
    
    -- | Return the original category given an 'Op' category.
    opOp :: Op c -> c
    opOp (Op c) = c
    
    instance (Category c m o, Morphism m o) => Category (Op c) (OpMorphism m) o where
        identity (Op c) o = OpMorphism $ identity c o
        ar (Op c) x y = OpMorphism <$> ar c y x
        genAr (Op c) x y = OpMorphism <$> genAr c y x
        decompose (Op c) (OpMorphism m) = OpMorphism <$> reverse (decompose c m)
    
    instance (FiniteCategory c m o, Morphism m o) => FiniteCategory (Op c) (OpMorphism m) o where
        ob (Op c) = ob c
    
    instance (PrettyPrint m) => PrettyPrint (OpMorphism m) where
        pprint (OpMorphism m) = "Op("++ pprint m ++ ")"
    
    instance (PrettyPrint c) => PrettyPrint (Op c) where
        pprint (Op x) = "Op("++ pprint x ++ ")"