[Agda] Container isomorphism?

[Edsko de Vries]

Hi Andreas,

On Tue, Dec 7, 2010 at 5:49 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 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.

Thanks for the suggestion; however, if I understood

http://www.e-pig.org/epilogue/?p=324

correctly, then I will again get stuck because of lack of
extensionality if I try that..

Edsko

>
> 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
>>
>