projects
/
bitonic-mengthesis.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
...
[bitonic-mengthesis.git]
/
hurkens.ka
diff --git
a/hurkens.ka
b/hurkens.ka
index 61cbadcfc0473feddcdeea0b60726cfa8e3c6c6d..ba9602ad309da965a5f5bd31e7c2dab68ca375ef 100644
(file)
--- a/
hurkens.ka
+++ b/
hurkens.ka
@@
-1,39
+1,39
@@
-bot :
* => ([A : *] ->
A)
+bot :
⋆ ⇒ ([A : ⋆] →
A)
-not [A :
*] : * => (A ->
bot)
+not [A :
⋆] : ⋆ ⇒ (A →
bot)
-P [A :
*] : * => (A -> *
)
+P [A :
⋆] : ⋆ ⇒ (A → ⋆
)
-U :
* => ([X : *] -> (P (P X) -> X) ->
P (P X))
+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)))
+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)
)
+sigma [s : U] : P (P U)
⇒ (s U tau
)
-Delta : P U
=>
(
-
\y => not ([p : P U] -> sigma y p ->
p (tau (sigma y)))
+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)
+Omega : U
⇒
(
+
tau (λ p ⇒ [x : U] → sigma x p →
p x)
)
)
-D :
* =>
(
-
[p : P U] -> sigma Omega p ->
p (tau (sigma Omega))
+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)))
+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)))))
+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)))
+lem3 : D
⇒
(
+
λ p ⇒ lem1 (λ y ⇒
p (tau (sigma y)))
)
)
-loop : bot
=>
(lem2 lem3)
+loop : bot
⇒
(lem2 lem3)