```------------------------------------------------------------------------
-- Some definitions related to and properties of the Maybe type
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

open import Equality

module Maybe
{reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Prelude

open import Bijection eq using (_↔_)
open Derived-definitions-and-properties eq

-- A dependent eliminator.

maybe : ∀ {a b} {A : Set a} {B : Maybe A → Set b} →
((x : A) → B (just x)) → B nothing → (x : Maybe A) → B x
maybe j n (just x) = j x
maybe j n nothing  = n

-- A universe-polymorphic variant of bind.

infixl 5 _>>=′_

_>>=′_ : ∀ {a b} {A : Set a} {B : Set b} →
Maybe A → (A → Maybe B) → Maybe B
x >>=′ f = maybe f nothing x

instance

Monad.associativity  monad (just x) f g = refl (f x >>= g)

record MaybeT {d c} (M : Set d → Set c) (A : Set d) : Set c where
constructor wrap
field
run : M (Maybe A)

open MaybeT public

-- Failure.

fail : ∀ {d c} {M : Set d → Set c} ⦃ is-monad : Raw-monad M ⦄ {A} →
MaybeT M A
run fail = return nothing

-- MaybeT id is pointwise isomorphic to Maybe.

MaybeT-id↔Maybe : ∀ {a} {A : Set a} → MaybeT id A ↔ Maybe A
MaybeT-id↔Maybe = record
{ surjection = record
{ logical-equivalence = record { to = run; from = wrap }
; right-inverse-of    = refl
}
; left-inverse-of = refl
}

instance

-- MaybeT is a "raw monad" transformer.

∀ {d c} → Raw-monad-transformer (MaybeT {d = d} {c = c})

return (just x)

run x >>= maybe (run ∘ f) (return nothing)

map just m

transform-MaybeT :
∀ {d c} {M : Set d → Set c} ⦃ is-raw-monad : Raw-monad M ⦄ →
transform-MaybeT =

-- MaybeT is a monad transformer (assuming extensionality).

∀ {d c} →
Extensionality d c →
Monad-transformer (MaybeT {d = d} {c = c})

return (just x) >>= maybe (run ∘ f) (return nothing)  ≡⟨ left-identity (just x) (maybe (run ∘ f) (return nothing)) ⟩∎
run (f x)                                             ∎)

run x >>= maybe (return ∘ just) (return nothing)  ≡⟨ cong (run x >>=_) (ext (maybe (λ _ → refl _) (refl _))) ⟩
run x >>= return                                  ≡⟨ right-identity _ ⟩∎
run x                                             ∎)

run x >>=
(maybe (λ x → run (f x) >>= maybe (run ∘ g) (return nothing))
(return nothing))                                       ≡⟨ cong (run x >>=_) (ext (maybe (λ _ → refl _) (

return nothing                                                      ≡⟨ sym \$ left-identity _ _ ⟩∎
return nothing >>= maybe (run ∘ g) (return nothing)                 ∎))) ⟩

run x >>= (λ x → maybe (run ∘ f) (return nothing) x >>=
maybe (run ∘ g) (return nothing))               ≡⟨ associativity _ _ _ ⟩∎

(run x >>= maybe (run ∘ f) (return nothing)) >>=
maybe (run ∘ g) (return nothing)                               ∎)