import Algebra.Applicative

public export
Applicative Optional where
  pure = Some
  Nothing <*> _ = Nothing
  _ <*> Nothing = Nothing
  (Some f) <*> (Some x) = Some $ f x
  proofIdentity Nothing  = Refl
  proofIdentity (Some x) = Refl
  proofComposition Nothing  Nothing  _ = Refl
  proofComposition Nothing  (Some g) _ = Refl
  proofComposition (Some f) Nothing  _ = Refl
  proofComposition (Some f) (Some g) Nothing  = Refl
  proofComposition (Some f) (Some g) (Some x) = Refl
  proofHomomorphism f x = Refl
  proofInterchange Nothing  x = Refl
  proofInterchange (Some f) x = Refl