{-# LANGUAGE TypeOperators, TypeFamilies, RankNTypes, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.RepresentableFunctor
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
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
-- | An initial universal property, a universal morphism from x to u.
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
-- | A terminal universal property, a universal morphism from u to x.
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
  }