hurkens.ka

   1 bot : * => ([A : *] -> A)
   2
   3 not [A : *] : * => (A -> bot)
   4
   5 P [A : *] : * => (A -> *)
   6
   7 U : * => ([X : *] -> (P (P X) -> X) -> P (P X))
   8
   9 tau [t : P (P U)] : U => (
  10     \X f p => t (\x => p (f (x X f)))
  11 )
  12
  13 sigma [s : U] : P (P U) => (s U (\t => tau t))
  14
  15 Delta : P U => (
  16     \y => not ([p : P U] -> sigma y p -> p (tau (sigma y)))
  17 )
  18
  19 Omega : U => (
  20     tau (\p => [x : U] -> sigma x p -> p x)
  21 )
  22
  23 D : * => (
  24     [p : P U] -> sigma Omega p -> p (tau (sigma Omega))
  25 )
  26
  27 lem1 [p : P U] [H1 : [x : U] -> sigma x p -> p x] : p Omega => (
  28     H1 Omega (\x => H1 (tau (sigma x)))
  29 )
  30
  31 lem2 : not D => (
  32     lem1 Delta (\x H2 H3 => H3 Delta H2 (\p => H3 (\y => p (tau (sigma y)))))
  33 )
  34
  35 lem3 : D => (
  36     \p => lem1 (\y => p (tau (sigma y)))
  37 )
  38
  39 loop  : bot => (lem2 lem3)