    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Maybe-related properties
    ------------------------------------------------------------------------

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

    module Data.Maybe.Properties where

    open import Algebra.Bundles using (Semigroup; Monoid)
    import Algebra.Structures as Structures using (IsMagma; IsSemigroup; IsMonoid)
    import Algebra.Definitions as Definitions
      using (Associative; LeftIdentity; RightIdentity; Identity; Idempotent)
    open import Data.Maybe.Base
      using (Maybe; just; nothing; map; _<∣>_; maybe; maybe′)
    open import Data.Maybe.Relation.Unary.All using (All; just; nothing)
    open import Data.Product.Base using (_,_)
    open import Function.Base using (_∋_; id; _∘_; _∘′_)
    open import Function.Definitions using (Injective)
    open import Level using (Level)
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; refl; cong; cong₂; _≗_)
    open import Relation.Binary.PropositionalEquality.Properties
      using (isEquivalence)
    open import Relation.Binary.Definitions using (DecidableEquality)
    open import Relation.Nullary.Decidable using (yes; no; map′)

    private
      variable
        a b c : Level
        A : Set a
        B : Set b
        C : Set c

    ------------------------------------------------------------------------
    -- Equality

    just-injective : ∀ {x y} → (Maybe A ∋ just x) ≡ just y → x ≡ y
    just-injective refl = refl

    ≡-dec : DecidableEquality A → DecidableEquality (Maybe A)
    ≡-dec _≟_ nothing  nothing  = yes refl
    ≡-dec _≟_ (just x) nothing  = no λ()
    ≡-dec _≟_ nothing  (just y) = no λ()
    ≡-dec _≟_ (just x) (just y) = map′ (cong just) just-injective (x ≟ y)

    ------------------------------------------------------------------------
    -- map

    map-id : map id ≗ id {A = Maybe A}
    map-id (just x) = refl
    map-id nothing  = refl

    map-id-local : ∀ {f : A → A} {mx} → All (λ x → f x ≡ x) mx → map f mx ≡ mx
    map-id-local (just eq) = cong just eq
    map-id-local nothing   = refl

    map-<∣> : ∀ (f : A → B) mx my →
      map f (mx <∣> my) ≡ map f mx <∣> map f my
    map-<∣> f (just x) my = refl
    map-<∣> f nothing  my = refl

    map-cong : {f g : A → B} → f ≗ g → map f ≗ map g
    map-cong f≗g (just x) = cong just (f≗g x)
    map-cong f≗g nothing  = refl

    map-cong-local : ∀ {f g : A → B} {mx} →
      All (λ x → f x ≡ g x) mx → map f mx ≡ map g mx
    map-cong-local (just eq) = cong just eq
    map-cong-local nothing   = refl

    map-injective : ∀ {f : A → B} → Injective _≡_ _≡_ f → Injective _≡_ _≡_ (map f)
    map-injective f-inj {nothing} {nothing} p = refl
    map-injective f-inj {just x} {just y} p = cong just (f-inj (just-injective p))

    map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
    map-∘ (just x) = refl
    map-∘ nothing  = refl

    map-nothing : ∀ {f : A → B} {ma} → ma ≡ nothing → map f ma ≡ nothing
    map-nothing refl = refl

    map-just : ∀ {f : A → B} {ma a} → ma ≡ just a → map f ma ≡ just (f a)
    map-just refl = refl

    ------------------------------------------------------------------------
    -- maybe

    maybe-map : ∀ {C : Maybe B → Set c}
                (j : (x : B) → C (just x)) (n : C nothing) (f : A → B) ma →
                maybe {B = C} j n (map f ma) ≡ maybe {B = C ∘ map f} (j ∘ f) n ma
    maybe-map j n f (just x) = refl
    maybe-map j n f nothing  = refl

    maybe′-map : ∀ j (n : C) (f : A → B) ma →
                 maybe′ j n (map f ma) ≡ maybe′ (j ∘′ f) n ma
    maybe′-map = maybe-map

    maybe′-∘ : ∀ {b} (f : B → C) (g : A → B) → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)
    maybe′-∘ _ _ = maybe (λ _ → refl) refl

    ------------------------------------------------------------------------
    -- _<∣>_

    module _ {A : Set a} where

      open Definitions {A = Maybe A} _≡_

      <∣>-assoc : Associative _<∣>_
      <∣>-assoc (just x) y z = refl
      <∣>-assoc nothing  y z = refl

      <∣>-identityˡ : LeftIdentity nothing _<∣>_
      <∣>-identityˡ (just x) = refl
      <∣>-identityˡ nothing  = refl

      <∣>-identityʳ : RightIdentity nothing _<∣>_
      <∣>-identityʳ (just x) = refl
      <∣>-identityʳ nothing  = refl

      <∣>-identity : Identity nothing _<∣>_
      <∣>-identity = <∣>-identityˡ , <∣>-identityʳ

      <∣>-idem : Idempotent _<∣>_
      <∣>-idem (just x) = refl
      <∣>-idem nothing = refl

    module _ (A : Set a) where

      open Structures {A = Maybe A} _≡_

      <∣>-isMagma : IsMagma _<∣>_
      <∣>-isMagma = record
        { isEquivalence = isEquivalence
        ; ∙-cong        = cong₂ _<∣>_
        }

      <∣>-isSemigroup : IsSemigroup _<∣>_
      <∣>-isSemigroup = record
        { isMagma = <∣>-isMagma
        ; assoc   = <∣>-assoc
        }

      <∣>-isMonoid : IsMonoid _<∣>_ nothing
      <∣>-isMonoid = record
        { isSemigroup = <∣>-isSemigroup
        ; identity    = <∣>-identity
        }

      <∣>-semigroup : Semigroup a a
      <∣>-semigroup = record
        { isSemigroup = <∣>-isSemigroup
        }

      <∣>-monoid : Monoid a a
      <∣>-monoid = record
        { isMonoid = <∣>-isMonoid
        }

    ------------------------------------------------------------------------
    -- DEPRECATED
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 2.0

    map-id₂ = map-id-local
    {-# WARNING_ON_USAGE map-id₂
    "Warning: map-id₂ was deprecated in v2.0.
    Please use map-id-local instead."
    #-}

    map-cong₂ = map-cong-local
    {-# WARNING_ON_USAGE map-id₂
    "Warning: map-cong₂ was deprecated in v2.0.
    Please use map-cong-local instead."
    #-}

    map-compose = map-∘
    {-# WARNING_ON_USAGE map-compose
    "Warning: map-compose was deprecated in v2.0.
    Please use map-∘ instead."
    #-}

    map-<∣>-commute = map-<∣>
    {-# WARNING_ON_USAGE map-<∣>-commute
    "Warning: map-<∣>-commute was deprecated in v2.0.
    Please use map-<∣> instead."
    #-}