{-- powersets --}

Fam = \ S -> sig { I : Set, g : ( i : I )-> S }
    : ( S : Type )-> Type,

Pow = \ S -> ( s : S )-> Set
    : ( S : Type )-> Type,

{-- transition and interactive structures --}

Ts  = \ S -> ( s : S )-> Fam S
    : ( S : Type )-> Type,

Is  = \ S -> ( s : S )-> Fam (Fam S)
    : ( S : Type )-> Type,

{-- Martin-Löf's successor constructor --}

S   = \ A -> data { $0, $s ( a : A ) }
    : ( A : Set )-> Set,

{-- Von Neumann successor of a family --}

Vn  = \ AB ->
      let {
	A = AB.I
	  : Set,

	B = AB.g
	  : Pow A }
      in struct { I = S A, g = \ i -> case i of { $0   -> A, $s a -> B a } }
    : ( AB : Fam Set )-> Fam Set,

{-- W, WW, WWW --}

W   = \ A B -> data { $w ( a   : A, phi : ( b : B a )-> W A B ) }
    : ( A : Set, B : Pow A )-> Set,

WW  = \ A B c -> case c of { $w a phi -> W (B a) (\ s -> WW A B (phi s)) }
    : ( A : Set, B : Pow A, c : W A B )-> Set,

WWW = \ A B c cc ->
      case c of {
	$w a phi -> let {
		      F = \ b -> WW A B (phi b)
			: ( b : B a )-> Set }
		    in case cc of {
			 $w b psi -> struct {
				       I = F b,
				       g = \ i -> WW (B a) F (psi i) } } }
    : ( A  : Set, B  : Pow A, c  : W A B, cc : WW A B c )-> Fam Set,

WWWWWW0
    = \ AB ->
      let {
	A = AB.I
	  : Set,

	B = AB.g
	  : Pow A }
      in struct {
	   I = W A B,
	   g = \ t -> struct { I = WW A B t, g = WWW A B t } }
    : ( AB : Fam Set )-> Fam (Fam (Fam Set)),

WWWWWW
    = WWWWWW0
    : Is (Fam Set),

End = Set
    : Type