{-# LANGUAGE TypeOperators, TypeFamilies, RankNTypes, NoImplicitPrelude #-}
module Data.Category.RepresentableFunctor where
import Data.Category
import Data.Category.Functor
data Representable f repObj = Representable
{ Representable f repObj -> f
representedFunctor :: f
, Representable f repObj -> Obj (Dom f) repObj
representingObject :: Obj (Dom f) repObj
, Representable f repObj
-> forall (k :: * -> * -> *) z.
(Dom f ~ k, Cod f ~ (->)) =>
Obj k z -> (f :% z) -> k repObj z
represent :: forall k z. (Dom f ~ k, Cod f ~ (->)) => Obj k z -> f :% z -> k repObj z
, Representable f repObj
-> forall (k :: * -> * -> *).
(Dom f ~ k, Cod f ~ (->)) =>
f :% repObj
universalElement :: forall k. (Dom f ~ k, Cod f ~ (->)) => f :% repObj
}
unrepresent :: (Functor f, Dom f ~ k, Cod f ~ (->)) => Representable f repObj -> k repObj z -> f :% z
unrepresent :: Representable f repObj -> k repObj z -> f :% z
unrepresent Representable f repObj
rep k repObj z
h = (Representable f repObj -> f
forall f repObj. Representable f repObj -> f
representedFunctor Representable f repObj
rep f -> Dom f repObj z -> Cod f (f :% repObj) (f :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% k repObj z
Dom f repObj z
h) (Representable f repObj
-> forall (k :: * -> * -> *).
(Dom f ~ k, Cod f ~ (->)) =>
f :% repObj
forall f repObj.
Representable f repObj
-> forall (k :: * -> * -> *).
(Dom f ~ k, Cod f ~ (->)) =>
f :% repObj
universalElement Representable f repObj
rep)
covariantHomRepr :: Category k => Obj k x -> Representable (x :*-: k) x
covariantHomRepr :: Obj k x -> Representable (x :*-: k) x
covariantHomRepr Obj k x
x = Representable :: forall f repObj.
f
-> Obj (Dom f) repObj
-> (forall (k :: * -> * -> *) z.
(Dom f ~ k, Cod f ~ (->)) =>
Obj k z -> (f :% z) -> k repObj z)
-> (forall (k :: * -> * -> *).
(Dom f ~ k, Cod f ~ (->)) =>
f :% repObj)
-> Representable f repObj
Representable
{ representedFunctor :: x :*-: k
representedFunctor = Obj k x -> x :*-: k
forall (k :: * -> * -> *) x. Category k => Obj k x -> x :*-: k
HomX_ Obj k x
x
, representingObject :: Obj (Dom (x :*-: k)) x
representingObject = Obj k x
Obj (Dom (x :*-: k)) x
x
, represent :: forall (k :: * -> * -> *) z.
(Dom (x :*-: k) ~ k, Cod (x :*-: k) ~ (->)) =>
Obj k z -> ((x :*-: k) :% z) -> k x z
represent = \Obj k z
_ (x :*-: k) :% z
h -> k x z
(x :*-: k) :% z
h
, universalElement :: forall (k :: * -> * -> *).
(Dom (x :*-: k) ~ k, Cod (x :*-: k) ~ (->)) =>
(x :*-: k) :% x
universalElement = Obj k x
forall (k :: * -> * -> *).
(Dom (x :*-: k) ~ k, Cod (x :*-: k) ~ (->)) =>
(x :*-: k) :% x
x
}
contravariantHomRepr :: Category k => Obj k x -> Representable (k :-*: x) x
contravariantHomRepr :: Obj k x -> Representable (k :-*: x) x
contravariantHomRepr Obj k x
x = Representable :: forall f repObj.
f
-> Obj (Dom f) repObj
-> (forall (k :: * -> * -> *) z.
(Dom f ~ k, Cod f ~ (->)) =>
Obj k z -> (f :% z) -> k repObj z)
-> (forall (k :: * -> * -> *).
(Dom f ~ k, Cod f ~ (->)) =>
f :% repObj)
-> Representable f repObj
Representable
{ representedFunctor :: k :-*: x
representedFunctor = Obj k x -> k :-*: x
forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X Obj k x
x
, representingObject :: Obj (Dom (k :-*: x)) x
representingObject = Obj k x -> Op k x x
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op Obj k x
x
, represent :: forall (k :: * -> * -> *) z.
(Dom (k :-*: x) ~ k, Cod (k :-*: x) ~ (->)) =>
Obj k z -> ((k :-*: x) :% z) -> k x z
represent = \Obj k z
_ (k :-*: x) :% z
h -> k z x -> Op k x z
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op k z x
(k :-*: x) :% z
h
, universalElement :: forall (k :: * -> * -> *).
(Dom (k :-*: x) ~ k, Cod (k :-*: x) ~ (->)) =>
(k :-*: x) :% x
universalElement = Obj k x
forall (k :: * -> * -> *).
(Dom (k :-*: x) ~ k, Cod (k :-*: x) ~ (->)) =>
(k :-*: x) :% x
x
}
type InitialUniversal x u a = Representable ((x :*-: Cod u) :.: u) a
initialUniversal :: Functor u
=> u
-> Obj (Dom u) a
-> Cod u x (u :% a)
-> (forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y)
-> InitialUniversal x u a
initialUniversal :: u
-> Obj (Dom u) a
-> Cod u x (u :% a)
-> (forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y)
-> InitialUniversal x u a
initialUniversal u
u Obj (Dom u) a
obj Cod u x (u :% a)
mor forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y
factorizer = Representable :: forall f repObj.
f
-> Obj (Dom f) repObj
-> (forall (k :: * -> * -> *) z.
(Dom f ~ k, Cod f ~ (->)) =>
Obj k z -> (f :% z) -> k repObj z)
-> (forall (k :: * -> * -> *).
(Dom f ~ k, Cod f ~ (->)) =>
f :% repObj)
-> Representable f repObj
Representable
{ representedFunctor :: (x :*-: Cod u) :.: u
representedFunctor = Obj (Cod u) x -> x :*-: Cod u
forall (k :: * -> * -> *) x. Category k => Obj k x -> x :*-: k
HomX_ (Cod u x (u :% a) -> Obj (Cod u) x
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Cod u x (u :% a)
mor) (x :*-: Cod u) -> u -> (x :*-: Cod u) :.: u
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: u
u
, representingObject :: Obj (Dom ((x :*-: Cod u) :.: u)) a
representingObject = Obj (Dom u) a
Obj (Dom ((x :*-: Cod u) :.: u)) a
obj
, represent :: forall (k :: * -> * -> *) z.
(Dom ((x :*-: Cod u) :.: u) ~ k,
Cod ((x :*-: Cod u) :.: u) ~ (->)) =>
Obj k z -> (((x :*-: Cod u) :.: u) :% z) -> k a z
represent = forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y
forall (k :: * -> * -> *) z.
(Dom ((x :*-: Cod u) :.: u) ~ k,
Cod ((x :*-: Cod u) :.: u) ~ (->)) =>
Obj k z -> (((x :*-: Cod u) :.: u) :% z) -> k a z
factorizer
, universalElement :: forall (k :: * -> * -> *).
(Dom ((x :*-: Cod u) :.: u) ~ k,
Cod ((x :*-: Cod u) :.: u) ~ (->)) =>
((x :*-: Cod u) :.: u) :% a
universalElement = Cod u x (u :% a)
forall (k :: * -> * -> *).
(Dom ((x :*-: Cod u) :.: u) ~ k,
Cod ((x :*-: Cod u) :.: u) ~ (->)) =>
((x :*-: Cod u) :.: u) :% a
mor
}
type TerminalUniversal x u a = Representable ((Cod u :-*: x) :.: Opposite u) a
terminalUniversal :: Functor u
=> u
-> Obj (Dom u) a
-> Cod u (u :% a) x
-> (forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a)
-> TerminalUniversal x u a
terminalUniversal :: u
-> Obj (Dom u) a
-> Cod u (u :% a) x
-> (forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a)
-> TerminalUniversal x u a
terminalUniversal u
u Obj (Dom u) a
obj Cod u (u :% a) x
mor forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a
factorizer = Representable :: forall f repObj.
f
-> Obj (Dom f) repObj
-> (forall (k :: * -> * -> *) z.
(Dom f ~ k, Cod f ~ (->)) =>
Obj k z -> (f :% z) -> k repObj z)
-> (forall (k :: * -> * -> *).
(Dom f ~ k, Cod f ~ (->)) =>
f :% repObj)
-> Representable f repObj
Representable
{ representedFunctor :: (Cod u :-*: x) :.: Opposite u
representedFunctor = Obj (Cod u) x -> Cod u :-*: x
forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X (Cod u (u :% a) x -> Obj (Cod u) x
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Cod u (u :% a) x
mor) (Cod u :-*: x) -> Opposite u -> (Cod u :-*: x) :.: Opposite u
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: u -> Opposite u
forall f. Functor f => f -> Opposite f
Opposite u
u
, representingObject :: Obj (Dom ((Cod u :-*: x) :.: Opposite u)) a
representingObject = Obj (Dom u) a -> Op (Dom u) a a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op Obj (Dom u) a
obj
, represent :: forall (k :: * -> * -> *) z.
(Dom ((Cod u :-*: x) :.: Opposite u) ~ k,
Cod ((Cod u :-*: x) :.: Opposite u) ~ (->)) =>
Obj k z -> (((Cod u :-*: x) :.: Opposite u) :% z) -> k a z
represent = \(Op y) ((Cod u :-*: x) :.: Opposite u) :% z
f -> Dom u z a -> Op (Dom u) a z
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (Obj (Dom u) z -> Cod u (u :% z) x -> Dom u z a
forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a
factorizer Obj (Dom u) z
y Cod u (u :% z) x
((Cod u :-*: x) :.: Opposite u) :% z
f)
, universalElement :: forall (k :: * -> * -> *).
(Dom ((Cod u :-*: x) :.: Opposite u) ~ k,
Cod ((Cod u :-*: x) :.: Opposite u) ~ (->)) =>
((Cod u :-*: x) :.: Opposite u) :% a
universalElement = Cod u (u :% a) x
forall (k :: * -> * -> *).
(Dom ((Cod u :-*: x) :.: Opposite u) ~ k,
Cod ((Cod u :-*: x) :.: Opposite u) ~ (->)) =>
((Cod u :-*: x) :.: Opposite u) :% a
mor
}