open import 1Lab.Prelude

open import Data.Fin.Finite
open import Data.Maybe.Base
open import Data.List.Base using (_∷_; [])
open import Data.Dec.Base
open import Data.Nat.Base
open import Data.Fin hiding (_≀_)

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?

FinitenessπŸ”—

If A is finite, then Maybe A is also finite.

Finite-Maybe
  : ⦃ fa : Finite A ⦄
  β†’ Finite (Maybe A)
Finite-Maybe ⦃ fa ⦄ .cardinality = suc (fa .cardinality)
Finite-Maybe {A = A} ⦃ fa ⦄ .enumeration =
  βˆ₯-βˆ₯-map (Isoβ†’Equiv ∘ maybe-iso) (fa .enumeration) where
    maybe-iso : A ≃ Fin (fa .cardinality) β†’ Iso (Maybe A) (Fin (suc (fa .cardinality)))
    maybe-iso f .fst (just x) = fsuc (Equiv.to f x)
    maybe-iso f .fst nothing = fzero
    maybe-iso f .snd .is-iso.inv fzero = nothing
    maybe-iso f .snd .is-iso.inv (fsuc i) = just (Equiv.from f i)
    maybe-iso f .snd .is-iso.rinv fzero = refl
    maybe-iso f .snd .is-iso.rinv (fsuc i) = ap fsuc (Equiv.Ξ΅ f i)
    maybe-iso f .snd .is-iso.linv (just x) = ap just (Equiv.Ξ· f x)
    maybe-iso f .snd .is-iso.linv nothing = refl

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