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