module Data.Category.Adjunction (
Adjunction(..)
, mkAdjunction
, leftAdjunct
, rightAdjunct
, idAdj
, composeAdj
, AdjArrow(..)
, initialPropAdjunction
, terminalPropAdjunction
, adjunctionInitialProp
, adjunctionTerminalProp
, contAdj
) where
import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.RepresentableFunctor
data Adjunction c d f g = (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
=> Adjunction
{ leftAdjoint :: f
, rightAdjoint :: g
, unit :: Nat d d (Id d) (g :.: f)
, counit :: Nat c c (f :.: g) (Id c)
}
mkAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
=> f -> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunction f g un coun = Adjunction f g (Nat Id (g :.: f) un) (Nat (f :.: g) Id coun)
leftAdjunct :: Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct (Adjunction _ g un _) i h = (g % h) . (un ! i)
rightAdjunct :: Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct (Adjunction f _ _ coun) i h = (coun ! i) . (f % h)
adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)
adjunctionInitialProp adj@(Adjunction f g un _) y = initialUniversal g (f % y) (un ! y) (rightAdjunct adj)
adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)
adjunctionTerminalProp adj@(Adjunction f g _ coun) x = terminalUniversal f (g % x) (coun ! x) (leftAdjunct adj)
initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
=> f -> g -> (forall y. Obj d y -> InitialUniversal y g (f :% y)) -> Adjunction c d f g
initialPropAdjunction f g univ = mkAdjunction f g
(universalElement . univ)
(\a -> represent (univ (g % a)) a (g % a))
terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
=> f -> g -> (forall x. Obj c x -> TerminalUniversal x f (g :% x)) -> Adjunction c d f g
terminalPropAdjunction f g univ = mkAdjunction f g
(\a -> unOp (represent (univ (f % a)) (Op a) (f % a)))
(universalElement . univ)
idAdj :: Category k => Adjunction k k (Id k) (Id k)
idAdj = mkAdjunction Id Id (\x -> x) (\x -> x)
composeAdj :: Adjunction d e f g -> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g')
composeAdj (Adjunction f g u c) (Adjunction f' g' u' c') = Adjunction (f' :.: f) (g :.: g')
(compAssoc (g :.: g') f' f . Precompose f % (compAssocInv g g' f' . Postcompose g % u' . idPrecompInv g) . u)
(c' . Precompose g' % (idPrecomp f' . Postcompose f' % c . compAssoc f' f g) . compAssocInv (f' :.: f) g g')
data AdjArrow c d where
AdjArrow :: (Category c, Category d) => Adjunction c d f g -> AdjArrow (CatW c) (CatW d)
instance Category AdjArrow where
src (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj
tgt (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj
AdjArrow x . AdjArrow y = AdjArrow (composeAdj x y)
precomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e)
precomposeAdj (Adjunction f g un coun) = mkAdjunction
(Precompose g)
(Precompose f)
(\nh@(Nat h _ _) -> compAssocInv h g f . (nh `o` un) . idPrecompInv h)
(\nh@(Nat h _ _) -> idPrecomp h . (nh `o` coun) . compAssoc h f g)
postcomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat e c) (Nat e d) (Postcompose f e) (Postcompose g e)
postcomposeAdj (Adjunction f g un coun) = mkAdjunction
(Postcompose f)
(Postcompose g)
(\nh@(Nat h _ _) -> compAssoc g f h . (un `o` nh) . idPostcompInv h)
(\nh@(Nat h _ _) -> idPostcomp h . (coun `o` nh) . compAssocInv f g h)
contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r)
contAdj = mkAdjunction
(Opposite (hom_X (\x -> x)) :.: OpOpInv)
(hom_X (\x -> x))
(\_ x f -> f x)
(\_ -> Op (\x f -> f x))