{-# OPTIONS --safe #-}

module DepthComonads.Maybe where

open import Agda.Builtin.Maybe public
open import DepthComonads.Level

maybe : B → (A → B) → Maybe A → B
maybe b f nothing = b
maybe b f (just x) = f x
{-# INLINE maybe #-}