{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}
module Math.Categories.Opposite
(
OpMorphism(..),
opOpMorphism,
Op(..),
opOp,
)
where
import Math.Category
import Math.FiniteCategory
import Math.IO.PrettyPrint
import Data.WeakSet.Safe
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)
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
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)
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
")"