why do you call the inhabitant of the unit type "the empty pair"? shouldn't it rather be "the empty tuple"? in my opinion, pairs always have two components and can not be empty.
