Species of Types are extensional [008R]

The identity type of species is equivalent to the type of equivalences between them. This is immediate by function extensionality