module ProductAsRecord where

open import Identity

-- Labelled records, Figure 11-7 in Pierce, are tuples with named components

record _×_ (A B : Set) : Set where
  constructor <_,_>
  field
    l1 : A
    l2 : B

{- The constructor could have been defined as

<_,_> : {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

-- When we define pairs with records we have "surjective pairing", that is, the law

surjective-pairing : ∀ {A} {B} → (c : A × B) → < fst c , snd c > ≡ c
surjective-pairing c = refl

-- We do not have this law when defining pairs with data. Try it!