\(a : *)
->  \(b : *)

->  type Prod2

    data Make (_1 : a) (_2 : b)

    in   Prod2