\import Logic
\import Meta
\import Paths
\import Paths.Meta
\import Set

\record Partial \extends BaseSet
  | isDefined : \Prop
  | \coerce value : isDefined -> E
  \where {
    \lemma partial-ext {X : \Set} {u v : Partial X} (d : u.isDefined <-> v.isDefined) (e : \Pi (p : u.isDefined) -> u p = v (d. p)) : u = v
      => exts (<->_=. d, \lam p => e p *> pmap v prop-pi)
  }

\func defined {X : \Set} (x : X) : Partial X \cowith
  | isDefined => \Sigma
  | value _ => x

\func undefined {X : \Set} : Partial X \cowith
  | isDefined => Empty
  | value => \case __

\lemma defined-ext {X : \Set} {u : Partial X} {x : X} (d : u.isDefined) (p : u d = x) : u = defined x
  => Partial.partial-ext (\lam _ => (), \lam _ => d) \lam q => pmap u prop-pi *> p
  \where {
    \protected \lemma isDefined (p : u = defined x) : u.isDefined
      => transportInv (\lam x => Partial.isDefined {x}) p ()

    \protected \lemma value (p : u = defined x) : u (isDefined p) = x
      => transportInv (\lam (v : Partial X) => \Pi (p : v.isDefined) -> v p = x) p (\lam _ => idp) (isDefined p)
  }

\lemma undefined-ext {X : \Set} {u : Partial X} (d : Not u.isDefined) : u = undefined
  => Partial.partial-ext (d,absurd) \lam p => absurd (d p)