[Agda] Container isomorphism?

[Andreas Abel]

My comments does not have much to do with containers, but if you want to 
show that a set is isomorphic to the natural numbers you could show that 
it has the zero, the successor, and the induction principle for natural 
numbers.

Cheers,
Andreas

On 12/7/10 6:08 PM, Edsko de Vries wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>