blob: 61cbadcfc0473feddcdeea0b60726cfa8e3c6c6d (
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 (\t => tau t))
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)
|
