diff options
author | Francesco Mazzoli <f@mazzo.li> | 2013-06-10 17:03:52 +0100 |
---|---|---|
committer | Francesco Mazzoli <f@mazzo.li> | 2013-06-10 17:03:52 +0100 |
commit | 220ca85e4c690269298b9e8c1ef1752fad285855 (patch) | |
tree | 8a5baaec4bd038e8af7966c49e21b4ea8c0a22a4 /hurkens.ka | |
parent | 2a33412a41393afc6574354625c0d9434f099754 (diff) |
...
Diffstat (limited to 'hurkens.ka')
-rw-r--r-- | hurkens.ka | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/hurkens.ka b/hurkens.ka new file mode 100644 index 0000000..61cbadc --- /dev/null +++ b/hurkens.ka @@ -0,0 +1,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) |