Proving binary string bijection with naturals in agda

Here’s (github.com/siers/agda-plfa) my solution to the exercise «Bin-predicates (stretch)» from the PLFA book’s «Relations» chapter which proves that the binary string ADT and the conversions defined as to and from do indeed form an bijection (isomorphism) with the naturals.