Hurkens' simplification of Girard's paradox for System U

:let False = (A : *) -> A

:let Not (A : *) = A -> False

:let U = (X : []) -> (((X -> *) -> *) -> X) -> (X -> *) -> *

:{:let tau (t : (U -> *) -> *) : U
            = \ (X : [])
                (f : ((X -> *) -> *) -> X)
                (p : X -> *) ->
                   t (\ (x : U) -> p (f (x X f)))
:}


:{:let sigma (s : U) : (U -> *) -> *
              = s U (\ (t : (U -> *) -> *) -> tau t)
:}

:let delta (y : U) = (p : U -> *) -> sigma y p -> p (tau (sigma y))


:let Delta (y : U) : * = Not (delta y)

:{:let Omega : U
              = tau (\ (p : U -> *) -> (x : U) -> sigma x p -> p x)
:}

:let D = (p : U -> *) -> sigma Omega p -> p (tau (sigma Omega))

:{:let lem1 (p : U -> *) (H1 : (x : U) -> sigma x p -> p x) : p Omega
             = H1 Omega (\ (x : U) -> H1 (tau (sigma x)))
:}

:{:let lem2 : Not D
             = lem1 Delta
                    (\ (x  : U)
                       (H2 : sigma x Delta)
                       (H3 : delta x) ->
                           H3 Delta H2
                              (\ (p : U -> *) ->
                                    H3 (\ (y : U) -> p (tau (sigma y)))))
:}

:{:let lem3 : D
             = \ (p : U -> *) ->
                    lem1 (\ (x : U) -> p (tau (sigma x)))
:}

:let loop : False = lem2 lem3