...

[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)