record _@$\wedge$@_ (A B : Set) : Set where
  field
    p1 : A
    p2 : B