It occurred to me that as it is Christmas, we should make a holy
trinity:

   w, ww, www

  How should we type this?  Surely:

   w : Fam Set -> Set
   ww : (PI (A,B) : Fam Set) w(A,B) -> Set
   www : (PI (A,B) : Fam Set, t : w(A,B))ww(A,B) t -> Fam Set

General definitions:

>  Fam, Pow :: Type -> Type,
>  Fam A = (SIGMA I : Set)I -> A,
>  Pow A = A -> Set

>  fam : Fam Set -> Set -> Set
>  fam (A,B) S = (SIGMA a : A)B a -> S

--W--W--W--W--W--W--W--W--W--W--W--W--W--W--W--W--W--W--W--W--W--W

>  W : Fam Set -> Set
>  W (A,B) = mu S : S = fam (A,B) S

where mu stands for a fixed point operator.  
So we have:

>         W(A,B) = fam(A,B) (W(A,B))

I write W(A,B) or (W x : A)B x .

--WW--WW--WW--WW--WW--WW--WW--WW--WW--WW--WW--WW--WW--WW--WW--WW--WW

>  WW : (PI (A,B) : Fam Set) W(A,B) -> Set
>  WW (A,B) = mu (\ (a,phi) : W(A,B) -> = W (B a) (F . phi)

where `.' stands for function composition. 
So we have: 

>         WW(A,B) (a,phi) = (W x : B a) WW(A,B) (phi x)

  I write WW(A,B) :: W(A,B) -> Set, etc.

--WWW--WWW--WWW--WWW--WWW--WWW--WWW--WWW--WWW--WWW--WWW--WWW--WWW--WWW

What is WWW?  On aesthetic grounds (though I would prefer a recursive
definition):

>  WWW : (PI (A,B) : Fam Set, t : W(A,B)) WW(A,B) t -> Fam Set
>  WWW (A,B) (a,phi) (b,psi) 
>    = LET  F = WW (A,B) . phi :: B a -> Set
>      IN ( F b, WW (B a, F . psi ))
	
This is, of course, to indulge oneself in the formal seductions of 
notations.   Today is Xmas, and I am indulging myself.

What can we do with this monster?  In effect, it gives us a function
of type:

>  \(A,B)->(W(A,B), \t=(a,phi)->
>                   (WW(A,B), \t'=(b,psi)->WWW(A,B) t t'))
>  : Fam Set -> Fam^3 Set

In effect we have a `large' variant of a Petersson-Synek structure,
with base `set' the type of families of sets.  So to each family of
sets, we can attach the set of Petersson-Synek trees determined by
this structure.  This is surely an unimaginably closed forest of
trees!!