open import 1Lab.Prelude

open import Data.Maybe.Base
open import Data.List.Base using (_∷_; [])
open import Data.Dec.Base
open import Data.Nat.Base
open import Data.Sum.Base

module Data.Maybe.Properties where

private variable
  ℓ ℓ' : Level
  A B C : Type ℓ

Properties of Maybe🔗

Path space🔗

We can use these lemmas to characterise the path space of Maybe A in terms of the path space of A. This involves a standard encode-decode argument: for a more in-depth explanation, see Data.List.

module MaybePath {ℓ} {A : Type ℓ} where
  Code : Maybe A → Maybe A → Type _
  Code (just x) (just y) = x ≡ y
  Code (just x) nothing  = Lift _ ⊥
  Code nothing (just y)  = Lift _ ⊥
  Code nothing nothing   = Lift _ ⊤

The rest of this argument is standard, so we omit it.

  refl-code : ∀ x → Code x x
  refl-code (just x) = refl
  refl-code nothing = lift tt

  decode : ∀ x y → Code x y → x ≡ y
  decode (just x) (just y) p = ap just p
  decode nothing nothing _ = refl

  encode : ∀ x y → x ≡ y → Code x y
  encode (just x) (just y) p = just-inj p
  encode (just x) nothing p = absurd (just≠nothing p)
  encode nothing (just x) p = absurd (nothing≠just p)
  encode nothing nothing p = lift tt

  encode-refl : ∀ {x} → encode x x refl ≡ refl-code x
  encode-refl {x = just x} = refl
  encode-refl {x = nothing} = refl

  decode-refl : ∀ {x} → decode x x (refl-code x) ≡ refl
  decode-refl {x = just x} = refl
  decode-refl {x = nothing} = refl

  decode-encode : ∀ {x y} → (p : x ≡ y) → decode x y (encode x y p) ≡ p
  decode-encode {x = x} =
    J (λ y' p → decode x y' (encode x y' p) ≡ p)
      (ap (decode x x) encode-refl ∙ decode-refl)

  encode-decode : ∀ {x y} → (p : Code x y) → encode x y (decode x y p) ≡ p
  encode-decode {just x} {just y} p = refl
  encode-decode {nothing} {nothing} p = refl

  Path≃Code : ∀ x y → (x ≡ y) ≃ Code x y
  Path≃Code x y =
    Iso→Equiv (encode x y , iso (decode x y) encode-decode decode-encode)

  Code-is-hlevel
    : {x y : Maybe A} (n : Nat)
    → is-hlevel A (2 + n)
    → is-hlevel (Code x y) (1 + n)
  Code-is-hlevel {x = just x} {y = just y} n ahl = ahl x y
  Code-is-hlevel {x = just x} {y = nothing} n ahl = hlevel (1 + n)
  Code-is-hlevel {x = nothing} {y = just x} n ahl = hlevel (1 + n)
  Code-is-hlevel {x = nothing} {y = nothing} n ahl = hlevel (1 + n)

Now that we’ve characterised the path space, we can determine the h-level of Maybe.

Maybe-is-hlevel
  : (n : Nat)
  → is-hlevel A (2 + n)
  → is-hlevel (Maybe A) (2 + n)
Maybe-is-hlevel n ahl x y =
  Equiv→is-hlevel (1 + n) (MaybePath.Path≃Code x y) (MaybePath.Code-is-hlevel n ahl)

instance
  H-Level-Maybe
    : ∀ {ℓ} {A : Type ℓ} {n} ⦃ _ : 2 ≤ n ⦄ ⦃ _ : H-Level A n ⦄
    → H-Level (Maybe A) n
  H-Level-Maybe {n = suc (suc n)} = hlevel-instance $
    Maybe-is-hlevel n (hlevel (2 + n))

We also note that just is an embedding; this follows immediately from the characterisation of the path space.

just-cancellable : ∀ {x y : A} → (just x ≡ just y) ≃ (x ≡ y)
just-cancellable {x = x} {y = y} = MaybePath.Path≃Code (just x) (just y)

just-is-embedding : is-embedding (just {A = A})
just-is-embedding = cancellable→embedding just-cancellable

This lets us show that Maybe reflects h-levels.

Maybe-reflect-hlevel
  : (n : Nat)
  → is-hlevel (Maybe A) (2 + n)
  → is-hlevel A (2 + n)
Maybe-reflect-hlevel n mhl =
  embedding→is-hlevel {f = just} (1 + n) just-is-embedding mhl

Discreteness🔗

If Maybe A is discrete, then A must also be discrete. This follows from the fact that just is injective.

Maybe-reflect-discrete
  : Discrete (Maybe A)
  → Discrete A
Maybe-reflect-discrete eq? = Discrete-inj just just-inj eq?

Misc. properties🔗

If A is empty, then a Maybe A must be nothing.

refute-just : ¬ A → (x : Maybe A) → x ≡ nothing
refute-just ¬a (just a) = absurd (¬a a)
refute-just ¬a nothing = refl

As a corollary, if A is empty, then Maybe A is contractible.

empty→maybe-is-contr : ¬ A → is-contr (Maybe A)
empty→maybe-is-contr ¬a .centre = nothing
empty→maybe-is-contr ¬a .paths x = sym $ refute-just ¬a x

Next, note that map is functorial.

map-id : ∀ {ℓ} {A : Type ℓ} (x : Maybe A) → map id x ≡ x
map-id (just x) = refl
map-id nothing = refl

map-∘
  : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {f : B → C} {g : A → B}
  → (x : Maybe A)
  → map (f ∘ g) x ≡ map f (map g x)
map-∘ (just x) = refl
map-∘ nothing = refl

Furthermore, <|> is left and right unital, associative, and is preserved by map.

<|>-idl : ∀ {A : Type ℓ} → (x : Maybe A) → (nothing <|> x) ≡ x
<|>-idl x = refl

<|>-idr : ∀ {A : Type ℓ} → (x : Maybe A) → (x <|> nothing) ≡ x
<|>-idr (just x) = refl
<|>-idr nothing = refl

<|>-assoc
  : ∀ {A : Type ℓ}
  → (x y z : Maybe A)
  → (x <|> (y <|> z)) ≡ ((x <|> y) <|> z)
<|>-assoc (just x) y z = refl
<|>-assoc nothing y z = refl

map-<|>
  : ∀ {A : Type ℓ} {B : Type ℓ'} {f : A → B}
  → (x y : Maybe A)
  → map f (x <|> y) ≡ (map f x <|> map f y)
map-<|> (just x) y = refl
map-<|> nothing y = refl

Injectivity🔗

We can prove that the Maybe type constructor, considered as a function from a universe to itself, is injective.

maybe-injective : Maybe A ≃ Maybe B → A → B
maybe-injective e x with e .fst (just x) in p
... | just y = y
... | nothing with e .fst nothing in q
... | just y = y
... | nothing = absurd (just≠nothing (Equiv.injective₂ e (Id≃path.to p) (Id≃path.to q)))

Maybe-injective : Maybe A ≃ Maybe B → A ≃ B
Maybe-injective e = Iso→Equiv (a→b , iso b→a (lemma e) il) where
  a→b = maybe-injective e
  b→a = maybe-injective (Equiv.inverse e)

  module _ (e : Maybe A ≃ Maybe B) where abstract
    private
      module e = Equiv e
      module e⁻¹ = Equiv e.inverse

    lemma : is-right-inverse (maybe-injective (Equiv.inverse e)) (maybe-injective e)
    lemma x with e.from (just x) in p
    lemma x | just y with e.to (just y) in q
    lemma x | just y | just z  = just-inj (sym (Id≃path.to q) ∙ ap e.to (sym (Id≃path.to p)) ∙ e.ε _)
    lemma x | just y | nothing with e.to nothing in r
    lemma x | just y | nothing | nothing = absurd (just≠nothing (e.injective₂ (Id≃path.to q) (Id≃path.to r)))
    lemma x | just y | nothing | just z  = absurd (nothing≠just (sym (Id≃path.to q) ∙ ap e.to (sym (Id≃path.to p)) ∙ e.ε _))
    lemma x | nothing with e.from nothing in q
    lemma x | nothing | nothing = absurd (just≠nothing (e⁻¹.injective₂ (Id≃path.to p) (Id≃path.to q)))
    lemma x | nothing | just y with e.to (just y) in r
    lemma x | nothing | just y | just z = absurd (just≠nothing (sym (Id≃path.to r) ∙ ap e.to (sym (Id≃path.to q)) ∙ e.ε _))
    lemma x | nothing | just y | nothing with e.to nothing in s
    lemma x | nothing | just y | nothing | nothing = absurd (just≠nothing (e.injective₂ (Id≃path.to r) (Id≃path.to s)))
    lemma x | nothing | just y | nothing | just z = just-inj (sym (Id≃path.to s) ∙ ap e.to (sym (Id≃path.to p)) ∙ e.ε _)

  abstract
    il : is-left-inverse b→a a→b
    il = p' where
      p : is-right-inverse (maybe-injective (Equiv.inverse (Equiv.inverse e))) (maybe-injective (Equiv.inverse e))
      p = lemma (Equiv.inverse e)

      p' : is-right-inverse (maybe-injective e) (maybe-injective (Equiv.inverse e))
      p' = subst
        (λ e' → is-right-inverse (maybe-injective e') (maybe-injective (Equiv.inverse e)))
        {Equiv.inverse (Equiv.inverse e)} {e}
        (ext (λ _ → refl)) p

Maybe-is-sum : Maybe A ≃ (⊤ ⊎ A)
Maybe-is-sum {A = A} = Iso→Equiv (to , iso from ir il) where
  to   : Maybe A → ⊤ ⊎ A
  to (just x) = inr x
  to nothing = inl tt

  from : ⊤ ⊎ A → Maybe A
  from (inr x) = just x
  from (inl _) = nothing

  ir : is-right-inverse from to
  ir (inl x) = refl
  ir (inr x) = refl

  il : is-right-inverse to from
  il nothing = refl
  il (just x) = refl