%%% Set extensionality proves "xi"
%%%
%%% Kevin Watkins
%%% August 2004
%%%
%%% See "Higher order semantics and extensionality", Benzmüller, Brown,
%%% Kohlhase, to appear in JSL.


%%% 0. Preliminaries

jg : type.
|- : jg -> type.

eqv = [J] [J'] {J''} ((|- J -> |- J') -> (|- J' -> |- J) -> |- J'') -> |- J''.
                                                %infix none 0 eqv.
%abbrev eqvI : J eqv J
   = [J] [f] f ([x] x) ([x] x).
%abbrev sym : J eqv J' -> J' eqv J
   = [eq] [J''] [f] eq J'' ([x] [y] f y x).
%abbrev trans : J1 eqv J2 -> J2 eqv J3 -> J1 eqv J3
   = [eq1] [eq2] [J'] [f] eq1 J' ([x1] [y1] eq2 J' ([x2] [y2] f ([z] x2 (x1 z))
                                                                ([z] y1 (y2 z)))).


%%% 1. The base theory of simply-typed functions

tp : type.
--> : 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 @.

apply = [x] [y] x @ y.
beta : {Ctx:((tm A -> tm B) -> (tm A -> tm B)) -> jg}
        Ctx ([x] apply (\ x)) eqv Ctx ([x] x).


%%% 2. Propositions as terms

o : tp.
true : tm o -> jg.
pf = [A] |- (true A).


%%% 3. Watkins-description (does not require an equality)

int : ((tm A -> tm o) -> tm o) -> tm A.

%abbrev lift : tm A -> ((tm A -> tm o) -> tm o) = [x] [p] p x.
intax : {Ctx:(tm A -> tm A) -> jg}
        Ctx ([x] int (lift x)) eqv Ctx ([x] x).


%%% 4. Boolean extensionality

boolext : (true P eqv true Q) -> {Ctx:tm o -> jg} Ctx P eqv Ctx Q.


%%% 5a. The eta rule

eta : {Ctx:(tm (A --> B) -> tm (A --> B)) -> jg}
        Ctx ([x] \ (apply x)) eqv Ctx ([x] x).


%%% 5b. The xi rule

xi : ({x:tm A} {Ctx:tm B -> jg} Ctx (F x) eqv Ctx (G x)) ->
        {Ctx:(tm A -> tm B) -> jg} Ctx F eqv Ctx G.


%%% 5c. Functional extensionality

fext : ({x:tm A} {Ctx:tm B -> jg} Ctx (S @ x) eqv Ctx (T @ x)) ->
        {Ctx:tm (A --> B) -> jg} Ctx S eqv Ctx T.


%%% Aside: Contextual equivalences of meta-functions can be reduced
%%% to contextual equivalences of object functions.

%abbrev
lower : ({Ctx:(tm A -> tm B) -> jg} Ctx F eqv Ctx G) ->
        {Ctx:tm (A --> B) -> jg} Ctx (\ F) eqv Ctx (\ G)
  = [D] [Ctx] D ([f] Ctx (\ f)).

%abbrev
raise : ({Ctx:tm (A --> B) -> jg} Ctx (\ F) eqv Ctx (\ G)) ->
        {Ctx:(tm A -> tm B) -> jg} Ctx F eqv Ctx G
  = [D] [Ctx] trans (sym (beta ([h] Ctx ([x] h F x))))
             (trans (D ([h] Ctx ([x] apply h x)))
                    (beta ([h] Ctx ([x] h G x)))).

% As a consequence, the rules intax, eta, xi can be restated
% equivalently as follows:

intax' : {Ctx:tm (A --> A) -> jg}
        Ctx (\[x] int (lift x)) eqv Ctx (\[x] x).
eta' : {Ctx:tm ((A --> B) --> (A --> B)) -> jg}
        Ctx (\[x] \ (apply x)) eqv Ctx (\[x] x).
xi' : ({x:tm A} {Ctx:tm B -> jg} Ctx (F x) eqv Ctx (G x)) ->
        {Ctx:tm (A --> B) -> jg} Ctx (\ F) eqv Ctx (\ G).

% Of course, the beta rule cannot be similarly reduced, because
% raise/lower themselves depend upon beta.


%%% Aside: Contextual equivalences of meta-functions have weaker
%%% variants.  If xi is available, the weaker and stronger versions
%%% collapse.

%abbrev
weaken : ({Ctx:(tm A -> tm B) -> jg} Ctx F eqv Ctx G) ->
        {T:tm A} {Ctx:tm B -> jg} Ctx (F T) eqv Ctx (G T)
  = [D] [T] [Ctx] D ([h] Ctx (h T)).

%abbrev
strengthen : ({T:tm A} {Ctx:tm B -> jg} Ctx (F T) eqv Ctx (G T)) ->
        {Ctx:(tm A -> tm B) -> jg} Ctx F eqv Ctx G
  = xi.

% Hence, the intax and eta rules have weaker variants as follows, which
% are equivalent to the stronger when xi is available.

wkintax : {Ctx:tm A -> jg}
        Ctx (int (lift T)) eqv Ctx T.
wketa : {Ctx:tm (A --> B) -> jg}
        Ctx (\ (apply T)) eqv Ctx T.

% And the beta rule, being a contextual equivalence of meta-functionals
% rather than meta-functions, has three weaker variants:

wkbeta1 : {Ctx:((tm A -> tm B) -> tm B) -> jg}
        Ctx ([x] apply (\ x) T) eqv Ctx ([x] x T).
wkbeta2 : {Ctx:(tm A -> tm B) -> jg}
        Ctx (apply (\ F)) eqv Ctx F.
wkbeta3 : {Ctx:tm B -> jg}
        Ctx (apply (\ F) T) eqv Ctx (F T).

% I have not explored the relation between intax/intax', eta/eta', xi/xi'
% in these weaker systems.


%%% 7. Set extensionality

setext : ({x} true (P x) eqv true (Q x)) ->
        {Ctx:(tm A -> tm o) -> jg} Ctx P eqv Ctx Q.

% "First-order" version
setext' : ({x} true (P x) eqv true (Q x)) ->
        {Ctx:tm (A --> o) -> jg} Ctx (\ P) eqv Ctx (\ Q).


%%% I. Set extensionality entails Boolean extensionality
%%% (if some type is non-empty)

sometype : tp.
something : tm sometype.

%abbrev
boolext~ : (true P eqv true Q) -> {Ctx:tm o -> jg} Ctx P eqv Ctx Q
  = [D] [Ctx] setext ([x] D) ([f] Ctx (f something)).


%%% II. Set extensionality entails xi, if Watkins-description
%%% is available

% Plan of proof:
% a. Define ordered pairs (not necessarily surjective)
% b. Use the ordered pairs to extend setext to binary relations
% c. Construct a representation of functions by their graphs
%    (again, not necessarily surjective)
% d. Prove xi using binary relation extensionality on graphs

%%% IIa. Definition of pairs

* = [A] [B] (A --> B --> o) --> o.              %infix right 5 *.
pair : tm A -> tm B -> tm (A * B) = [x] [y] \[f] f @ x @ y.
pi1 : tm (A * B) -> tm A = [z] int [p] z @ (\[x] \[y] p x).
pi2 : tm (A * B) -> tm B = [z] int [p] z @ (\[x] \[y] p y).

%abbrev
beta_pair1 : {Ctx:(tm A -> tm B -> tm A) -> jg}
        Ctx ([x] [y] pi1 (pair x y)) eqv Ctx ([x] [y] x)
  = [Ctx] trans (beta ([h] Ctx ([x] [y] int [p] h ([f] f @ x @ y) (\[x'] \[y'] p x'))))
         (trans (beta ([h] Ctx ([x] [y] int [p] h ([x'] \[y'] p x') x @ y)))
         (trans (beta ([h] Ctx ([x] [y] int [p] h ([y'] p x) y)))
                (intax ([h] Ctx ([x] [y] h x))))).
%abbrev
beta_pair2 : {Ctx:(tm A -> tm B -> tm B) -> jg}
        Ctx ([x] [y] pi2 (pair x y)) eqv Ctx ([x] [y] y)
  = [Ctx] trans (beta ([h] Ctx ([x] [y] int [p] h ([f] f @ x @ y) (\[x'] \[y'] p y'))))
         (trans (beta ([h] Ctx ([x] [y] int [p] h ([x'] \[y'] p y') x @ y)))
         (trans (beta ([h] Ctx ([x] [y] int [p] h ([y'] p y') y)))
                (intax ([h] Ctx ([x] [y] h y))))).

% Aside: an alternate elimination form

split : tm (A * B) -> (tm A -> tm B -> tm C) -> tm C
  = [z] [f] int [p] z @ (\[x] \[y] p (f x y)).

%abbrev
beta_pair : {Ctx:((tm A -> tm B -> tm C) -> (tm A -> tm B -> tm C)) -> jg}
        Ctx ([f] [x] [y] split (pair x y) f) eqv Ctx ([f] [x] [y] f x y)
  = [Ctx] trans (beta ([h] Ctx ([f] [x] [y] int [p] h ([f] f @ x @ y) (\[x] \[y] p (f x y)))))
         (trans (beta ([h] Ctx ([f] [x] [y] int [p] h ([x] \[y] p (f x y)) x @ y)))
         (trans (beta ([h] Ctx ([f] [x] [y] int [p] h ([y] p (f x y)) y)))
                (intax ([h] Ctx ([f] [x] [y] h (f x y)))))).


%%% IIb. Binary relation extensionality

%abbrev
lemma : {Ctx:((tm A -> tm B -> tm C) -> (tm A -> tm B -> tm C)) -> jg}
        Ctx ([f] [x] [y] f (pi1 (pair x y)) (pi2 (pair x y))) eqv Ctx ([f] f)
  = [Ctx] trans (beta_pair1 ([h] Ctx ([f] [x] [y] f (h x y) (pi2 (pair x y)))))
                (beta_pair2 ([h] Ctx ([f] [x] [y] f x (h x y)))).

%abbrev
binext : ({x} {y} true (P x y) eqv true (Q x y)) ->
        {Ctx:(tm A -> tm B -> tm o) -> jg} Ctx P eqv Ctx Q
  = [D] [Ctx] trans (sym (lemma ([h] Ctx (h P))))
             (trans (setext ([z] D (pi1 z) (pi2 z)) ([h] Ctx ([x] [y] h (pair x y))))
                    (lemma ([h] Ctx (h Q)))).


%%% IIc. Definition of the graph of a meta-function

%abbrev
graph : (tm A -> tm B) -> (tm A -> tm (B --> o) -> tm o)
  = [f] [x] [p] p @ (f x).
%abbrev
ungraph : (tm A -> tm (B --> o) -> tm o) -> (tm A -> tm B)
  = [g] [x] int [p] g x (\[y] p y).

%abbrev
beta_graph : {Ctx:((tm A -> tm B) -> (tm A -> tm B)) -> jg}
        Ctx ([f] ungraph (graph f)) eqv Ctx ([f] f)
  = [Ctx] trans (beta ([h] Ctx ([f] [x] int [p] h ([y] p y) (f x))))
                (intax ([h] Ctx ([f] [x] h (f x)))).


%%% IId. The xi rule

%abbrev
lemma : ({x:tm A} {Ctx:tm B -> jg} Ctx (F x) eqv Ctx (G x)) ->
        {Ctx:(tm A -> tm (B --> o) -> tm o) -> jg} Ctx (graph F) eqv Ctx (graph G)
  = [D] [Ctx] binext ([x] [p] D x ([y] true (p @ y))) Ctx.

%abbrev
xi~ : ({x:tm A} {Ctx:tm B -> jg} Ctx (F x) eqv Ctx (G x)) ->
        {Ctx:(tm A -> tm B) -> jg} Ctx F eqv Ctx G
  = [D] [Ctx] trans (sym (beta_graph ([h] Ctx (h F))))
             (trans (lemma D ([h] Ctx (ungraph h)))
                    (beta_graph ([h] Ctx (h G)))).


%%% 8. Equality

== : tm A -> (tm A -> tm o).                    %infix none 2 ==.

in : ({Ctx:tm A -> jg} Ctx S eqv Ctx T) -> pf (S == T).
out : pf (S == T) -> ({Ctx:tm A -> jg} Ctx S eqv Ctx T).

% The above is a symmetric description; the following simpler
% axiom is equivalent to in:

refl : pf (T == T).

%abbrev
in~ : ({Ctx:tm A -> jg} Ctx S eqv Ctx T) -> pf (S == T)
  = [D] D ([h] true (S == h)) _ ([f] [g] f refl).
%abbrev
refl~ : pf (T == T)
  = in ([Ctx] eqvI).


%%% Aside: If equality is available, then the "first-order" contextual
%%% equivalences can be stated in terms of it:

boolext== : (true P eqv true Q) -> pf (P == Q).
fext== : ({x:tm A} pf (S @ x == T @ x)) -> pf (S == T).
intax'== : pf ((\[x] int (lift x)) == (\[x] x)).
eta'== : pf ((\[x] \ (apply x)) == (\[x] x)).
xi'== : ({x:tm A} pf (F x == G x)) -> pf (\ F == \ G).
setext'== : ({x:tm A} true (P x) eqv true (Q x)) -> pf (\ P == \ Q).
wkintax== : pf (int (lift T) == T).
wketa== : pf (\ (apply T) == T).
wkbeta3== : pf (apply (\ F) T == F T).


%%% 9. Andrews-description
% See "General models, descriptions, and choice in type theory",
% Andrews, JSL 37(2):385--394, 1972.

the : (tm A -> tm o) -> tm A.

equal = [x] [y] x == y.
desc : {Ctx:(tm A -> tm A) -> jg}
        Ctx ([x] the (equal x)) eqv Ctx ([x] x).


%%% III. Andrews-description entails Watkins-description
%%% (in the presence of equality)

%abbrev
int~ : ((tm A -> tm o) -> tm o) -> tm A
  = [f] the [x] f ([y] y == x).
%abbrev
intax~ : {Ctx:(tm A -> tm A) -> jg}
        Ctx ([x] int~ (lift x)) eqv Ctx ([x] x)
  = [Ctx] desc Ctx.


%%% IV. Watkins-description is always available at o

%abbrev
into : ((tm o -> tm o) -> tm o) -> tm o
  = [f] f ([x] x).
%abbrev
intoax : {Ctx:(tm o -> tm o) -> jg}
        Ctx ([x] into (lift x)) eqv Ctx ([x] x)
  = [Ctx] eqvI.


%%% V. If Watkins-description is available at B it's available
%%%    at A --> B (assuming eta).

%abbrev
int--> : (((tm B -> tm o) -> tm o) -> tm B) ->
         (((tm (A --> B) -> tm o) -> tm o) -> tm (A --> B))
  = [i] [f] \[x] i ([p] f ([g] p (g @ x))).
%abbrev
int-->ax : ({Ctx:(tm B -> tm B) -> jg} Ctx ([x] I (lift x)) eqv Ctx ([x] x))
        -> ({Ctx:(tm (A --> B) -> tm (A --> B)) -> jg} Ctx ([x] int--> I (lift x)) eqv Ctx ([x] x))
  = [D] [Ctx] trans (D ([h] Ctx ([x] \[y] h (x @ y))))
                    (eta ([h] Ctx ([x] h x))).