\begin{code}
{-# OPTIONS --cubical --safe #-}

module Data.Maybe.Base where

open import Level
\end{code}
%<*maybe-def>
\begin{code}
data Maybe (A : Type a) : Type a where
  nothing  : Maybe A
  just     : A  Maybe A
\end{code}
%</maybe-def>
\begin{code}

maybe : {B : Maybe A  Type b}  B nothing  ((x : A)  B (just x))  (x : Maybe A)  B x
maybe b f nothing = b
maybe b f (just x) = f x
\end{code}