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