Hurken's paradox in SAWCore

Hurkens.sawcore

-- Adapted from:
-- - https://github.com/agda/agda/blob/4a93aa6ffbcc55df5e4f65ecb4dc1d6215501a79/test/Fail/Issue3327.agda
-- - https://github.com/dhall-lang/dhall-lang/issues/250

module Hurkens where

import Prelude;

-- This should not be allowed
data Sort : sort 0 where {
  in : sort 0 -> Sort;
}

out : Sort -> sort 0;
out A' = Sort#rec (\ (_:Sort) -> sort 0) (\ (A:sort 0) -> A) A';

-- The rest is Hurken's paradox.

Bot : Sort;
Bot = in ((A:Sort) -> out A);

Arrow : Sort -> Sort -> Sort;
Arrow A B = in (out A -> out B);

Pi : (A:Sort) -> (out A -> Sort) -> Sort;
Pi A B = in ((x:out A) -> out (B x));

Not : Sort -> Sort;
Not A = Arrow A Bot;

P : Sort -> Sort;
P A = in (out A -> Sort);

U : Sort;
U = in ((X : Sort) -> out (Arrow (Arrow (P (P X)) X) (P (P X))));

tau : out (Arrow (P (P U)) U);
tau t = \ (X : Sort) -> \ (f : out (Arrow (P (P X)) X)) -> \ (p : out (P X)) ->
          t (\ (x : out U) -> p (f (x X f)));

sigma : out (Arrow U (P (P U)));
sigma s pu = s U (\ (t : out (P (P U))) -> tau t) pu;

delta : out (P U);
delta = \ (y : out U) -> Not (Pi (P U) (\ (p : out (P U)) -> Arrow (sigma y p) (p (tau (sigma y)))));

omega : out U;
omega X t px = tau (\ (p : out (P U)) -> Pi U (\ (x : out U) -> Arrow (sigma x p) (p x))) X t px;

D : Sort;
D = Pi (P U) (\ (p : out (P U)) -> Arrow (sigma omega p) (p (tau (sigma omega))));

lem1 : out (Pi (P U) (\ (p : out (P U)) -> Arrow (Pi U (\ (x : out U) -> Arrow (sigma x p) (p x))) (p omega)));
lem1 p H1 = H1 omega (\ (x : out U) -> H1 (tau (sigma x)));

lem2 : out (Not D);
lem2 d A = lem1 delta (\ (x : out U) -> \ (H2 : out (sigma x delta)) ->
                       \ (H3 : out (Pi (P U) (\ (p : out (P U)) -> Arrow (sigma x p) (p (tau (sigma x)))))) ->
                         H3 delta H2 (\ (p : out (P U)) -> H3 (\ (y : out U) -> p (tau (sigma y))))) d A;

lem3 : out D;
lem3 p = lem1 (\ (y : out U) -> p (tau (sigma y)));

loop : out Bot;
loop = lem2 lem3;

absurd : EqP Bool True False;
absurd = loop (in (EqP Bool True False));