module Monads-Sets where

open import Level
open import Categories.Category.Instance.Sets
open import Categories.Category
open import Categories.Monad
open import Categories.Category.Cartesian
open import Categories.Category.CartesianClosed.Canonical
open import Categories.Category.BinaryProducts
open import Categories.Object.Exponential
open import Categories.Object.Product
open import Categories.Object.Terminal
open import Categories.Functor renaming (id to idF)
open import Categories.Category.Cocartesian
open import Categories.NaturalTransformation renaming (id to idN)
open import Data.Unit.Polymorphic
open import Data.Empty.Polymorphic
open import Data.Product
open import Data.Product.Properties using (×-≡,≡↔≡)
open import Data.Sum
open import Data.Sum.Properties
open import Function.Base renaming (_∘_ to _∘f_)
open import Axiom.Extensionality.Propositional
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)

module _ (o ℓ e : Level) (ext : Extensionality o o) where

    -- helpers
    ,-resp-≡ : ∀ {ℓ : Level} {A B : Set ℓ} {p₁@(a₁ , b₁) p₂@(a₂ , b₂) : A × B} → (a₁ ≡ a₂ × b₁ ≡ b₂) → p₁ ≡ p₂
    ,-resp-≡ (refl , refl) = refl
    inj₁-resp-≡ : ∀ {ℓ} {A B : Set ℓ} {c1 c2 : A} → (c1 ≡ c2) → (inj₁ {B = B} c1 ≡ inj₁ {B = B} c2)
    inj₁-resp-≡ refl = refl
    inj₂-resp-≡ : ∀ {ℓ} {A B : Set ℓ} {c1 c2 : B} → (c1 ≡ c2) → (inj₂ {A = A} c1 ≡ inj₂ {A = A} c2)
    inj₂-resp-≡ refl = refl

    --*
    -- Sets is cartesian(closed) and cocartesian
    --*

    SetsCartesian : Cartesian (Sets o)
    SetsCartesian = record
        { terminal = record
            { ⊤ = ⊤
            ; ⊤-is-terminal = record
                { ! = λ {A} _ → tt
                ; !-unique = λ f → refl
                }
            }
        ; products = record
            { product = λ {A} {B} → record
                { A×B = A × B
                ; π₁ = proj₁
                ; π₂ = proj₂
                ; ⟨_,_⟩ = <_,_>
                ; project₁ = refl
                ; project₂ = refl
                ; unique = λ p1 p2 → sym (,-resp-≡ (p1 , p2))
                }
            }
        }

    SetsCocartesian : Cocartesian (Sets o)
    SetsCocartesian = record
        { initial = record
            { ⊥ = ⊥
            ; ⊥-is-initial = record
                { ! = ⊥-elim
                ; !-unique = λ {A} f {x} → ⊥-elim {Whatever = λ y → ⊥-elim y ≡ f y} x
                }
            }
        ; coproducts = record
            { coproduct = λ {A} {B} → record
                { A+B = A ⊎ B
                ; i₁ = inj₁
                ; i₂ = inj₂
                ; [_,_] = [_,_]
                ; inject₁ = refl
                ; inject₂ = refl
                ; unique = λ p1 p2 → λ where
                    {inj₁ x} → sym $ p1 {x}
                    {inj₂ x} → sym $ p2 {x}
                }
            }
        }

    SetsCCC : CartesianClosed (Sets o)
    SetsCCC = record 
        { ⊤ = ⊤
        ; _×_ = _×_
        ; ! = !
        ; π₁           = π₁
        ; π₂           = π₂
        ; ⟨_,_⟩        = ⟨_,_⟩
        ; !-unique     = !-unique
        ; π₁-comp      = λ {_ _ f _ g} → project₁ {h = f} {g}
        ; π₂-comp      = λ {_ _ f _ g} → project₂ {h = f} {g}
        ; ⟨,⟩-unique   = λ {_ _ _ f g h} → unique {h = h} {f} {g}
        ; _^_          = λ X Y → Y → X
        ; eval         = λ {X Y} (f , y) → f y
        ; curry        = λ {C A B} f c a → f (c ,′ a)
        ; eval-comp    = λ {A} {B} {C} {f} {x} → refl
        ; curry-unique = λ {A} {B} {C} {f} {g} fg {x} → ext λ y → fg
        }
        where 
            open Category (Sets o)
            open Cartesian SetsCartesian
            open HomReasoning
            --open BinaryProducts products renaming (_×_ to _×'_; ⟨_,_⟩ to ⟨_,_⟩'; π₁ to π₁'; π₂ to π₂')
            open Terminal terminal using (!; !-unique)
            open BinaryProducts products using (π₁; π₂; ⟨_,_⟩; project₁; project₂; unique)

    --*
    -- ExceptionMonad TX = X + E
    --*

    ExceptionMonad : Set o → Monad (Sets o)
    ExceptionMonad E = record
        { F = F
        ; η = η'
        ; μ = μ'
        ; assoc = λ {X} → λ where
            {inj₁ x} → refl
            {inj₂ x} → refl
        ; sym-assoc = λ {X} → λ where
            {inj₁ x} → refl
            {inj₂ x} → refl
        ; identityˡ = λ {X} → λ where
            {inj₁ x} → refl
            {inj₂ x} → refl
        ; identityʳ = λ {X} → λ where
            {inj₁ x} → refl
            {inj₂ x} → refl
        }
        where
            open Cocartesian (SetsCocartesian) using (_+_; _+₁_)
            F = record
                { F₀ = λ X → X + E
                ; F₁ = λ f → f +₁ id
                ; identity = λ {A} → λ where
                    {inj₁ x} → refl
                    {inj₂ x} → refl
                ; homomorphism = λ {X} {Y} {Z} {f} {g} → λ where
                    {inj₁ x} → refl
                    {inj₂ x} → refl
                ; F-resp-≈ = λ {A} {B} {f} {g} f≈g → λ where
                    {inj₁ x} → inj₁-resp-≡ (f≈g {x})
                    {inj₂ x} → refl
                }
            η' = ntHelper record
                { η = λ X → inj₁
                ; commute = λ {X} {Y} f {x} → refl
                }
            μ' = ntHelper record
                { η = λ X → [ id , inj₂ ]
                ; commute = λ {X} {Y} f → λ where
                        {inj₁ x} → refl
                        {inj₂ x} → refl
                }

    MaybeMonad : Monad (Sets o)
    MaybeMonad = ExceptionMonad ⊤

    --*
    -- Reader Monad TX = X^S
    --*

    ReaderMonad : Set o → Monad (Sets o)
    ReaderMonad S = record
        { F = F
        ; η = η'
        ; μ = μ'
        ; assoc = refl
        ; sym-assoc = refl
        ; identityˡ = refl
        ; identityʳ = refl
        }
        where
            open Cocartesian (SetsCocartesian) using (_+_; _+₁_)
            open CartesianClosed SetsCCC
            F = record
                { F₀ = λ X → X ^ S
                ; F₁ = λ f g s → f (g s)
                ; identity = λ {A} {x} → refl
                ; homomorphism = λ {X Y Z f g x} → refl
                ; F-resp-≈ = λ {A B f g} fg {x} → ext λ y → fg {x y}
                }
            η' = ntHelper record
                { η = λ X → const
                ; commute = λ {X Y} f {x} → refl
                }
            μ' = ntHelper record
                { η = λ X x s → x s s
                ; commute = λ {X Y} f {x} → refl
                }