module Data.Category.Functor (
Cat(..)
, CatW
, Dom
, Cod
, Functor(..)
, (:%)
, Id(..)
, (:.:)(..)
, Const(..), ConstF
, (:*-:)(..)
, (:-*:)(..)
, Opposite(..)
, EndoHask(..)
, InitialUniversal(..)
, TerminalUniversal(..)
) where
import Prelude hiding (id, (.), Functor)
import qualified Prelude
import Data.Category
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 (:*-:) :: * -> (* -> * -> *) -> * where
HomX_ :: Category (~>) => Obj (~>) x -> x :*-: (~>)
type instance Dom (x :*-: (~>)) = (~>)
type instance Cod (x :*-: (~>)) = (->)
type instance (x :*-: (~>)) :% a = x ~> a
instance Category (~>) => Functor (x :*-: (~>)) where
HomX_ _ % f = (f .)
data (:-*:) :: (* -> * -> *) -> * -> * where
Hom_X :: Category (~>) => Obj (~>) x -> (~>) :-*: x
type instance Dom ((~>) :-*: x) = Op (~>)
type instance Cod ((~>) :-*: x) = (->)
type instance ((~>) :-*: x) :% a = a ~> x
instance Category (~>) => Functor ((~>) :-*: x) where
Hom_X _ % Op f = (. 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 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 InitialUniversal x u a = InitialUniversal
{ iuObject :: Obj (Dom u) a
, initialMorphism :: Cod u x (u :% a)
, initialFactorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y }
data TerminalUniversal x u a = TerminalUniversal
{ tuObject :: Obj (Dom u) a
, terminalMorphism :: Cod u (u :% a) x
, terminalFactorizer :: forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a }