{-# 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 (Eq, Show, Ord)
    
    -- | Transforms back an opposite morphism into the original morphism.
    opOpMorph :: OppositeMorphism m o -> m
    opOpMorph (OpMorph m) = m
    
    instance (Morphism m o) => Morphism (OppositeMorphism m o) o where
        source (OpMorph m) = target m
        target (OpMorph m) = source m
        (@) (OpMorph g) (OpMorph f) = OpMorph $ f @ g
        
    instance (PrettyPrintable m) => PrettyPrintable (OppositeMorphism m o) where
        pprint (OpMorph m) = "Op "++(pprint m)
        
    -- | Opposite category of a given category.
    data OppositeCategory c m o = Op c deriving (Eq, Show, Ord)
    
    -- | Transforms an opposite category into the original category.
    opOp :: OppositeCategory c m o -> c
    opOp (Op c) = c
    
    instance (FiniteCategory c m o, Morphism m o) => FiniteCategory (OppositeCategory c m o) (OppositeMorphism m o) o where
        ob (Op c) = ob c
        identity (Op c) o = OpMorph $ identity c o
        ar (Op c) s t = OpMorph <$> ar c t s
    
    instance (GeneratedFiniteCategory c m o, Morphism m o) => GeneratedFiniteCategory (OppositeCategory c m o) (OppositeMorphism m o) o where
        genAr (Op c) s t = OpMorph <$> genAr c t s
        decompose (Op c) (OpMorph m) = OpMorph <$> decompose c m
        
    instance (PrettyPrintable c) => PrettyPrintable (OppositeCategory c m o) where
        pprint (Op cat) = "Op "++(pprint cat)