[Agda] Container isomorphism?

Thorsten Altenkirch txa at Cs.Nott.AC.UK
Tue Dec 7 20:46:29 CET 2010


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


More information about the Agda mailing list