%%% Hurkens' simplification of Girard's paradox
%%% (itself inspired by the Burali-Forti paradox for naive set theory)
%%%
%%% Kevin Watkins
%%% July 2004
%%%
%%% See "A simplification of Girard's paradox," Antonius J.C. Hurkens,
%%% Proceedings TLCA'95.

%% The consistent system HOL

tp : type.
o : tp.
--> : tp -> tp -> tp.                   %infix right 0 -->.

tm : tp -> type.
\ : (tm A -> tm B) -> tm (A --> B).
@ : tm (A --> B) -> (tm A -> tm B).     %infix left 10 @.

=> : tm o -> tm o -> tm o.              %infix right 5 =>.
all : (tm A -> tm o) -> tm o.

pf : tm o -> type.
lam : (pf P -> pf Q) -> pf (P => Q).
app : pf (P => Q) -> (pf P -> pf Q).    %infix left 10 app.
gen : ({T:tm A} pf (P T)) -> pf (all P).
spec : pf (all P) -> ({T:tm A} pf (P T)). %infix left 10 spec.

% Conversion rule
apply = [x] [y] x @ y.
beta : {P:((tm A -> tm B) -> (tm A -> tm B)) -> tm o}
         pf (P ([F] apply (\ F))) -> pf (P ([F] F)).

% It is also consistent to add the following, but they are not
% used in the paradox.
alltp : (tp -> tm o) -> tm o.
gentp : ({A:tp} pf (P A)) -> pf (alltp P).
spectp : pf (alltp P) -> ({A:tp} pf (P A)). %infix left 10 spectp.


%% The inconsistent system U

% These constructors are not used except to establish the
% existence of a "powerful universe".

pi : (tp -> tp) -> tp.
\\ : ({A:tp} tm (B A)) -> tm (pi B).
@@ : tm (pi B) -> ({A:tp} tm (B A)).    %infix left 10 @@.

aapply = [x] [a] x @@ a.
bbeta : {P:(({A:tp} tm (B A)) -> ({A:tp} tm (B A))) -> tm o}
         pf (P ([F] aapply (\\ F))) -> pf (P ([F] F)).


%% Leibniz equality

== : tm A -> tm A -> tm o
  = [T] [U] all[P:tm (A --> o)] P @ T => P @ U.
                                        %infix none 0 ==.
refl : pf (T == T)
  = gen[P] lam[D] D.
sub : pf (T == U) -> {P:tm A -> tm o} pf (P T) -> pf (P U)
  = [D] [P] [E] beta ([h] h ([x] P x) T => P U)
       (beta ([h] (\[x] P x) @ T => h ([x] P x) U)
       (D spec (\[x] P x))) app E.
sym : pf (T == U) -> pf (U == T)
  = [D] sub D ([x] x == T) refl.


%% Conversions

; : pf (S == T) -> pf (T == U) -> pf (S == U)
  = [D] [E] sub E ([x] S == x) D.
                                        %infix left 20 ;.

conv : pf P -> pf (P == Q) -> pf Q
  = [D] [E] sub E ([x] x) D.
                                        %infix left 10 conv.


%% Normalization

% Definition of redices
redex : tm A -> type.
bred : {S:((tm A -> tm B) -> (tm A -> tm B)) -> tm C}
        redex (S ([F] apply (\ F))).
bbred : {S:(({A:tp} tm (B A)) -> ({A:tp} tm (B A))) -> tm C}
        redex (S ([F] aapply (\\ F))).

% Congruence rules for redices
congred : {F:tm A -> tm B} redex T -> redex (F T) -> type.
congred_b : congred F (bred ([h] R h)) (bred ([h] F (R h))).
congred_bb : congred F (bbred ([h] R h)) (bbred ([h] F (R h))).

fcongred : {F:(tm A -> tm B) -> tm C}
        ({x} redex (T x)) -> redex (F ([x] T x)) -> type.
fcongred_b : fcongred F ([x] bred ([h] R h x)) (bred ([h] F ([x] R h x))).
fcongred_bb : fcongred F ([x] bbred ([h] R h x)) (bbred ([h] F ([x] R h x))).

ffcongred : {F:({A:tp} tm (B A)) -> tm C}
        ({x} redex (T x)) -> redex (F ([x] T x)) -> type.
ffcongred_b : ffcongred F ([x] bred ([h] R h x)) (bred ([h] F ([x] R h x))).
ffcongred_bb : ffcongred F ([x] bbred ([h] R h x)) (bbred ([h] F ([x] R h x))).

% Leftmost-outermost redex
lor : {T:tm A} redex T -> type.
lor_bred : lor ((\[x] T x) @ U) (bred ([h] h ([x] T x) U)).
lor_bbred : lor ((\\[x] T x) @@ U) (bbred ([h] h ([x] T x) U)).
lor_\ : lor (\[x] T x) Redex'
        <- ({x} lor (T x) (Redex x))
        <- fcongred ([f] \ f) ([x] Redex x) Redex'.
lor_\\ : lor (\\[x] T x) Redex'
        <- ({x} lor (T x) (Redex x))
        <- ffcongred ([f] \\ f) ([x] Redex x) Redex'.
lor_@1 : lor (T @ U) Redex'
        <- lor T Redex
        <- congred ([x] x @ U) Redex Redex'.
lor_@2 : lor (T @ U) Redex'
        <- lor U Redex
        <- congred ([x] T @ x) Redex Redex'.
lor_@@ : lor (T @@ U) Redex'
        <- lor T Redex
        <- congred ([x] x @@ U) Redex Redex'.
lor_=>1 : lor (T => U) Redex'
        <- lor T Redex
        <- congred ([x] x => U) Redex Redex'.
lor_=>2 : lor (T => U) Redex'
        <- lor U Redex
        <- congred ([x] T => x) Redex Redex'.
lor_all : lor (all[x] T x) Redex'
        <- ({x} lor (T x) (Redex x))
        <- fcongred ([f] all f) ([x] Redex x) Redex'.

% Proof of a single reduction step
redconv : redex T -> {S:tm A} pf (T == S) -> type.
redconv_b : redconv (bred R) _ (beta ([h] R ([F] apply (\ F)) == R h) refl).
redconv_bb : redconv (bbred R) _ (bbeta ([h] R ([F] aapply (\\ F)) == R h) refl).

% Normalize
ahn : {T:tm A} pf (T == S) -> type.

ahn_step : ahn T (Proof1 ; Proof2)
        <- lor T Redex
        <- redconv Redex S Proof1
        <- ahn S Proof2.
ahn_done : ahn T refl.

% Without explicitly naming the term to normalize
mknorm : pf (T == S) -> type.
mknorm_ : mknorm Proof <- ahn _ Proof.

% Convert any two convertible terms
mkconv : {T:tm A} {U:tm A} pf (T == U) -> type.

mkconv_ : mkconv T U (Proof1 ; sym Proof2)
        <- ahn T Proof1
        <- ahn U Proof2.


%% The paradox itself

% Preliminaries
al = [A] [P] all[x:tm A] P x.
<F> = all[p] p.
not = [P] P => <F>.
set = [A] A --> o.
lift : (tm A -> tm B) -> (tm (set B) -> tm (set A))
  = [F] [T] \[x] T @ (F x).

% These three definitions (and the associated conversion) are the
% only ones making use of the full power of U-.
univ = pi[X] (set (set X) --> X) --> set (set X).
univ' = set univ.
univ'' = set univ'.
tau : tm univ'' -> tm univ
  = [T] \\[X] \[f] \[p] T @ (\[x] p @ (f @ (x @@ X @ f))).
sigma : tm univ -> tm univ''
  = [S] S @@ univ @ (\[t] tau t).

% The following conversion is the defining property of a
% "powerful universe".
%solve _ : mkconv (\[x] sigma (tau x))
                  (\[x] lift (lift ([x] tau (sigma x))) x) Proof.

omega : tm univ
  = tau (\[p] al(univ)[x] sigma x @ p => p @ x).
delta : tm univ'
  = \[y] not (al(univ')[p] sigma y @ p => p @ (tau (sigma y))).
theta : tm o
  = al(univ')[p] (al(univ)[x] sigma x @ p => p @ x) => p @ omega.

done : type.

%define part1 : pf theta
  = gen[p] lam[d] d spec omega conv (C1 p) app
        (gen[x] d spec (tau (sigma x)) conv (C2 p x))
%solve _ : {p} {x} (done <- mknorm (C1 p) <- mknorm (C2 p x)) -> done.

%define part2 : pf (not theta)
  = lam[d] d spec delta conv C1
        app (gen[x] lam[e] lam[f] f spec delta conv (C2 x) app e
                app (gen[p] f spec (\[y] p @ tau (sigma y)) conv (C3 x p)))
        app (gen[p] d spec (\[y] p @ tau (sigma y)) conv (C4 p))
%solve _ : {p} {x} (done
          <- mknorm C1
          <- mknorm (C2 x)
          <- mknorm (C3 x p)
          <- mknorm (C4 p)) -> done.

paradox : pf <F>
  = part2 app part1.