{-# OPTIONS --safe #-}

module EssentialAgda where

open import Prelude using (Type)
open import Data.Nat


record Pair (A B : Type) : Type where
  constructor ⦅_,_⦆
  field
    fst : A
    snd : B


p23 : Pair ℕ ℕ
p23 = record { fst = 2; snd = 3 }


p23' : Pair ℕ ℕ
p23' = ⦅ 2 , 3 ⦆


p24 : Pair ℕ ℕ
p24 = record p23 { snd = 4 }