module ProductAsRecord where -- Labelled records, Figure 11-7 in Pierce, are tuples with named components record _×_ (A B : Set) : Set where field l1 : A l2 : B -- A ×' B is like A × B but with labels l1 and l2. (Recall also that we have "surjective pairing" for records, cf lecture) -- Instead of < a , b > we write <_,_> : {A B : Set} -> A -> B -> A × B < a , b > = record { l2 = b ; l1 = a } -- and we then we can write _×_.l1 _×_.l2 for the projections (cf fst and snd): fst : {A B : Set} -> A × B -> A fst = _×_.l1 snd : {A B : Set} -> A × B -> B snd = _×_.l2