43 lines
1.6 KiB
Text
43 lines
1.6 KiB
Text
load "misc.quox"
|
||
|
||
def0 Irr1 : (A : ★) → (A → ★) → ★ =
|
||
λ A P ⇒ (x : A) → (p q : P x) → p ≡ q : P x
|
||
|
||
def0 Sub : (A : ★) → (P : A → ★) → ★ =
|
||
λ A P ⇒ (x : A) × [0. P x]
|
||
|
||
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.(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 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 → ★) → 0.(Irr1 A P) →
|
||
((x : A) → Dup A x) →
|
||
(s : Sub A P) → SubDup A P s =
|
||
λ A P pirr 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 → ★) → 0.(Irr1 A P) →
|
||
((x : A) → Dup A x) →
|
||
(s : Sub A P) → Dup (Sub A P) s =
|
||
λ A P pirr dup s ⇒ subdup-to-dup A P pirr s (subdup A P pirr dup s)
|
||
|
||
def forget : 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 }
|