{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- 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, adjHomDst
  , adjHomDisj

    -- * Map

  , adjMapCnt
  , coAdjunctionOp

    -- * Proposition

  , prpAdjunction, prpAdjunctionRight, prpAdjunctionLeft

  ) where

import OAlg.Prelude

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

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
_) = Adjunction h d c -> Struct Mlt c -> Point c -> d -> c
forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Struct Mlt c -> Point c -> d -> c
adjrStruct Adjunction h d c
adj (Struct (ObjectClass h) c -> Struct Mlt c
forall x. Struct (ObjectClass h) x -> Struct Mlt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (h d c -> Struct (ObjectClass h) c
forall x y. h x y -> Struct (ObjectClass h) y
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 = h d c -> d -> c
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h d c
r d
f c -> c -> c
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
_) = Adjunction h d c -> Struct Mlt d -> Point d -> c -> 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 (Struct (ObjectClass h) d -> Struct Mlt d
forall x. Struct (ObjectClass h) x -> Struct Mlt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (h c d -> Struct (ObjectClass h) d
forall x y. h x y -> Struct (ObjectClass h) y
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 d -> d -> d
forall c. Multiplicative c => c -> c -> c
* h c d -> c -> d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
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
_) = Homomorphous (ObjectClass h) d c -> Homomorphous Mlt d c
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (h d c -> Homomorphous (ObjectClass h) d c
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h d c
r)

--------------------------------------------------------------------------------

-- adjHomDst -


-- | attest of being 'Distributive' homomorphous.

adjHomDst :: HomDistributive h => Adjunction h d c -> Homomorphous Dst d c
adjHomDst :: forall (h :: * -> * -> *) d c.
HomDistributive h =>
Adjunction h d c -> Homomorphous Dst d c
adjHomDst (Adjunction h c d
_ h d c
r Point c -> c
_ Point d -> d
_) = Homomorphous (ObjectClass h) d c -> Homomorphous Dst d c
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (h d c -> Homomorphous (ObjectClass h) d c
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h d c
r)

--------------------------------------------------------------------------------

-- adjHomDisj -


-- | the induce adjunction.

adjHomDisj ::
  ( HomMultiplicative h
  , Transformable (ObjectClass h) s
  )
  => Adjunction h x y -> Adjunction (Variant2 Covariant (HomDisj s o h)) x y
adjHomDisj :: forall (h :: * -> * -> *) s x y (o :: * -> *).
(HomMultiplicative h, Transformable (ObjectClass h) s) =>
Adjunction h x y
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) x y
adjHomDisj (Adjunction h y x
l h x y
r Point y -> y
u Point x -> x
v) = Variant2 'Covariant (HomDisj s o h) y x
-> Variant2 'Covariant (HomDisj s o h) x y
-> (Point y -> y)
-> (Point x -> x)
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) x y
forall (h :: * -> * -> *) c d.
h c d
-> h d c -> (Point c -> c) -> (Point d -> d) -> Adjunction h d c
Adjunction (h y x -> Variant2 'Covariant (HomDisj s o h) y x
forall (h :: * -> * -> *) s x y (o :: * -> *).
(Morphism h, Transformable (ObjectClass h) s) =>
h x y -> Variant2 'Covariant (HomDisj s o h) x y
homDisj h y x
l) (h x y -> Variant2 'Covariant (HomDisj s o h) x y
forall (h :: * -> * -> *) s x y (o :: * -> *).
(Morphism h, Transformable (ObjectClass h) s) =>
h x y -> Variant2 'Covariant (HomDisj s o h) x y
homDisj h x y
r) Point y -> y
u Point x -> x
v

--------------------------------------------------------------------------------

-- adjMapCnt -


-- | contravariant mapping of 'Adjunction'.

adjMapCnt :: FunctorialOriented h
  => Variant2 Contravariant (Inv2 h) x x'
  -> Variant2 Contravariant (Inv2 h) y y'
  -> Adjunction (Variant2 Covariant h) x y -> Adjunction (Variant2 Covariant h) y' x'
adjMapCnt :: forall (h :: * -> * -> *) x x' y y'.
FunctorialOriented h =>
Variant2 'Contravariant (Inv2 h) x x'
-> Variant2 'Contravariant (Inv2 h) y y'
-> Adjunction (Variant2 'Covariant h) x y
-> Adjunction (Variant2 'Covariant h) y' x'
adjMapCnt (Contravariant2 (Inv2 h x x'
tx h x' x
fx)) (Contravariant2 (Inv2 h y y'
ty h y' y
fy))
  (Adjunction (Covariant2 h y x
l) (Covariant2 h x y
r) Point y -> y
u Point x -> x
v) = Variant2 'Covariant h x' y'
-> Variant2 'Covariant h y' x'
-> (Point x' -> x')
-> (Point y' -> y')
-> Adjunction (Variant2 'Covariant h) y' x'
forall (h :: * -> * -> *) c d.
h c d
-> h d c -> (Point c -> c) -> (Point d -> d) -> Adjunction h d c
Adjunction Variant2 'Covariant h x' y'
l' Variant2 'Covariant h y' x'
r' Point x' -> x'
u' Point y' -> y'
v' where

  l' :: Variant2 'Covariant h x' y'
l' = h x' y' -> Variant2 'Covariant h x' y'
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 (h y y'
ty h y y' -> h x' y -> h x' y'
forall y z x. h y z -> h x y -> h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. h x y
r h x y -> h x' x -> h x' y
forall y z x. h y z -> h x y -> h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. h x' x
fx) 
  r' :: Variant2 'Covariant h y' x'
r' = h y' x' -> Variant2 'Covariant h y' x'
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 (h x x'
tx h x x' -> h y' x -> h y' x'
forall y z x. h y z -> h x y -> h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. h y x
l h y x -> h y' y -> h y' x
forall y z x. h y z -> h x y -> h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. h y' y
fy)
  u' :: Point x' -> x'
u' = h x x' -> x -> x'
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf h x x'
tx (x -> x') -> (Point x' -> x) -> Point x' -> x'
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Point x -> x
v (Point x -> x) -> (Point x' -> Point x) -> Point x' -> x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. h x' x -> Point x' -> Point x
forall (h :: * -> * -> *) x y.
FunctorialPoint h =>
h x y -> Point x -> Point y
pmapf h x' x
fx
  v' :: Point y' -> y'
v' = h y y' -> y -> y'
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf h y y'
ty (y -> y') -> (Point y' -> y) -> Point y' -> y'
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Point y -> y
u (Point y -> y) -> (Point y' -> Point y) -> Point y' -> y
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. h y' y -> Point y' -> Point y
forall (h :: * -> * -> *) x y.
FunctorialPoint h =>
h x y -> Point x -> Point y
pmapf h y' y
fy

--------------------------------------------------------------------------------

-- coAdjunction -


coAdjunctionStruct ::
  ( HomMultiplicative h
  , Transformable (ObjectClass h) s
  , TransformableGRefl o s
  , DualisableMultiplicative s o
  )
  => Homomorphous s x y
  -> Adjunction h x y -> Adjunction (Variant2 Covariant (HomDisj s o h)) (o y) (o x)
coAdjunctionStruct :: forall (h :: * -> * -> *) s (o :: * -> *) x y.
(HomMultiplicative h, Transformable (ObjectClass h) s,
 TransformableGRefl o s, DualisableMultiplicative s o) =>
Homomorphous s x y
-> Adjunction h x y
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) (o y) (o x)
coAdjunctionStruct (Struct s x
sx:>:Struct s y
sy) Adjunction h x y
adj = Variant2 'Contravariant (Inv2 (HomDisj s o h)) x (o x)
-> Variant2 'Contravariant (Inv2 (HomDisj s o h)) y (o y)
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) x y
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) (o y) (o x)
forall (h :: * -> * -> *) x x' y y'.
FunctorialOriented h =>
Variant2 'Contravariant (Inv2 h) x x'
-> Variant2 'Contravariant (Inv2 h) y y'
-> Adjunction (Variant2 'Covariant h) x y
-> Adjunction (Variant2 'Covariant h) y' x'
adjMapCnt (Struct s x
-> Variant2 'Contravariant (Inv2 (HomDisj s o h)) x (o x)
forall (h :: * -> * -> *) (o :: * -> *) s x.
(Morphism h, TransformableGRefl o s) =>
Struct s x -> Variant2 'Contravariant (IsoHomDisj s o h) x (o x)
isoHomDisj Struct s x
sx) (Struct s y
-> Variant2 'Contravariant (Inv2 (HomDisj s o h)) y (o y)
forall (h :: * -> * -> *) (o :: * -> *) s x.
(Morphism h, TransformableGRefl o s) =>
Struct s x -> Variant2 'Contravariant (IsoHomDisj s o h) x (o x)
isoHomDisj Struct s y
sy) (Adjunction h x y
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) x y
forall (h :: * -> * -> *) s x y (o :: * -> *).
(HomMultiplicative h, Transformable (ObjectClass h) s) =>
Adjunction h x y
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) x y
adjHomDisj Adjunction h x y
adj)

-- | the co-'Adjunction' according to 'Op'.

coAdjunctionOp :: HomMultiplicative h
  => Adjunction h x y -> Adjunction (Variant2 Covariant (HomDisj Mlt Op h)) (Op y) (Op x)
coAdjunctionOp :: forall (h :: * -> * -> *) x y.
HomMultiplicative h =>
Adjunction h x y
-> Adjunction
     (Variant2 'Covariant (HomDisj Mlt Op h)) (Op y) (Op x)
coAdjunctionOp Adjunction h x y
a = Homomorphous Mlt x y
-> Adjunction h x y
-> Adjunction
     (Variant2 'Covariant (HomDisj Mlt Op h)) (Op y) (Op x)
forall (h :: * -> * -> *) s (o :: * -> *) x y.
(HomMultiplicative h, Transformable (ObjectClass h) s,
 TransformableGRefl o s, DualisableMultiplicative s o) =>
Homomorphous s x y
-> Adjunction h x y
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) (o y) (o x)
coAdjunctionStruct (Adjunction h x y -> Homomorphous Mlt x y
forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Homomorphous Mlt d c
adjHomMlt Adjunction h x y
a) Adjunction h x y
a 


--------------------------------------------------------------------------------

-- relAdjunctionRightUnit -


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

--------------------------------------------------------------------------------

-- relAdjunctionRightNatural -


relAdjunctionRightNaturalHom :: (Hom Mlt h, Show2 h)
  => Homomorphous Mlt d c -> Adjunction h d c -> c -> Statement
relAdjunctionRightNaturalHom :: forall (h :: * -> * -> *) d c.
(Hom Mlt h, Show2 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 (c -> Point c
forall q. Oriented q => q -> Point q
end c
f) c -> c -> c
forall c. Multiplicative c => c -> c -> c
* c
f c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== h d c -> d -> c
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h d c
r (h c d -> c -> d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h c d
l c
f) c -> c -> c
forall c. Multiplicative c => c -> c -> c
* Point c -> c
u (c -> Point c
forall q. Oriented q => q -> Point q
start c
f))
      Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=c -> String
forall a. Show a => a -> String
show c
f,String
"l"String -> String -> Parameter
:=h c d -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h c d
l,String
"r"String -> String -> Parameter
:=h d c -> String
forall a b. h a b -> String
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, Show2 h) => Adjunction h d c -> Point c -> c -> Statement
prpAdjunctionRight :: forall (h :: * -> * -> *) d c.
(Hom Mlt h, Show2 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 [ Homomorphous Mlt d c -> Adjunction h d c -> Point c -> Statement
forall (h :: * -> * -> *) d c.
(Hom Mlt h, Show2 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
      , Homomorphous Mlt d c -> Adjunction h d c -> c -> Statement
forall (h :: * -> * -> *) d c.
(Hom Mlt h, Show2 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 = Homomorphous (ObjectClass h) d c -> Homomorphous Mlt d c
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (h d c -> Homomorphous (ObjectClass h) d c
forall x y. h x y -> Homomorphous (ObjectClass h) x y
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, Show2 h) => Adjunction h d c -> Point d -> d -> Statement
prpAdjunctionLeft :: forall (h :: * -> * -> *) d c.
(Hom Mlt h, Show2 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
:<=>:
  Adjunction (Variant2 'Covariant (HomDisj Mlt Op h)) (Op c) (Op d)
-> Point (Op d) -> Op d -> Statement
forall (h :: * -> * -> *) d c.
(Hom Mlt h, Show2 h) =>
Adjunction h d c -> Point c -> c -> Statement
prpAdjunctionRight (Adjunction h d c
-> Adjunction
     (Variant2 'Covariant (HomDisj Mlt Op h)) (Op c) (Op d)
forall (h :: * -> * -> *) x y.
HomMultiplicative h =>
Adjunction h x y
-> Adjunction
     (Variant2 'Covariant (HomDisj Mlt Op h)) (Op y) (Op x)
coAdjunctionOp Adjunction h d c
adj) Point d
Point (Op d)
y (d -> Op d
forall x. x -> Op x
Op d
g)

--------------------------------------------------------------------------------

-- prpAjunction -


-- | validity of an adjunction according to the properties of 'Adjunction'.

prpAdjunction
  :: (Hom Mlt h, Entity2 h)
  => Adjunction h d c
  -> X (Point d) -> X d
  -> X (Point c) -> X c
  -> Statement
prpAdjunction :: forall (h :: * -> * -> *) d c.
(Hom Mlt h, Entity2 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 [ h c d -> Statement
forall x y. h x y -> Statement
forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 h c d
l
      , h d c -> Statement
forall x y. h x y -> Statement
forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 h d c
r
      , X (Point c, c) -> ((Point c, c) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (X (Point c) -> X c -> X (Point c, c)
forall a b. X a -> X b -> X (a, b)
xTupple2 X (Point c)
xpc X c
xc) ((Point c -> c -> Statement) -> (Point c, c) -> Statement
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Adjunction h d c -> Point c -> c -> Statement
forall (h :: * -> * -> *) d c.
(Hom Mlt h, Show2 h) =>
Adjunction h d c -> Point c -> c -> Statement
prpAdjunctionRight Adjunction h d c
adj))
      , X (Point d, d) -> ((Point d, d) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (X (Point d) -> X d -> X (Point d, d)
forall a b. X a -> X b -> X (a, b)
xTupple2 X (Point d)
xpd X d
xd) ((Point d -> d -> Statement) -> (Point d, d) -> Statement
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Adjunction h d c -> Point d -> d -> Statement
forall (h :: * -> * -> *) d c.
(Hom Mlt h, Show2 h) =>
Adjunction h d c -> Point d -> d -> Statement
prpAdjunctionLeft Adjunction h d c
adj))
      ]

--------------------------------------------------------------------------------

-- Adjunction - Validable -


instance ( HomMultiplicative h, Entity2 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
:<=>:
    Adjunction h d c
-> X (Point d) -> X d -> X (Point c) -> X c -> Statement
forall (h :: * -> * -> *) d c.
(Hom Mlt h, Entity2 h) =>
Adjunction h d c
-> X (Point d) -> X d -> X (Point c) -> X c -> Statement
prpAdjunction Adjunction h d c
adj X (Point d)
forall x. XStandard x => X x
xStandard X d
forall x. XStandard x => X x
xStandard X (Point c)
forall x. XStandard x => X x
xStandard X c
forall x. XStandard x => X x
xStandard