module Foundation.Data.Maybe where

open import Foundation.Prelude
open import Foundation.Data.Sum
open import Foundation.Data.Unit

open import Data.Maybe public
  using ()
  renaming (is-just to isSome; is-nothing to isNone)

open import Data.Maybe.Properties public
  using ()
  renaming (just-injective to some-inj)

open import Cubical.Data.Maybe as 🧊
  using ()
  renaming (
    Maybe to infix 30 _？🧊; nothing to none🧊; just to some🧊;
    Maybe≡SumUnit to Maybe≡SumUnit🧊)

import Cubical.Data.Sum as 🧊

Maybe→🧊 : A ？ → A ？🧊
Maybe→🧊 none = none🧊
Maybe→🧊 (some x) = some🧊 x

Maybe←🧊 : A ？🧊 → A ？
Maybe←🧊 none🧊 = none
Maybe←🧊 (some🧊 x) = some x

Maybe→←🧊 : (x : A ？🧊) → Maybe→🧊 (Maybe←🧊 x) ≡ x
Maybe→←🧊 none🧊 = refl
Maybe→←🧊 (some🧊 x) = refl

Maybe←→🧊 : (x : A ？) → Maybe←🧊 (Maybe→🧊 x) ≡ x
Maybe←→🧊 none = refl
Maybe←→🧊 (some x) = refl

Maybe≅🧊 : A ？ ≅ A ？🧊
Maybe≅🧊 = mk≅ Maybe→🧊 Maybe←🧊 Maybe→←🧊 Maybe←→🧊

Maybe≡🧊 : A ？ ≡ A ？🧊
Maybe≡🧊 = ua Maybe≅🧊

Maybe≡SumUnit : A ？ ≡ ⊤ ⊎ A
Maybe≡SumUnit {A} =
  A ？ ≡⟨ Maybe≡🧊 ⟩
  A ？🧊 ≡⟨ Eq←🧊 Maybe≡SumUnit🧊 ⟩
  ⊤ 🧊.⊎ A ≡˘⟨ Sum≡🧊 ⟩
  ⊤ ⊎ A ∎

isSetMaybe : isSet A → isSet (A ？)
isSetMaybe setA = subst isSet Maybe≡SumUnit (isSet⊎ isSet⊤ setA)
