load "maybe.quox"

namespace sub {

def0 Irr : ★ → ★ =
  λ A ⇒ (x y : A) → x ≡ y : A

def0 Irr1 : (A : ★) → (A → ★) → ★ =
  λ A P ⇒ (x : A) → Irr (P x)

def0 Sub : (A : ★) → (P : A → ★) → ★ =
  λ A P ⇒ (x : A) × [0. P x]

def sub : 0.(A : ★) → 0.(P : A → ★) → (x : A) → 0.(P x) → Sub A P =
  λ A P x p ⇒ (x, [p])

def sub? : 0.(A : ★) → 0.(P : A → ★) → (ω.(x : A) → Dec (P x)) →
           ω.(x : A) → Maybe (Sub A P) =
  λ A P p? x ⇒
    dec.elim (P x) (λ _ ⇒ Maybe (Sub A P))
      (λ yes ⇒ Just (Sub A P) (sub A P x yes))
      (λ no  ⇒ Nothing (Sub A P))
      (p? x)

def0 sub-eq : (A : ★) → (P : A → ★) → (Irr1 A P) → (x y : Sub A P) →
              (fst x ≡ fst y : A) → (x ≡ y : Sub A P) =
  λ A P pirr x y xy0 ⇒
    let x1 = get0 (P (fst x)) (snd x); y1 = get0 (P (fst y)) (snd y) in
    let xy1 : Eq (𝑖 ⇒ P (xy0 @𝑖)) x1 y1 =
      δ 𝑖 ⇒ pirr (xy0 @𝑖)
        (coe (𝑗 ⇒ P (xy0 @𝑗)) @0 @𝑖 x1)
        (coe (𝑗 ⇒ P (xy0 @𝑗)) @1 @𝑖 y1) @𝑖 in
    δ 𝑖 ⇒ (xy0 @𝑖, [xy1 @𝑖])


def0 SubDup : (A : ★) → (P : A → ★) → Sub A P → ★ =
  λ A P s ⇒ (x! : [ω.A]) × [0. x! ≡ [fst s] : [ω.A]]

def subdup : 0.(A : ★) → 0.(P : A → ★) →
             ((x : A) → Dup A x) → (s : Sub A P) → SubDup A P s =
  λ A P dupA s ⇒
    case s return s' ⇒ SubDup A P s' of { (x, p) ⇒
      drop0 (P x) (SubDup A P (x, p)) p (dupA x)
    }


{-
type checker loop?????????????????? :(
def subdup-to-dup :
    0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) →
    0.(s : Sub A P) → SubDup A P s → Dup (Sub A P) s =
  λ A P pirr s sd ⇒
    case sd return Dup (Sub A P) s of { (sω, ss0) ⇒
      case sω
      return sω' ⇒ 0.(sω' ≡ [fst s] : [ω.A]) → Dup (Sub A P) s
      of { [s!] ⇒ λ ss' ⇒
        let ω.p  : [0.P (fst s)] = revive0 (P (fst s)) (snd s);
            0.ss : s! ≡ fst s : A = boxω-inj A s! (fst s) ss';
            0.pss : [0.P s!] ≡ [0.P (fst s)] : ★ = (δ 𝑖 ⇒ [0.P (ss @𝑖)]) in
        ([(s!, coe (𝑖 ⇒ pss @𝑖) @1 @0 p)],
         [δ 𝑖 ⇒ [(ss @𝑖, coe (𝑗 ⇒ pss @𝑗) @1 @𝑖 p)]])
      } (δ _ ⇒ sω)
    }
-}

}