{-
Unpack an `Optional`, returning the default when it's `None`.
-}
let default
    : ∀(a : Type) → a → Optional a → a
    = λ(a : Type) →
      λ(default : a) →
      λ(o : Optional a) →
        merge { Some = λ(x : a) → x, None = default } o

let example0 = assert : default Bool False (None Bool) ≡ False

let example1 = assert : default Bool False (Some True) ≡ True

in  default