66 lines
2.2 KiB
Text
66 lines
2.2 KiB
Text
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ω)
|
||
}
|
||
-}
|
||
|
||
}
|