{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}

-- |
-- Module      : OAlg.Adjunction.Definition
-- Description : definition of adjunctions between multiplicative structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- definition of adjunctions between 'Multiplicative' structures. We relay on the terms and notation as
-- used in [nLab](http://ncatlab.org/nlab/show/adjoint+functor)
module OAlg.Adjunction.Definition
  (
    -- * Adjunction
    Adjunction(..), unitr, unitl, adjl, adjr, adjHomMlt

    -- * Dual
  , coAdjunction

    -- * Proposition
  , prpAdjunction, prpAdjunctionRight, prpAdjunctionLeft
  ) where

import OAlg.Prelude

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative

import OAlg.Hom

--------------------------------------------------------------------------------
-- Adjunction -

-- | adjunction between two multiplicative structures @__d__@ and @__c__@ according
--   two given multiplicative homomorphisms @l :: __h__ __c__ __d__@ and
--   @r :: __h__ __d__ __c__@.  
--
-- @
--              l
--          <------- 
--        d          c
--          -------->
--              r
-- @
--
--  __Property__ Let @'Adjunction' l r u v@ be in @'Adjunction' __h__ __d__ __c__@ where
--  @__h__@ is a 'Mlt'-homomorphism,
--  then holds:
--
--  (1) Naturality of the right unit @u@:
--
--      (1) For all @x@ in @'Point' __c__@ holds:
--      @'orientation' (u x) '==' x ':>' 'pmap' r ('pmap' l x)@.
--
--      (2) For all @f@ in @__c__@ holds:
--      @u ('end' f) '*' f '==' 'amap' r ('amap' l) f '*' u ('start' f)@.
--
--  (2) Naturality of the left unit @v@:
--
--      (1) For all @y@ in @'Point' __d__@ holds:
--      @'orientation' (v y) '==' 'pmap' l ('pmap' r y) ':>' y@.
--
--      (2) For all @g@ in @__d__@ holds:
--      @g '*' v ('start' g) '==' v ('end' g) '*' 'amap' l ('amap' r) g@.
--
--  (3) Triangle identities:
--
--      (1) For all @x@ in @'Point' __c__@ holds:
--      @'one' ('pmap' l x) == v ('pmap' l x) '*' 'amap' l (u x)@. 
--
--      (2) For all @y@ in @'Point' __d__@ holds:
--      @'one' ('pmap' r y) == 'amap' r (v y) '*' u ('pmap' r y)@.
--
--  The following diagrams illustrate the above equations
--
--  naturality of the right unit @u@ (Equations 1.1 and 1.2):
--
-- @
--         u a
--     a -------> pmap r (pmap l a)         
--     |                |
--   f |                | amap r (amap l f)
--     v                v
--     b -------> pmap r (pmap l b)
--         u b
--
-- @
--
--  naturality of the left unit @v@ (Equations 2.1 and 2.2):
--
-- @
--         v a
--    a <------- pmap l (pmap r a)
--    |                |
--  g |                | amap l (ampa r g)
--    v                v
--    b <------ pmap l (pmap r b)
--         v b
-- @
--
--  the left adjoint of the right unit @u@ is 'one' (Equation 3.1, see 'adjl'):
--
-- @
--                                  pmap l x         x
--                                 /   |             |
--                                /    |             |
--                               /     |             |
--                 amap l (u x) /      | one  ~  u x |    
--                             /       |             |
--                            /        |             |
--                           v         v             v
--  pmap l (pmap r (pmap l x)) ---> pmap l x    pmap r (pmap l x)
--                         v (pmap l x)
-- @
--
-- the right adjoint of the left unit @v@ is 'one' (Equation 3.2, see 'adjr'):
--
-- @
--                             u (pmap r y)
--  pmap l (pmap r y)     pmap r y ---> pmap r (pmap l (pmap r y))
--        |                  |         /
--        |                  |        /
--        | v y    ~     one |       / amap r (v y)
--        |                  |      /
--        |                  |     /
--        v                  v    v
--        y               pmap r y
-- @
data Adjunction h d c where
  Adjunction
    :: h c d -- ^ the homomorphism from right to left.
    -> h d c -- ^ the homomorphism from left to right.
    -> (Point c -> c) -- ^ the unit on the right side.
    -> (Point d -> d) -- ^ the unit on the left side.
    -> Adjunction h d c

--------------------------------------------------------------------------------
-- unitr -

-- | the unit on the right side.
unitr :: Adjunction h d c -> Point c -> c
unitr :: forall (h :: * -> * -> *) d c. Adjunction h d c -> Point c -> c
unitr (Adjunction h c d
_ h d c
_ Point c -> c
u Point d -> d
_) = Point c -> c
u

--------------------------------------------------------------------------------
-- unitl -

-- | the unit on the left side.
unitl :: Adjunction h d c -> Point d -> d
unitl :: forall (h :: * -> * -> *) d c. Adjunction h d c -> Point d -> d
unitl (Adjunction h c d
_ h d c
_ Point c -> c
_ Point d -> d
v) = Point d -> d
v

--------------------------------------------------------------------------------
-- adjr -

-- | the right adjoint @g'@ of a factor in @g@ in @__d__@
--
--  __Property__ Let @x@ be in @__c__@ and @g@ in @__d__@ with @'start' g '==' 'pmap' l x@
--  then the right adjoint @g'@ of @g@ is given by @g' = 'amap' r g '*' u x@.
--
--
-- @
--                             u x
--       pmap l x           x -----> pmap r (pmap l x)
--          |               |       /
--          |               |      /
--          |               |     /
--          | g     ~    g' |    / amap r g
--          |               |   /
--          |               |  /
--          v               v v
--          y            pmap r y
-- @
adjr :: Hom Mlt h => Adjunction h d c -> Point c -> d -> c
adjr :: forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point c -> d -> c
adjr adj :: Adjunction h d c
adj@(Adjunction h c d
_ h d c
r Point c -> c
_ Point d -> d
_) = forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Struct Mlt c -> Point c -> d -> c
adjrStruct Adjunction h d c
adj (forall s t x. Transformable s t => Struct s x -> Struct t x
tau (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h d c
r)) where
  adjrStruct :: Hom Mlt h
    => Adjunction h d c -> Struct Mlt c -> Point c -> d -> c
  adjrStruct :: forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Struct Mlt c -> Point c -> d -> c
adjrStruct (Adjunction h c d
_ h d c
r Point c -> c
u Point d -> d
_) Struct Mlt c
Struct Point c
x d
f = forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h d c
r d
f forall c. Multiplicative c => c -> c -> c
* Point c -> c
u Point c
x


-- | the left adjoint @f'@ of a factor @f@ in @__c__@.
--
-- __Property__ Let @y@ be in @__d__@ and @f@ in @__c__@ with @'end' f '==' 'pmap' r y@
-- then the left adjoint @f'@ of @f@ is given by @f' = v y '*' 'amap' l f@.
--
--
-- @
--                      pmap l x           x
--                       /   |             |
--                      /    |             |
--                     /     |             |
--           amap l f /      | f'   ~    f |
--                   /       |             |
--                  /        |             |
--                 v         v             v
--  pmap l (pmap r y) -----> y          pmap r y
--                      v y
-- @
adjl :: Hom Mlt h => Adjunction h d c -> Point d -> c -> d
adjl :: forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point d -> c -> d
adjl adj :: Adjunction h d c
adj@(Adjunction h c d
l h d c
_ Point c -> c
_ Point d -> d
_) = forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Struct Mlt d -> Point d -> c -> d
adjlStruct Adjunction h d c
adj (forall s t x. Transformable s t => Struct s x -> Struct t x
tau (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h c d
l)) where
  adjlStruct :: Hom Mlt h
    => Adjunction h d c -> Struct Mlt d -> Point d -> c -> d
  adjlStruct :: forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Struct Mlt d -> Point d -> c -> d
adjlStruct (Adjunction h c d
l h d c
_ Point c -> c
_ Point d -> d
v) Struct Mlt d
Struct Point d
y c
f = Point d -> d
v Point d
y forall c. Multiplicative c => c -> c -> c
* forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h c d
l c
f

--------------------------------------------------------------------------------
-- adjHomMlt -

-- | attest of being 'Multiplicative' homomorphous.
adjHomMlt :: Hom Mlt h => Adjunction h d c -> Homomorphous Mlt d c
adjHomMlt :: forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Homomorphous Mlt d c
adjHomMlt (Adjunction h c d
_ h d c
r Point c -> c
_ Point d -> d
_) = forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h d c
r)

--------------------------------------------------------------------------------
-- Adjunction - Duality -

type instance Dual (Adjunction h d c) = Adjunction (OpHom h) (Op c) (Op d)


-- | the dual adjunction.
coAdjunction :: Hom Mlt h => Adjunction h d c -> Dual (Adjunction h d c)
coAdjunction :: forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Dual (Adjunction h d c)
coAdjunction (Adjunction h c d
l h d c
r Point c -> c
u Point d -> d
v)
  = forall (h :: * -> * -> *) c d.
h c d
-> h d c -> (Point c -> c) -> (Point d -> d) -> Adjunction h d c
Adjunction (forall (h :: * -> * -> *) x y.
Transformable1 Op (ObjectClass h) =>
h x y -> OpHom h (Op x) (Op y)
OpHom h d c
r) (forall (h :: * -> * -> *) x y.
Transformable1 Op (ObjectClass h) =>
h x y -> OpHom h (Op x) (Op y)
OpHom h c d
l) (forall x. (Point x -> x) -> Point (Op x) -> Op x
coUnit Point d -> d
v) (forall x. (Point x -> x) -> Point (Op x) -> Op x
coUnit Point c -> c
u) where

  coUnit :: (Point x -> x) -> Point (Op x) -> Op x
  coUnit :: forall x. (Point x -> x) -> Point (Op x) -> Op x
coUnit Point x -> x
u = forall x. x -> Op x
Op forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Point x -> x
u

--------------------------------------------------------------------------------
-- relAdjunctionRightUnit -

relAdjunctionRightUnitHom :: Hom Mlt h
  => Homomorphous Mlt d c -> Adjunction h d c -> Point c -> Statement
relAdjunctionRightUnitHom :: forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Homomorphous Mlt d c -> Adjunction h d c -> Point c -> Statement
relAdjunctionRightUnitHom (Struct Mlt d
Struct :>: Struct Mlt c
Struct) (Adjunction h c d
l h d c
r Point c -> c
u Point d -> d
v) Point c
x
  = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid (c
ux,d
vlx)
        , String -> Label
Label String
"1.1" Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation c
ux forall a. Eq a => a -> a -> Bool
== Point c
x forall p. p -> p -> Orientation p
:> forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h d c
r (forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h c d
l Point c
x))
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"x"String -> String -> Parameter
:=forall a. Show a => a -> String
show Point c
x,String
"u x"String -> String -> Parameter
:=forall a. Show a => a -> String
show c
ux,String
"l"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h c d
l,String
"r"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h d c
r]
        , String -> Label
Label String
"3.1" Label -> Statement -> Statement
:<=>: (forall c. Multiplicative c => Point c -> c
one Point d
lx forall a. Eq a => a -> a -> Bool
== d
vlx forall c. Multiplicative c => c -> c -> c
* forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h c d
l c
ux)
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"x"String -> String -> Parameter
:=forall a. Show a => a -> String
show Point c
x,String
"pmap l x"String -> String -> Parameter
:= forall a. Show a => a -> String
show Point d
lx,String
"l"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h c d
l,String
"r"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h d c
r]
        ]
  where ux :: c
ux  = Point c -> c
u Point c
x
        vlx :: d
vlx = Point d -> d
v Point d
lx
        lx :: Point d
lx  = forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h c d
l Point c
x

--------------------------------------------------------------------------------
-- relAdjunctionRightNatural -

relAdjunctionRightNaturalHom :: Hom Mlt h
  => Homomorphous Mlt d c -> Adjunction h d c -> c -> Statement
relAdjunctionRightNaturalHom :: forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Homomorphous Mlt d c -> Adjunction h d c -> c -> Statement
relAdjunctionRightNaturalHom (Struct Mlt d
Struct :>: Struct Mlt c
Struct) (Adjunction h c d
l h d c
r Point c -> c
u Point d -> d
_) c
f
  = String -> Label
Label String
"1.2" Label -> Statement -> Statement
:<=>: (Point c -> c
u (forall q. Oriented q => q -> Point q
end c
f) forall c. Multiplicative c => c -> c -> c
* c
f forall a. Eq a => a -> a -> Bool
== forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h d c
r (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h c d
l c
f) forall c. Multiplicative c => c -> c -> c
* Point c -> c
u (forall q. Oriented q => q -> Point q
start c
f))
      Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall a. Show a => a -> String
show c
f,String
"l"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h c d
l,String
"r"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h d c
r]


--------------------------------------------------------------------------------
-- prpAdjunctionRight -

-- | validity of the unit on the right side.
prpAdjunctionRight :: Hom Mlt h => Adjunction h d c -> Point c -> c -> Statement
prpAdjunctionRight :: forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point c -> c -> Statement
prpAdjunctionRight adj :: Adjunction h d c
adj@(Adjunction h c d
_ h d c
r Point c -> c
_ Point d -> d
_) Point c
x c
f = String -> Label
Prp String
"AdjunctionRight" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Homomorphous Mlt d c -> Adjunction h d c -> Point c -> Statement
relAdjunctionRightUnitHom Homomorphous Mlt d c
s Adjunction h d c
adj Point c
x
      , forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Homomorphous Mlt d c -> Adjunction h d c -> c -> Statement
relAdjunctionRightNaturalHom Homomorphous Mlt d c
s Adjunction h d c
adj c
f
      ]
  where s :: Homomorphous Mlt d c
s = forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h d c
r)

--------------------------------------------------------------------------------
-- prpAdjunctionLeft -

-- | validity of the unit on the left side.
prpAdjunctionLeft :: Hom Mlt h => Adjunction h d c -> Point d -> d -> Statement
prpAdjunctionLeft :: forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point d -> d -> Statement
prpAdjunctionLeft Adjunction h d c
adj Point d
y d
g = String -> Label
Prp String
"AdjucntionLeft" Label -> Statement -> Statement
:<=>:
  forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point c -> c -> Statement
prpAdjunctionRight (forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Dual (Adjunction h d c)
coAdjunction Adjunction h d c
adj) Point d
y (forall x. x -> Op x
Op d
g)

--------------------------------------------------------------------------------
-- prpAjunction -

-- | validity of an adjunction according to the properties of 'Adjunction'.
prpAdjunction
  :: Hom Mlt h
  => Adjunction h d c
  -> X (Point d) -> X d
  -> X (Point c) -> X c
  -> Statement
prpAdjunction :: forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c
-> X (Point d) -> X d -> X (Point c) -> X c -> Statement
prpAdjunction adj :: Adjunction h d c
adj@(Adjunction h c d
l h d c
r Point c -> c
_ Point d -> d
_) X (Point d)
xpd X d
xd X (Point c)
xpc X c
xc = String -> Label
Prp String
"Adjunction" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 h c d
l
      , forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 h d c
r
      , forall x. X x -> (x -> Statement) -> Statement
Forall (forall a b. X a -> X b -> X (a, b)
xTupple2 X (Point c)
xpc X c
xc) (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point c -> c -> Statement
prpAdjunctionRight Adjunction h d c
adj))
      , forall x. X x -> (x -> Statement) -> Statement
Forall (forall a b. X a -> X b -> X (a, b)
xTupple2 X (Point d)
xpd X d
xd) (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point d -> d -> Statement
prpAdjunctionLeft Adjunction h d c
adj))
      ]

--------------------------------------------------------------------------------
-- Adjunction - Validable -

instance ( HomMultiplicative h
         , XStandardPoint d, XStandard d, XStandardPoint c, XStandard c
         )
  => Validable (Adjunction h d c) where
  valid :: Adjunction h d c -> Statement
valid Adjunction h d c
adj = String -> Label
Label String
"Mlt" Label -> Statement -> Statement
:<=>:
    forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c
-> X (Point d) -> X d -> X (Point c) -> X c -> Statement
prpAdjunction Adjunction h d c
adj forall x. XStandard x => X x
xStandard forall x. XStandard x => X x
xStandard forall x. XStandard x => X x
xStandard forall x. XStandard x => X x
xStandard