postulate A :: Set
postulate B :: Set
postulate C :: Set
postulate D :: Set

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

CD :: Set
   = sig{c :: C; d :: D;}

f (a_c:: A->C)
  (b_d:: B->D)
  (ab:: AB)
  :: CD
  = let a:: A = ab.a
        b:: B = ab.b
        c'::C = a_c a
        d'::D = b_d b
    in  struct{c = c';d = d';}