{-# OPTIONS --cubical-compatible --safe #-}
module Data.Maybe.Properties where
open import Algebra.Bundles using (Semigroup; Monoid)
import Algebra.Structures as Structures
import Algebra.Definitions as Definitions
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)
open import Relation.Nullary.Decidable using (map′)
private
variable
a b c : Level
A : Set a
B : Set b
C : Set c
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-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-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
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
}
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."
#-}