Start sketching CBPV implementation in Scala

Not to merge yet. Agda is more suited to prototyping this code, thanks to totality checking.