module Data.Category.Pair where
import Prelude (($), undefined)
import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
data P1
data P2
data Pair :: * -> * -> * where
IdFst :: Pair P1 P1
IdSnd :: Pair P2 P2
instance Category Pair where
data Obj Pair a where
Fst :: Obj Pair P1
Snd :: Obj Pair P2
src IdFst = Fst
src IdSnd = Snd
tgt IdFst = Fst
tgt IdSnd = Snd
id Fst = IdFst
id Snd = IdSnd
IdFst . IdFst = IdFst
IdSnd . IdSnd = IdSnd
_ . _ = undefined
data PairDiagram :: (* -> * -> *) -> * -> * -> * where
PairDiagram :: Category (~>) => Obj (~>) x -> Obj (~>) y -> PairDiagram (~>) x y
type instance Dom (PairDiagram (~>) x y) = Pair
type instance Cod (PairDiagram (~>) x y) = (~>)
type instance PairDiagram (~>) x y :% P1 = x
type instance PairDiagram (~>) x y :% P2 = y
instance Functor (PairDiagram (~>) x y) where
PairDiagram x _ %% Fst = x
PairDiagram _ y %% Snd = y
PairDiagram x _ % IdFst = id x
PairDiagram _ y % IdSnd = id y
pairNat :: (Functor f, Functor g, Dom f ~ Pair, Cod f ~ d, Dom g ~ Pair, Cod g ~ d)
=> f -> g -> Com f g P1 -> Com f g P2 -> Nat Pair d f g
pairNat f g c1 c2 = Nat f g (\x -> unCom $ n c1 c2 x) where
n :: (Functor f, Functor g, Dom f ~ Pair, Cod f ~ d, Dom g ~ Pair, Cod g ~ d)
=> Com f g P1 -> Com f g P2 -> Obj Pair a -> Com f g a
n c _ Fst = c
n _ c Snd = c
arrowPair :: Category (~>) => (x1 ~> x2) -> (y1 ~> y2) -> Nat Pair (~>) (PairDiagram (~>) x1 y1) (PairDiagram (~>) x2 y2)
arrowPair l r = pairNat (PairDiagram (src l) (src r)) (PairDiagram (tgt l) (tgt r)) (Com l) (Com r)