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

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

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

-- Is the value just something?

is-just : ∀ {a} {A : Set a} → Maybe A → Bool
is-just = maybe (const true) false

-- Is the value nothing?

is-nothing : ∀ {a} {A : Set a} → Maybe A → Bool
is-nothing = not ∘ is-just

-- Is-just x is a proposition that is inhabited iff x is
-- just something.

Is-just : ∀ {a} {A : Set a} → Maybe A → Set
Is-just = T ∘ is-just

-- Is-nothing x is a proposition that is inhabited iff x is nothing.

Is-nothing : ∀ {a} {A : Set a} → Maybe A → Set
Is-nothing = T ∘ is-nothing

-- Is-just and Is-nothing are mutually exclusive.

not-both-just-and-nothing :
∀ {a} {A : Set a} (x : Maybe A) →
Is-just x → Is-nothing x → ⊥₀
not-both-just-and-nothing (just _) _  ()
not-both-just-and-nothing nothing  () _

-- 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 :
∀ {d c} {M : Set d → Set c} ⦃ is-raw-monad : Raw-monad M ⦄ →

-- 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 >>=_) (apply-ext 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 >>=_) (apply-ext 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)                               ∎)

map just (return x)  ≡⟨ map-return just x ⟩∎
return (just x)      ∎)

map just (x >>= f)                                    ≡⟨ map->>= _ _ _ ⟩
x >>= map just ∘ f                                    ≡⟨ sym \$ >>=-map ext _ _ _ ⟩∎
map just x >>= maybe (map just ∘ f) (return nothing)  ∎)
```