Move the types into their respective function definition files

[sbp]

Coq defines its types in Numbers.BinNums which seems a little strange to me. It may be because they modularise [NPZ]Arith over so many files and they found that it's better to import the types into each file rather than do chained exporting.

On the other hand, in idris-bi we're keeping everything in the files Bip.idr, Bin.idr, and Biz.idr. It might be a good idea to move Bip into Bip.idr and so on. That way we would eliminate the Bi.idr file entirely. Who's really going to import Data.Bi without importing one of the other files?

[clayrat]

Yeah, makes sense.