%% Not yet the Return of the Kind
%% the towers of 2K from [Urzyczyn, MSCS 1997, p.11]
%% Author: Andreas Abel

%% Fix some type B.

type B    : * ;

%% Pointed types

type P0   : (* -> *) -> *
          = \F:(*->*) forall X:*. X -> F X; 

%% K-combinator: first projection

type K    : * -> *
          = \A:*. B -> A;

term k    : P0 K 
          = \\A:* \a:A \b:B. a;

%% Church numeral 2 on the first level

type P1   : ((* -> *) -> * -> *) -> *
          = \F:((*->*)->(*->*)) forall X:(*->*). P0 X -> P0 (F X);

type Two0 : (* -> *) -> * -> *
          = \F:(*->*) \X:*. F (F X) ;

term two0 : P1 Two0
          = \\F:(*->*) \f:(P0 F) \\X:* \x:X.
            f[F X] (f[X] x);

%% The tower of height 1: 2 K

term t1k  : P0 (Two0 K) % forall A:*. A -> Two0 K A
          = two0[K] k;

%% The Church numeral 2 on the second level

type P2   : (((*->*)->*->*)->((*->*)->*->*)) -> *
          = \F:(((*->*)->(*->*))->((*->*)->(*->*))) 
          forall X:((*->*)->(*->*)). P1 X -> P1 (F X);

type Two1 : ((* -> *) -> * -> *) -> (* -> *) -> * -> *
          = \F:((* -> *) -> * -> *) \X:(* -> *). F (F X) ;

term two1 : P2 Two1
          = \\F1:((*->*)->*->*) \f:(P1 F1)
            \\F0:(*->*)         \x:(P0 F0).
            f[F1 F0] (f[F0] x);

% The tower of height 2: 2 2 K

term t2k  : P0 (Two1 Two0 K)
          = (two1[Two0] two0)[K] k;
 
%% The Church numeral 2 on the third level

type P3   : ((((*->*)->*->*)->((*->*)->*->*)) -> 
             (((*->*)->*->*)->((*->*)->*->*))) -> *
          = \F:((((*->*)->(*->*))->((*->*)->(*->*))) -> 
		(((*->*)->(*->*))->((*->*)->(*->*))))
          forall X:(((*->*)->(*->*))->((*->*)->(*->*))). P2 X -> P2 (F X);

type Two2 :(((*->*)->*->*)->(*->*)->*->*)->
            ((*->*)->*->*)->(*->*)->*->*
          = \F:(((*->*)->*->*)->(*->*)->*->*) 
            \X:((*->*)->*->*). F (F X) ;

term two2 : P3 Two2
          = \\F2:(((*->*)->*->*)->((*->*)->*->*)) \f:(P2 F2)
            \\F1:((*->*)->*->*)                   \x:(P1 F1).
            f[F2 F1] (f[F1] x);

% The tower of height 3: 2 2 2 K

term t3k  : P0 (Two2 Two1 Two0 K)
          = ((two2[Two1] two1)[Two0] two0)[K] k;
 
%% The Church numeral 2 on the fourth level

type P4   : (((((*->*)->*->*)->(*->*)->*->*) ->
               ((*->*)->*->*)->(*->*)->*->*) ->  
             ((((*->*)->*->*)->(*->*)->*->*) ->
               ((*->*)->*->*)->(*->*)->*->*)) -> *
          = \F:(((((*->*)->*->*)->(*->*)->*->*) ->
               ((*->*)->*->*)->(*->*)->*->*) ->  
             ((((*->*)->*->*)->(*->*)->*->*) ->
               ((*->*)->*->*)->(*->*)->*->*))
	    forall X: ((((*->*)->(*->*))->((*->*)->(*->*))) -> 
		       (((*->*)->(*->*))->((*->*)->(*->*)))).
            P3 X -> P3 (F X);

type Two3 : ((((*->*)->*->*)->(*->*)->*->*) ->
              ((*->*)->*->*)->(*->*)->*->*) ->  
             (((*->*)->*->*)->(*->*)->*->*) ->
              ((*->*)->*->*)->(*->*)->*->*
          = \F:((((*->*)->*->*)->(*->*)->*->*) ->
                (((*->*)->*->*)->(*->*)->*->*))
            \X:(((*->*)->*->*)->((*->*)->*->*)). F (F X) ;

term two3 : P4 Two3
          = \\F3:((((*->*)->*->*)->((*->*)->*->*))->
                  (((*->*)->*->*)->((*->*)->*->*)))
            \f:(P3 F3) 
            \\F2:(((*->*)->*->*)->((*->*)->*->*))
            \x:(P2 F2).
            f[F3 F2] (f[F2] x);

% The tower of height 4: 2 2 2 2 K

term t4k  : P0 (Two3 Two2 Two1 Two0 K)
          = (((two3[Two2] two2)[Two1] two1)[Two0] two0)[K] k;

% Please do not generalize further