using NoStdLib

fst : (a × b) → a
fst (a,_) = a

snd : (a × b) → b
snd (_,b) = b