module Data.Category.Functor (
Cat(..)
, CatW
, Dom
, Cod
, Functor(..)
, (:%)
, Id(..)
, (:.:)(..)
, Const(..), ConstF
, Opposite(..)
, OpOp(..)
, OpOpInv(..)
, EndoHask(..)
, Proj1(..)
, Proj2(..)
, (:***:)(..)
, DiagProd(..)
, Tuple1(..)
, Tuple2(..)
, Hom(..)
, (:*-:)
, homX_
, (:-*:)
, hom_X
) where
import Prelude hiding ((.), Functor)
import qualified Prelude
import Data.Category
import Data.Category.Product
infixr 9 %
infixr 9 :%
type family Dom ftag :: * -> * -> *
type family Cod ftag :: * -> * -> *
class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where
(%) :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
type family ftag :% a :: *
data Cat :: * -> * -> * where
CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (CatW (Dom ftag)) (CatW (Cod ftag))
data CatW :: (* -> * -> *) -> *
instance Category Cat where
src (CatA _) = CatA Id
tgt (CatA _) = CatA Id
CatA f1 . CatA f2 = CatA (f1 :.: f2)
data Id ((~>) :: * -> * -> *) = Id
type instance Dom (Id (~>)) = (~>)
type instance Cod (Id (~>)) = (~>)
type instance Id (~>) :% a = a
instance Category (~>) => Functor (Id (~>)) where
_ % f = f
data (g :.: h) where
(:.:) :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h
type instance Dom (g :.: h) = Dom h
type instance Cod (g :.: h) = Cod g
type instance (g :.: h) :% a = g :% (h :% a)
instance (Category (Cod g), Category (Dom h)) => Functor (g :.: h) where
(g :.: h) % f = g % (h % f)
data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where
Const :: Category c2 => Obj c2 x -> Const c1 c2 x
type instance Dom (Const c1 c2 x) = c1
type instance Cod (Const c1 c2 x) = c2
type instance Const c1 c2 x :% a = x
instance (Category c1, Category c2) => Functor (Const c1 c2 x) where
Const x % _ = x
type ConstF f = Const (Dom f) (Cod f)
data Opposite f where
Opposite :: Functor f => f -> Opposite f
type instance Dom (Opposite f) = Op (Dom f)
type instance Cod (Opposite f) = Op (Cod f)
type instance Opposite f :% a = f :% a
instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f) where
Opposite f % Op a = Op $ f % a
data OpOp ((~>) :: * -> * -> *) = OpOp
type instance Dom (OpOp (~>)) = Op (Op (~>))
type instance Cod (OpOp (~>)) = (~>)
type instance OpOp (~>) :% a = a
instance Category (~>) => Functor (OpOp (~>)) where
OpOp % Op (Op f) = f
data OpOpInv ((~>) :: * -> * -> *) = OpOpInv
type instance Dom (OpOpInv (~>)) = (~>)
type instance Cod (OpOpInv (~>)) = Op (Op (~>))
type instance OpOpInv (~>) :% a = a
instance Category (~>) => Functor (OpOpInv (~>)) where
OpOpInv % f = Op (Op f)
data EndoHask :: (* -> *) -> * where
EndoHask :: Prelude.Functor f => EndoHask f
type instance Dom (EndoHask f) = (->)
type instance Cod (EndoHask f) = (->)
type instance EndoHask f :% r = f r
instance Functor (EndoHask f) where
EndoHask % f = fmap f
data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1
type instance Dom (Proj1 c1 c2) = c1 :**: c2
type instance Cod (Proj1 c1 c2) = c1
type instance Proj1 c1 c2 :% (a1, a2) = a1
instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where
Proj1 % (f1 :**: _) = f1
data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj2
type instance Dom (Proj2 c1 c2) = c1 :**: c2
type instance Cod (Proj2 c1 c2) = c2
type instance Proj2 c1 c2 :% (a1, a2) = a2
instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where
Proj2 % (_ :**: f2) = f2
data f1 :***: f2 = f1 :***: f2
type instance Dom (f1 :***: f2) = Dom f1 :**: Dom f2
type instance Cod (f1 :***: f2) = Cod f1 :**: Cod f2
type instance (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)
instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where
(g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)
data DiagProd ((~>) :: * -> * -> *) = DiagProd
type instance Dom (DiagProd (~>)) = (~>)
type instance Cod (DiagProd (~>)) = (~>) :**: (~>)
type instance DiagProd (~>) :% a = (a, a)
instance Category (~>) => Functor (DiagProd (~>)) where
DiagProd % f = f :**: f
data Tuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple1 (Obj c1 a)
type instance Dom (Tuple1 c1 c2 a1) = c2
type instance Cod (Tuple1 c1 c2 a1) = c1 :**: c2
type instance Tuple1 c1 c2 a1 :% a2 = (a1, a2)
instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1) where
Tuple1 a % f = a :**: f
data Tuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple2 (Obj c2 a)
type instance Dom (Tuple2 c1 c2 a2) = c1
type instance Cod (Tuple2 c1 c2 a2) = c1 :**: c2
type instance Tuple2 c1 c2 a2 :% a1 = (a1, a2)
instance (Category c1, Category c2) => Functor (Tuple2 c1 c2 a2) where
Tuple2 a % f = f :**: a
data Hom ((~>) :: * -> * -> *) = Hom
type instance Dom (Hom (~>)) = Op (~>) :**: (~>)
type instance Cod (Hom (~>)) = (->)
type instance (Hom (~>)) :% (a1, a2) = a1 ~> a2
instance Category (~>) => Functor (Hom (~>)) where
Hom % (Op f1 :**: f2) = \g -> f2 . g . f1
type x :*-: (~>) = Hom (~>) :.: Tuple1 (Op (~>)) (~>) x
homX_ :: Category (~>) => Obj (~>) x -> x :*-: (~>)
homX_ x = Hom :.: Tuple1 (Op x)
type (~>) :-*: x = Hom (~>) :.: Tuple2 (Op (~>)) (~>) x
hom_X :: Category (~>) => Obj (~>) x -> (~>) :-*: x
hom_X x = Hom :.: Tuple2 x