module SigmaAsRecordModule (A : Set) (B : A → Set) where

open import Identity

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

record Σ : Set where
  constructor <_,_>
  field
    l1 : A
    l2 : B l1

-- and we then we can write _×_.l1  _×_.l2 for the projections (cf fst and snd):

fst : Σ -> A
fst = Σ.l1 

snd : (c : Σ) -> B (fst c)
snd = Σ.l2

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

surjective-pairing : (c : Σ) → < fst c , snd c > ≡ c
surjective-pairing c = refl

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