optionalFoldBuildB.dhall

{ example0 =
    λ(a : Type) →
    λ(o : Optional a) →
    λ(optional : Type) →
    λ(some : a → optional) →
    λ(none : optional) →
      merge { Some = some, None = none } o
, example1 =
    λ(a : Type) →
    λ ( build
      : ∀(optional : Type) →
        ∀(some : a → optional) →
        ∀(none : optional) →
          optional
      ) →
      build (Optional a) (λ(x : a) → Some x) (None a)
, example2 = merge { Some = Natural/even, None = False } (Some 1)
}