[Agda] Container isomorphism?

[Thorsten Altenkirch]

On 7 Dec 2010, at 17:08, 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 haven't checked the details but I suspect that this is easily seen to be isomorphic to the usual representation of ℕ using W-types 

W Bool (\ x -> if x then ⊤ else ⊥)

with some extra noise due to dealing with the representation of variables.

> 
> I would like to prove that this is in fact "the same" as the container type
> 
> cont ℕ (λ i → ⊤)

Here, I hope you mean a nullary container, whose extension is of type 1 -> Set and hence which is isomorphic to ℕ.

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

You will certainly need extensionality to show that any representation of the natural numbers using W types is isomorphic to the natural numbers. Basically you can't prove anything interesting about functions without extensionality (as you can't prove anything interesting about the natural numbers without induction).

Thorsten