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

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
decomp-maybe : β {β} {A : Type β} β hlevel-decomposition (Maybe A)
decomp-maybe = decomp (quote Maybe-is-hlevel) (level-minus 2 β· search β· [])


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