blob: ba9602ad309da965a5f5bd31e7c2dab68ca375ef (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
bot : ⋆ ⇒ ([A : ⋆] → A)
not [A : ⋆] : ⋆ ⇒ (A → bot)
P [A : ⋆] : ⋆ ⇒ (A → ⋆)
U : ⋆ ⇒ ([X : ⋆] → (P (P X) → X) → P (P X))
tau [t : P (P U)] : U ⇒ (
λ X f p ⇒ t (λ x ⇒ p (f (x X f)))
)
sigma [s : U] : P (P U) ⇒ (s U tau)
Delta : P U ⇒ (
λ y ⇒ not ([p : P U] → sigma y p → p (tau (sigma y)))
)
Omega : U ⇒ (
tau (λ p ⇒ [x : U] → sigma x p → p x)
)
D : ⋆ ⇒ (
[p : P U] → sigma Omega p → p (tau (sigma Omega))
)
lem1 [p : P U] [H1 : [x : U] → sigma x p → p x] : p Omega ⇒ (
H1 Omega (λ x ⇒ H1 (tau (sigma x)))
)
lem2 : not D ⇒ (
lem1 Delta (λ x H2 H3 ⇒ H3 Delta H2 (λ p ⇒ H3 (λ y ⇒ p (tau (sigma y)))))
)
lem3 : D ⇒ (
λ p ⇒ lem1 (λ y ⇒ p (tau (sigma y)))
)
loop : bot ⇒ (lem2 lem3)
|
