[Agda] Container isomorphism?

[Edsko de Vries]

Hi,

I am playing a little with containers in Agda, and the translation of
the universe of strictly positive types into containers as described
in "Generic Programming with Dependent Types" by Altenkirch, McBride
and Morris. This translation generates some rather obfuscated
container types; for instance, the translation of the code in the
universe for natural numbers (μ (one ⊕ vl)) is

cont (W (⊤ ⊎ ⊤) (PSum (λ s → ⊥) (λ _ → zero ≡ zero)))
 (λ i →
    WPath (⊤ ⊎ ⊤) (PSum (λ s → ⊥) (λ _ → zero ≡ zero))
   (PSum (λ s → ⊥) (λ _ → suc i ≡ zero)))

I would like to prove that this is in fact "the same" as the container type

cont ℕ (λ i → ⊤)

which is certainly a lot more readable. However, what exactly does
"the same" mean? If we mean ⇿ from Function.Inverse, then we will not
be able to prove this because of (the lack of) extensionality. Is
there a notion of isomorphisms between containers that will allow me
to prove this, or will I need to add an extensionality axiom?

Thanks,

Edsko