module SigmaAsRecord where

open import Identity

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

record Σ (A : Set) (B : A → Set) : 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 : Set} → {B : A → Set} → Σ A B -> A
fst = Σ.l1 

snd : {A : Set} → {B : A → Set} → (c : Σ A B) -> B (fst c)
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!