module Data.Tuple where data _×_ (A B : Set) : Set where <_,_> : A -> B -> A × B fst : {A B : Set} -> A × B -> A fst < x , y > = x snd : {A B : Set} -> A × B -> B snd < x , y > = y