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)} ⦃ s≀s (s≀s p) ⦄ = 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 = 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 inspect (e.from (just x))
    lemma x | just y , p with inspect (e.to (just y))
    lemma x | just y , p | just z  , q = just-inj (sym q βˆ™ ap e.to (sym p) βˆ™ e.Ξ΅ _)
    lemma x | just y , p | nothing , q with inspect (e.to nothing)
    lemma x | just y , p | nothing , q | nothing , r = absurd (just≠nothing (e.injective₂ q r))
    lemma x | just y , p | nothing , q | just z  , r = absurd (nothingβ‰ just (sym q βˆ™ ap e.to (sym p) βˆ™ e.Ξ΅ _))
    lemma x | nothing , p with inspect (e.from nothing)
    lemma x | nothing , p | nothing , q = absurd (justβ‰ nothing (e⁻¹.injectiveβ‚‚ p q))
    lemma x | nothing , p | just y , q with inspect (e.to (just y))
    lemma x | nothing , p | just y , q | just z  , r = absurd (justβ‰ nothing (sym r βˆ™ ap e.to (sym q) βˆ™ e.Ξ΅ _))
    lemma x | nothing , p | just y , q | nothing , r with inspect (e.to nothing)
    lemma x | nothing , p | just y , q | nothing , r | nothing , s = absurd (just≠nothing (e.injective₂ r s))
    lemma x | nothing , p | just y , q | nothing , r | just z , s = just-inj (sym s βˆ™ ap e.to (sym 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}
        trivial! 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