Heinlein question -- "Gulf" & "Friday" (open spoilers)

[BrainGlutton]

@MIchelleRose

Definitions: dolphins are fish, coryphaenidae, like the pompano. Porpoises are the mammals we know as bottlenose dolphins. The two terms are often mixed, much to the grief of marine biologists. I know a couple and they always frown when I use the term “dolphin” to describe tursiops truncatus. Bad form, doncha know.

Actually, AIUI, there are porpoises and there are also mammalian dolphins, two different groups of species.