module JK-Monads where

open import Logic
open import LogicalFacts
open import Equality

-----------------------------------------------
--                                           --
-- The selection and continuation monads.    --
--                                           --
-----------------------------------------------

J : {R : Ω} → Ω → Ω
J {R} A = (A → R) → A

K : {R : Ω} → Ω → Ω
K {R} A = (A → R) → R


-- The monads we'll consider are, for a parameter R fixed in
-- advance, or passed around, 
--
--      T A = J R A,
-- and
--      T A = K R A.
--

-- This will be a monad morphism:

J-K :  {R A : Ω} →
---
       J {R} A → K A

J-K ε p = p(ε p)


-- Under a (necessary) hypothesis, the following goes in the direction
-- opposite to J-K, but is not a morphism.  (Preservation of the unit
-- fails.)


K-J :  {R A : Ω} →
---
       (R → A) →     -- efq (ex falso quodlibet)
       K A → J A

K-J efq φ = efq ∘ φ


-- Notational conventions: 
--
--   +-------------+---------------------+
--   |   proofs of |  are ranged over by |
--   +-------------+---------------------+
--   |     J R A   |    ε                |
--   |     K R A   |    φ                |
--   |     A→R     |    p                |
--   +-------------+---------------------+
--
-- For variables ranging over sequences,
-- we append the suffix "s".


J-functor : {R A B : Ω} →
---------
            (A → B) → J {R} A → J B

J-functor f ε = λ q → f(ε(q ∘ f))



K-functor : {R A B : Ω} →
---------
            (A → B) → K {R} A → K B

K-functor f φ = λ q → φ(q ∘ f)



------------
--        --
-- Units  --
--        --
------------


ηJ : {R A : Ω} →
--
     A → J {R} A

ηJ a = λ p → a


ηK : {R A : Ω} →
--
     A → K {R} A

ηK a = λ p → p a


-----------------------
--                   --
--  Multiplications  --
--                   --
-----------------------


μJ : {R A : Ω} →
-- 
     J(J A) → J A

μJ {R} E = λ p → E (λ ε → J-K {R} ε p) p


μK : {R A : Ω} →
-- 
     K(K A) → K {R} A

μK Φ = λ p → Φ (λ φ → φ p)


----------------------------------------------------------
--                                                      --
--                                                      --
-- Monad laws for J (for K they are well known to hold) --
--                                                      --
----------------------------------------------------------


-- The proofs of the laws are automatic. We just need to write the
-- equations we want to prove. Then agda normalizes each side and sees
-- that they are equal, and accepts our proof "reflexivity".


J-functoriality₀ : {R A : Ω} →
----------------
                   J-functor id ≡ id {J {R} A}

J-functoriality₀ = reflexivity


J-functoriality₁ : {R A B C : Ω} →
----------------
                   (f : (A → B)) → (g : (B → C)) →
                   J-functor {R} (g ∘ f) ≡ (J-functor g) ∘ (J-functor f)

J-functoriality₁ f g = reflexivity


J-η-naturality : {R A B : Ω} →
--------------
                 (f : (A → B)) → (ηJ {R}) ∘ f ≡ (J-functor f) ∘ ηJ

J-η-naturality f = reflexivity


J-μ-naturality : {R A B : Ω} →
--------------
   (f : (A → B)) →
   (μJ {R} {B}) ∘ (J-functor (J-functor f)) ≡ (J-functor f) ∘ (μJ {R})

J-μ-naturality f = reflexivity


J-assoc : {R A : Ω} →
-------
          (μJ {R} {A}) ∘ (J-functor μJ) ≡ μJ ∘ μJ

J-assoc = reflexivity


J-unit₀ : {R A : Ω} →
--------
           μJ ∘ (J-functor ηJ) ≡ id {J {R} A}

J-unit₀ = reflexivity


J-unit₁ : {R A : Ω} →
--------
           μJ ∘ ηJ ≡ id {J {R} A}

J-unit₁ = reflexivity


-- Digression. Verification that J-K is a monad morphism:


J-K-morphism₀ : {R A : Ω} →
-------------
                (J-K {R} {A}) ∘ ηJ ≡ ηK

J-K-morphism₀ = reflexivity


J-K-morphism₁ : {R A : Ω} →
-------------
                (J-K {R} {A}) ∘ μJ ≡ μK ∘ J-K ∘ (J-functor J-K)

J-K-morphism₁ = reflexivity


---------------------------
--                       --
-- Extension operators.  --
--                       --
---------------------------


J-extend : {R A B : Ω} →
--------
           (A → J B) → (J A → J B)

J-extend {R} f = μJ ∘ (J-functor {R} f)


observation-J-extend : {R A B : Ω} →
--------------------
               (f : (A → J {R} B)) → (ε : J A) → (q : (B → R)) →

               J-extend f ε q ≡ f(ε(λ a → q(f a q))) q

observation-J-extend f ε q = reflexivity


K-extend : {R A B : Ω} →
--------
           (A → K B) → (K A → K B)

K-extend {R} f = μK ∘ (K-functor {R} f)


observation-K-extend : {R A B : Ω} →
--------------------
               (f : (A → K B)) → (φ : K A) → (q : (B → R)) →
               K-extend f φ q ≡ φ(λ a → f a q)

observation-K-extend f φ q = reflexivity

-----------------
--             --
-- Strengths.  --
--             --
-----------------


-- Any lambda-defined monad in a cartesian closed category is
-- enriched over the category, and hence is strong. This is why the
-- following two strengths have the same definition, although,
-- concretely, they are given by different lambda definitions
-- (observation-J-strength and observation-K-strength):


J-strength : {R A₀ A₁ : Ω} →
----------
             A₀ ∧ J A₁ → J(A₀ ∧ A₁)

J-strength {R} (∧-intro a₀ ε₁) = J-functor {R} (λ a₁ → ∧-intro a₀ a₁) ε₁


observation-J-strength :  {R A₀ A₁ : Ω}
----------------------
  (a₀ : A₀) → (ε₁ : J {R} A₁) →

  J-strength (∧-intro a₀ ε₁) ≡ λ p → ∧-intro a₀ (ε₁(λ a₁ → p(∧-intro a₀ a₁)))

observation-J-strength a₀ ε₁ = reflexivity


K-strength : {R A₀ A₁ : Ω} →
----------
             A₀ ∧ K A₁ → K(A₀ ∧ A₁)

K-strength {R} (∧-intro a₀ φ₁) = K-functor {R} (λ a₁ → ∧-intro a₀ a₁) φ₁


observation-K-strength :  {R A₀ A₁ : Ω}
----------------------
  (a₀ : A₀) → (φ₁ : K {R} A₁) →

  K-strength (∧-intro a₀ φ₁) ≡ λ p → φ₁(λ a₁ → p(∧-intro a₀ a₁))

observation-K-strength a₀ φ₁ = reflexivity


-- The verification that this is indeed a strength
-- (see http://en.wikipedia.org/wiki/Strong_monad)
-- is not needed.