postulate A:: Type 
postulate B:: Type 

AB :: Type
   = sig{a :: A;
         b :: B}


f :: A -> B -> AB
  = \(a'::A) -> \(b'::B) -> struct {
                              a = a';
                              b = b';}