module Data.Category (
CategoryO(..)
, CategoryA(..)
, Apply(..)
, Obj, obj
, F
, Dom
, Cod
, FunctorA(..)
, ContraFunctorA(..)
, Id(..)
, (:.:)(..)
, Const(..)
, (:*-:)(..)
, (:-*:)(..)
, Nat
, (:~>)
, Component
, InitialUniversal(..)
, TerminalUniversal(..)
, Adjunction(..)
) where
import Prelude hiding ((.), id, ($))
class CategoryO (~>) a where
id :: a ~> a
(!) :: Nat (~>) d f g -> Obj a -> Component f g a
class (CategoryO (~>) a, CategoryO (~>) b, CategoryO (~>) c) => CategoryA (~>) a b c where
(.) :: b ~> c -> a ~> b -> a ~> c
class (CategoryO (~>) a, CategoryO (~>) b) => Apply (~>) a b where
($$) :: a ~> b -> a -> b
type Obj a = a
obj :: Obj a
obj = undefined
type family F ftag a :: *
type family Dom ftag :: * -> * -> *
type family Cod ftag :: * -> * -> *
class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b)
=> FunctorA ftag a b where
(%) :: Obj ftag -> Dom ftag a b -> Cod ftag (F ftag a) (F ftag b)
class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b)
=> ContraFunctorA ftag a b where
(-%) :: Obj ftag -> Dom ftag a b -> Cod ftag (F ftag b) (F ftag a)
data Id ((~>) :: * -> * -> *) = Id
type instance F (Id (~>)) a = a
type instance Dom (Id (~>)) = (~>)
type instance Cod (Id (~>)) = (~>)
instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Id (~>)) a b where
_ % f = f
data (g :.: h) = g :.: h
type instance F (g :.: h) a = F g (F h a)
type instance Dom (g :.: h) = Dom h
type instance Cod (g :.: h) = Cod g
instance (FunctorA g (F h a) (F h b), FunctorA h a b, Cod h ~ Dom g) => FunctorA (g :.: h) a b where
_ % f = (obj :: g) % ((obj :: h) % f)
data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x = Const
type instance F (Const c1 c2 x) a = x
type instance Dom (Const c1 c2 x) = c1
type instance Cod (Const c1 c2 x) = c2
instance (CategoryO c1 a, CategoryO c1 b, CategoryO c2 x) => FunctorA (Const c1 c2 x) a b where
_ % _ = id
data (x :*-: ((~>) :: * -> * -> *)) = HomX_
type instance F (x :*-: (~>)) a = x ~> a
type instance Dom (x :*-: (~>)) = (~>)
type instance Cod (x :*-: (~>)) = (->)
instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) x a b) => FunctorA (x :*-: (~>)) a b where
_ % f = (f .)
data (((~>) :: * -> * -> *) :-*: x) = Hom_X
type instance F ((~>) :-*: x) a = a ~> x
type instance Dom ((~>) :-*: x) = (~>)
type instance Cod ((~>) :-*: x) = (->)
instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) a b x) => ContraFunctorA ((~>) :-*: x) a b where
_ -% f = (. f)
data family Nat (c :: * -> * -> *) (d :: * -> * -> *) (f :: *) (g :: *) :: *
type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g
type Component f g z = Cod f (F f z) (F g z)
type InitMorF x u = (x :*-: Cod u) :.: u
type TermMorF x u = (Cod u :-*: x) :.: u
data InitialUniversal x u a = InitialUniversal (F (InitMorF x u) a) (InitMorF x u :~> (a :*-: Dom u))
data TerminalUniversal x u a = TerminalUniversal (F (TermMorF x u) a) (TermMorF x u :~> (Dom u :-*: a))
data Adjunction f g = Adjunction
{ unit :: Id (Dom f) :~> (g :.: f)
, counit :: (f :.: g) :~> Id (Dom g)
}