{-# 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 ++ ")"