diff options
Diffstat (limited to 'hurkens.ka')
| -rw-r--r-- | hurkens.ka | 40 |
1 files changed, 20 insertions, 20 deletions
@@ -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) |