module exampleProductIntro where


record _×_  (A B : Set) : Set where 
  field
     first  : A
     second : B

postulate A : Set
postulate B : Set


f : A -> B -> A × B
f = \(a : A) -> \(b : B) 
     -> record{first = {! !};
               second = b}