[Agda] Nat -iso- Bin

[Sergei Meshveliani]

On Tue, 2013-10-29 at 23:21 +0400, Sergei Meshveliani wrote:
> Correction:  ``{m : ℕ} → ''  
> is not needed here.
> 
> Also there is a question about availability of  fromℕ ∘ toℕ ≗ id,
> fromDigits ∘ toDs ≗ id.
> 
> 
> On Tue, 2013-10-29 at 22:51 +0400, Sergei Meshveliani wrote:
> > Please, has  lib-0.7  something for the isomorphism  ℕ <-> Bin ?
> > 
> > For example, I need 
> > 
> >   toDigits-suc-eq : {m : ℕ} → 
> >                     let toDs : ℕ → Bin⁺
> >                         toDs = proj₁ ∘ toDigits 2                    
> >                     in 
> >                     toDs ∘ suc ≗ (addCarryToBitList 1b ∘ toDs) 
> > 
> > Probably,      fromℕ ∘ suc ≗ Bin.suc ∘ fromℕ 
> > will also do.
> > 
> > I think of proving  toDigits-suc-eq,  but this needs looking into a
> > non-trivial definition of  toDigits.
> > 

I hope now that 

  bs → fromDigits (addCarryToBitList 1b bs) \equiv (suc (fromDigits bs))

is not difficult to prove -- because  fromDigits  is simpler than
toDigits.
I hope that then, the proof part  pr  in  toDigits m  will help with the
proof for  toDigits-suc-eq.

On the other hand, something needs to be in Standard library that easily
gives the  suc (or _+_) isomorphism for  Nat <--> Bin, Bin⁺.
Am I missing something?

Regards,

------
Sergei