{-# OPTIONS --safe #-}
module Cubical.Data.Maybe.Properties where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function using (_∘_; idfun)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Pointed.Base using (Pointed; _→∙_; pt)
open import Cubical.Foundations.Structure using (⟨_⟩)
open import Cubical.Functions.Embedding using (isEmbedding)
open import Cubical.Data.Empty as  using (; isProp⊥)
open import Cubical.Data.Unit
open import Cubical.Data.Nat using (suc)
open import Cubical.Data.Sum using (_⊎_; inl; inr)
open import Cubical.Data.Sigma using (ΣPathP)
open import Cubical.Relation.Nullary using (¬_; Discrete; yes; no)
open import Cubical.Data.Maybe.Base as Maybe
Maybe∙ :  {} (A : Type )  Pointed 
Maybe∙ A .fst = Maybe A
Maybe∙ A .snd = nothing
-- Maybe∙ is the "free pointing" functor, that is, left adjoint to the
-- forgetful functor forgetting the base point.
module _ {} (A : Type ) {ℓ'} (B : Pointed ℓ') where
  freelyPointedIso : Iso (Maybe∙ A →∙ B) (A   B )
  Iso.fun freelyPointedIso f∙ = fst f∙  just
  Iso.inv freelyPointedIso f = Maybe.rec (pt B) f , refl
  Iso.rightInv freelyPointedIso f = refl
  Iso.leftInv freelyPointedIso f∙ =
      ( funExt (Maybe.elim _ (sym (snd f∙))  a  refl))
      , λ i j  snd f∙ (~ i  j))
map-Maybe-id :  {} {A : Type }   m  map-Maybe (idfun A) m  m
map-Maybe-id nothing = refl
map-Maybe-id (just _) = refl
-- Path space of Maybe type
module MaybePath {} {A : Type } where
  Cover : Maybe A  Maybe A  Type 
  Cover nothing  nothing   = Lift Unit
  Cover nothing  (just _)  = Lift 
  Cover (just _) nothing   = Lift 
  Cover (just a) (just a') = a  a'
  reflCode : (c : Maybe A)  Cover c c
  reflCode nothing  = lift tt
  reflCode (just b) = refl
  encode :  c c'  c  c'  Cover c c'
  encode c _ = J  c' _  Cover c c') (reflCode c)
  encodeRefl :  c  encode c c refl  reflCode c
  encodeRefl c = JRefl  c' _  Cover c c') (reflCode c)
  decode :  c c'  Cover c c'  c  c'
  decode nothing  nothing  _ = refl
  decode (just _) (just _) p = cong just p
  decodeRefl :  c  decode c c (reflCode c)  refl
  decodeRefl nothing  = refl
  decodeRefl (just _) = refl
  decodeEncode :  c c'  (p : c  c')  decode c c' (encode c c' p)  p
  decodeEncode c _ =
    J  c' p  decode c c' (encode c c' p)  p)
      (cong (decode c c) (encodeRefl c)  decodeRefl c)
  encodeDecode :  c c'  (d : Cover c c')  encode c c' (decode c c' d)  d
  encodeDecode nothing nothing _ = refl
  encodeDecode (just a) (just a') =
    J  a' p  encode (just a) (just a') (cong just p)  p) (encodeRefl (just a))
  Cover≃Path :  c c'  Cover c c'  (c  c')
  Cover≃Path c c' = isoToEquiv
    (iso (decode c c') (encode c c') (decodeEncode c c') (encodeDecode c c'))
  Cover≡Path :  c c'  Cover c c'  (c  c')
  Cover≡Path c c' = isoToPath
    (iso (decode c c') (encode c c') (decodeEncode c c') (encodeDecode c c'))
  isOfHLevelCover : (n : HLevel)
     isOfHLevel (suc (suc n)) A
      c c'  isOfHLevel (suc n) (Cover c c')
  isOfHLevelCover n p nothing  nothing   = isOfHLevelLift (suc n) (isOfHLevelUnit (suc n))
  isOfHLevelCover n p nothing  (just a') = isOfHLevelLift (suc n) (isProp→isOfHLevelSuc n isProp⊥)
  isOfHLevelCover n p (just a) nothing   = isOfHLevelLift (suc n) (isProp→isOfHLevelSuc n isProp⊥)
  isOfHLevelCover n p (just a) (just a') = p a a'
isOfHLevelMaybe :  {} (n : HLevel) {A : Type }
   isOfHLevel (suc (suc n)) A
   isOfHLevel (suc (suc n)) (Maybe A)
isOfHLevelMaybe n lA c c' =
  isOfHLevelRetract (suc n)
    (MaybePath.encode c c')
    (MaybePath.decode c c')
    (MaybePath.decodeEncode c c')
    (MaybePath.isOfHLevelCover n lA c c')
    : Level
   A : Type 
fromJust-def : A  Maybe A  A
fromJust-def a nothing = a
fromJust-def _ (just a) = a
just-inj : (x y : A)  just x  just y  x  y
just-inj x _ eq = cong (fromJust-def x) eq
isEmbedding-just : isEmbedding (just {A = A})
isEmbedding-just  w z = MaybePath.Cover≃Path (just w) (just z) .snd
¬nothing≡just :  {x : A}  ¬ (nothing  just x)
¬nothing≡just {A = A} {x = x} p = lower (subst (caseMaybe (Maybe A) (Lift )) p (just x))
¬just≡nothing :  {x : A}  ¬ (just x  nothing)
¬just≡nothing {A = A} {x = x} p = lower (subst (caseMaybe (Lift ) (Maybe A)) p (just x))
isProp-x≡nothing : (x : Maybe A)  isProp (x  nothing)
isProp-x≡nothing nothing x w =
  subst isProp (MaybePath.Cover≡Path nothing nothing) (isOfHLevelLift 1 isPropUnit) x w
isProp-x≡nothing (just _) p _ = ⊥.rec (¬just≡nothing p)
isProp-nothing≡x : (x : Maybe A)  isProp (nothing  x)
isProp-nothing≡x nothing x w =
  subst isProp (MaybePath.Cover≡Path nothing nothing) (isOfHLevelLift 1 isPropUnit) x w
isProp-nothing≡x (just _) p _ = ⊥.rec (¬nothing≡just p)
isContr-nothing≡nothing : isContr (nothing {A = A}  nothing)
isContr-nothing≡nothing = inhProp→isContr refl (isProp-x≡nothing _)
discreteMaybe : Discrete A  Discrete (Maybe A)
discreteMaybe eqA nothing nothing    = yes refl
discreteMaybe eqA nothing (just a')  = no ¬nothing≡just
discreteMaybe eqA (just a) nothing   = no ¬just≡nothing
discreteMaybe eqA (just a) (just a') with eqA a a'
... | yes p = yes (cong just p)
... | no ¬p = no  p  ¬p (just-inj _ _ p))
module SumUnit where
  Maybe→SumUnit : Maybe A  Unit  A
  Maybe→SumUnit nothing  = inl tt
  Maybe→SumUnit (just a) = inr a
  SumUnit→Maybe : Unit  A  Maybe A
  SumUnit→Maybe (inl _) = nothing
  SumUnit→Maybe (inr a) = just a
  Maybe→SumUnit→Maybe : (x : Maybe A)  SumUnit→Maybe (Maybe→SumUnit x)  x
  Maybe→SumUnit→Maybe nothing  = refl
  Maybe→SumUnit→Maybe (just _) = refl
  SumUnit→Maybe→SumUnit : (x : Unit  A)  Maybe→SumUnit (SumUnit→Maybe x)  x
  SumUnit→Maybe→SumUnit (inl _) = refl
  SumUnit→Maybe→SumUnit (inr _) = refl
Maybe≡SumUnit : Maybe A  Unit  A
Maybe≡SumUnit = isoToPath (iso Maybe→SumUnit SumUnit→Maybe SumUnit→Maybe→SumUnit Maybe→SumUnit→Maybe)
  where open SumUnit
congMaybeEquiv :  { ℓ'} {A : Type } {B : Type ℓ'}
   A  B  Maybe A  Maybe B
congMaybeEquiv e = isoToEquiv isom
  open Iso
  isom : Iso _ _
  isom .fun = map-Maybe (equivFun e)
  isom .inv = map-Maybe (invEq e)
  isom .rightInv nothing = refl
  isom .rightInv (just b) = cong just (secEq e b)
  isom .leftInv nothing = refl
  isom .leftInv (just a) = cong just (retEq e a)