{-# 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
import Data.Category.NaturalTransformation
import Data.Category.Adjunction


data Representable f repObj = Representable
  { forall f repObj. Representable f repObj -> f
representedFunctor :: f
  , forall f repObj. Representable f repObj -> Obj (Dom f) repObj
representingObject :: Obj (Dom f) repObj
  , forall 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
  , forall f repObj.
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 :: forall f (k :: * -> * -> *) repObj z.
(Functor f, Dom f ~ k, Cod f ~ (->)) =>
Representable f repObj -> k repObj z -> f :% z
unrepresent Representable f repObj
rep k repObj z
h = (forall f repObj. Representable f repObj -> f
representedFunctor Representable f repObj
rep forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% k repObj z
h) (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 :: forall (k :: * -> * -> *) x.
Category k =>
Obj k x -> Representable (x :*-: k) x
covariantHomRepr Obj k x
x = Representable
  { representedFunctor :: x :*-: k
representedFunctor = 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
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 -> (x :*-: k) :% z
h
  , universalElement :: forall (k :: * -> * -> *).
(Dom (x :*-: k) ~ k, Cod (x :*-: k) ~ (->)) =>
(x :*-: k) :% x
universalElement   = Obj k x
x
  }

contravariantHomRepr :: Category k => Obj k x -> Representable (k :-*: x) x
contravariantHomRepr :: forall (k :: * -> * -> *) x.
Category k =>
Obj k x -> Representable (k :-*: x) x
contravariantHomRepr Obj k x
x = Representable
  { representedFunctor :: k :-*: x
representedFunctor = forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X Obj k x
x
  , representingObject :: Obj (Dom (k :-*: x)) x
representingObject = 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 -> forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (k :-*: x) :% z
h
  , universalElement :: forall (k :: * -> * -> *).
(Dom (k :-*: x) ~ k, Cod (k :-*: x) ~ (->)) =>
(k :-*: x) :% x
universalElement   = Obj k x
x
  }

type InitialUniversal x u a = Representable (x :*%: 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 :: forall u a x.
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
u Obj (Dom u) a
ob Cod u x (u :% a)
mor forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y
factorizer = Representable
  { representedFunctor :: (x :*-: Cod u) :.: u
representedFunctor = forall f x. Functor f => Obj (Cod f) x -> f -> x :*%: f
HomXF (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Cod u x (u :% a)
mor) u
u
  , representingObject :: Obj (Dom ((x :*-: Cod u) :.: u)) a
representingObject = Obj (Dom u) a
ob
  , 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
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)
mor
  }

type TerminalUniversal x u a = Representable (u :%*: x) 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 :: forall u a x.
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
u Obj (Dom u) a
ob Cod u (u :% a) x
mor forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a
factorizer = Representable
  { representedFunctor :: (Cod u :-*: x)
:.: (Opp (Dom u) (Cod u)
     :.: Tuple1 (Op (Nat (Dom u) (Cod u))) (Op (Dom u)) u)
representedFunctor = forall f x. Functor f => f -> Obj (Cod f) x -> f :%*: x
HomFX u
u (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Cod u (u :% a) x
mor)
  , representingObject :: Obj
  (Dom
     ((Cod u :-*: x)
      :.: (Opp (Dom u) (Cod u)
           :.: Tuple1 (Op (Nat (Dom u) (Cod u))) (Op (Dom u)) u)))
  a
representingObject = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Obj (Dom u) a
ob
  , represent :: forall (k :: * -> * -> *) z.
(Dom
   ((Cod u :-*: x)
    :.: (Opp (Dom u) (Cod u)
         :.: Tuple1 (Op (Nat (Dom u) (Cod u))) (Op (Dom u)) u))
 ~ k,
 Cod
   ((Cod u :-*: x)
    :.: (Opp (Dom u) (Cod u)
         :.: Tuple1 (Op (Nat (Dom u) (Cod u))) (Op (Dom u)) u))
 ~ (->)) =>
Obj k z
-> (((Cod u :-*: x)
     :.: (Opp (Dom u) (Cod u)
          :.: Tuple1 (Op (Nat (Dom u) (Cod u))) (Op (Dom u)) u))
    :% z)
-> k a z
represent          = \(Op Dom u z z
y) ((Cod u :-*: x)
 :.: (Opp (Dom u) (Cod u)
      :.: Tuple1 (Op (Nat (Dom u) (Cod u))) (Op (Dom u)) u))
:% z
f -> forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a
factorizer Dom u z z
y ((Cod u :-*: x)
 :.: (Opp (Dom u) (Cod u)
      :.: Tuple1 (Op (Nat (Dom u) (Cod u))) (Op (Dom u)) u))
:% z
f)
  , universalElement :: forall (k :: * -> * -> *).
(Dom
   ((Cod u :-*: x)
    :.: (Opp (Dom u) (Cod u)
         :.: Tuple1 (Op (Nat (Dom u) (Cod u))) (Op (Dom u)) u))
 ~ k,
 Cod
   ((Cod u :-*: x)
    :.: (Opp (Dom u) (Cod u)
         :.: Tuple1 (Op (Nat (Dom u) (Cod u))) (Op (Dom u)) u))
 ~ (->)) =>
((Cod u :-*: x)
 :.: (Opp (Dom u) (Cod u)
      :.: Tuple1 (Op (Nat (Dom u) (Cod u))) (Op (Dom u)) u))
:% a
universalElement   = Cod u (u :% a) x
mor
  }


-- | For an adjunction F -| G, each pair (FY, unit_Y) is an initial morphism from Y to G.
adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)
adjunctionInitialProp :: forall (c :: * -> * -> *) (d :: * -> * -> *) f g y.
Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)
adjunctionInitialProp adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) Obj d y
y = forall u a x.
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 g
g (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj d y
y) (forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit Adjunction c d f g
adj forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj d y
y) (forall (c :: * -> * -> *) (d :: * -> * -> *) f g b a.
Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct Adjunction c d f g
adj)

-- | For an adjunction F -| G, each pair (GX, counit_X) is a terminal morphism from F to X.
adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)
adjunctionTerminalProp :: forall (c :: * -> * -> *) (d :: * -> * -> *) f g x.
Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)
adjunctionTerminalProp adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) Obj c x
x = forall u a x.
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 f
f (g
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c x
x) (forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat c c (f :.: g) (Id c)
adjunctionCounit Adjunction c d f g
adj forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj c x
x) (forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct Adjunction c d f g
adj)


initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
  => f -> g -> (forall y. InitialUniversal y g (f :% y)) -> Adjunction c d f g
initialPropAdjunction :: forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall y. InitialUniversal y g (f :% y))
-> Adjunction c d f g
initialPropAdjunction f
f g
g forall y. InitialUniversal y g (f :% y)
univ = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> d a (g :% (f :% a)))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunctionInit f
f g
g (\Obj d a
_ -> forall f repObj.
Representable f repObj
-> forall (k :: * -> * -> *).
   (Dom f ~ k, Cod f ~ (->)) =>
   f :% repObj
universalElement forall y. InitialUniversal y g (f :% y)
univ) (forall f repObj.
Representable f repObj
-> forall (k :: * -> * -> *) z.
   (Dom f ~ k, Cod f ~ (->)) =>
   Obj k z -> (f :% z) -> k repObj z
represent forall y. InitialUniversal y g (f :% y)
univ)

terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
  => f -> g -> (forall x. TerminalUniversal x f (g :% x)) -> Adjunction c d f g
terminalPropAdjunction :: forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall x. TerminalUniversal x f (g :% x))
-> Adjunction c d f g
terminalPropAdjunction f
f g
g forall x. TerminalUniversal x f (g :% x)
univ = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall b. Obj c b -> c (f :% (g :% b)) b)
-> Adjunction c d f g
mkAdjunctionTerm f
f g
g ((forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
Op k a b -> k b a
unOp forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
.) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f repObj.
Representable f repObj
-> forall (k :: * -> * -> *) z.
   (Dom f ~ k, Cod f ~ (->)) =>
   Obj k z -> (f :% z) -> k repObj z
represent forall x. TerminalUniversal x f (g :% x)
univ forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op) (\Obj c b
_ -> forall f repObj.
Representable f repObj
-> forall (k :: * -> * -> *).
   (Dom f ~ k, Cod f ~ (->)) =>
   f :% repObj
universalElement forall x. TerminalUniversal x f (g :% x)
univ)