------------------------------------------------------------------------
-- The Agda standard library
--
-- The Maybe type
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Maybe where

open import Data.Empty using ()
open import Data.Unit.Base using ()
open import Data.Bool.Base using (T)
open import Data.Maybe.Relation.Unary.All using (All)
open import Data.Maybe.Relation.Unary.Any using (Any; just)
open import Level using (Level)

private
  variable
    a : Level
    A : Set a

------------------------------------------------------------------------
-- The base type and some operations

open import Data.Maybe.Base public

------------------------------------------------------------------------
-- Using Any and All to define Is-just and Is-nothing

Is-just : Maybe A  Set _
Is-just = Any  _  )

Is-nothing : Maybe A  Set _
Is-nothing = All  _  )

to-witness :  {m : Maybe A}  Is-just m  A
to-witness (just {x = p} _) = p

to-witness-T :  (m : Maybe A)  T (is-just m)  A
to-witness-T (just p) _  = p