load "misc.quox"
load "either.quox"
load "maybe.quox"

namespace sub {

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

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

def0 Irr2 : (A B : ★) → (A → B → ★) → ★ =
  λ A B P ⇒ (x : A) → (y : B) → Irr (P x y)

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)) →
           ω.A → Maybe (Sub A P) =
  λ A P p? x ⇒
    dec.elim (P x) (λ _ ⇒ Maybe (Sub A P))
      (λ y ⇒ Just (Sub A P) (x, [y]))
      (λ n ⇒ Nothing (Sub A P))
      (p? x)


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

def0 proof : 0.(A : ★) → 0.(P : A → ★) → (s : Sub A P) → P (fst s) =
  λ A P s ⇒ get0 (P (fst s)) (snd s)

{-

def0 proof' : 0.(A : ★) → 0.(P : A → ★) → (s : Sub A P) → P (fst s) =
  λ A P s ⇒ get0 (P (fst s)) (snd s)

def0 val-fst : (A : ★) → (P : A → ★) →
               (s : Sub A P) → val A P s ≡ fst s : A =
  λ A P s ⇒
    case s return s' ⇒ val A P s' ≡ fst s' : A of {
      (x, p) ⇒ drop0-eq (P x) A p x
    }

def0 proof : 0.(A : ★) → 0.(P : A → ★) → (s : Sub A P) → P (val A P s) =
  λ A P s ⇒ coe (𝑖 ⇒ P (val-fst A P s @𝑖)) @1 @0 (proof' A P s)

postulate0 proof-snd' : (A : ★) → (P : A → ★) → (s : Sub A P) →
                  Eq (𝑖 ⇒ P (val-fst A P s @𝑖)) (proof A P s) (proof' A P s)

postulate0 proof-snd : (A : ★) → (P : A → ★) → (s : Sub A P) →
                 Eq (𝑖 ⇒ [0.P (val-fst A P s @𝑖)]) [proof A P s] (snd s)

#![log (all, 10) (equal, 100)]
def0 val-proof-eq : (A : ★) → (P : A → ★) → (s : Sub A P) →
                    sub A P (val A P s) (proof A P s) ≡ s : Sub A P =
  λ A P s ⇒
    case s return s' ⇒ sub A P (val A P s') (proof A P s') ≡ s' : Sub A P
    of { (xxxxx, p) ⇒
      case p
      return p' ⇒
        sub A P (val A P (xxxxx, p')) (proof A P (xxxxx, p')) ≡ (xxxxx, p') : Sub A P
      of { [p0] ⇒
        δ 𝑖 ⇒ (val-fst A P (xxxxx, [p0]) @𝑖, proof-snd A P (xxxxx, [p0]) @𝑖)
      }
    }
#![log pop]

def elim' : 0.(A : ★) → 0.(P : A → ★) →
            0.(R : (x : A) → P x → ★) →
            (1.(x : A) → 0.(p : P x) → R x p) →
            (s : Sub A P) → R (val A P s) (proof A P s) =
  λ A P R p s ⇒ p (val A P s) (proof A P s)

{-
def elim : 0.(A : ★) → 0.(P : A → ★) →
           0.(R : Sub A P → ★) →
           (1.(x : A) → 0.(p : P x) → R (x, [p])) →
           (s : Sub A P) → R s =
  λ A P R p s ⇒ p (val A P s) (proof A P s)
-}

-}



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

def subdup-to-dup :
    0.(A : ★) → 0.(P : A → ★) →
    0.(s : Sub A P) → SubDup A P s → Dup (Sub A P) s =
  λ A P s sd ⇒
    case sd return Dup (Sub A P) s of { (sω, ss0) ⇒
    case ss0 return Dup (Sub A P) s of { [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' in
        ([(s!, coe (𝑖 ⇒ [0.P (ss @𝑖)]) @1 @0 p)],
         [δ 𝑗 ⇒ [(ss @𝑗, coe (𝑖 ⇒ [0.P (ss @𝑖)]) @1 @𝑗 p)]])
      } ss0
    }}

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

def dup! : 0.(A : ★) → 0.(P : A → ★) → ((x : A) → Dup A x) →
           (s : Sub A P) → Dup (Sub A P) s =
  λ A P dupA s ⇒ subdup-to-dup A P s (subdup A P dupA s)


def0 irr1-het : (A : ★) → (P : A → ★) → Irr1 A P →
                (x y : A) → (p : P x) → (q : P y) →
                (xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) p q =
  λ A P pirr x y p q xy ⇒ δ 𝑖 ⇒
    pirr (xy @𝑖) (coe (𝑗 ⇒ P (xy @𝑗)) @0 @𝑖 p) (coe (𝑗 ⇒ P (xy @𝑗)) @1 @𝑖 q) @𝑖

def0 irr2-het : (A B : ★) → (P : A → B → ★) → Irr2 A B P →
                (x₀ x₁ : A) → (y₀ y₁ : B) → (p : P x₀ y₀) → (q : P x₁ y₁) →
                (xx : x₀ ≡ x₁ : A) → (yy : y₀ ≡ y₁ : B) →
                Eq (𝑖 ⇒ P (xx @𝑖) (yy @𝑖)) p q =
  λ A B P pirr x₀ x₁ y₀ y₁ p q xx yy ⇒ δ 𝑖 ⇒
    pirr (xx @𝑖) (yy @𝑖)
         (coe (𝑗 ⇒ P (xx @𝑗) (yy @𝑗)) @0 @𝑖 p)
         (coe (𝑗 ⇒ P (xx @𝑗) (yy @𝑗)) @1 @𝑖 q) @𝑖


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 proof = proof A P in
    (xy0 @𝑖, [irr1-het A P pirr (fst x) (fst y) (proof x) (proof y) xy0 @𝑖])


def eq? : 0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) →
          DecEq A → DecEq (Sub A P) =
  λ A P pirr aeq? s t ⇒
    let0 EQ : ★ = s ≡ t : Sub A P in
    dec.elim (fst s ≡ fst t : A) (λ _ ⇒ Dec EQ)
      (λ y ⇒ Yes EQ (sub-eq A P pirr s t y))
      (λ n ⇒ No  EQ (λ eq ⇒ n (δ 𝑖 ⇒ fst (eq @𝑖))))
      (aeq? (fst s) (fst t))

}

def0 Sub = sub.Sub