[Agda] Container isomorphism?

[Edsko de Vries]

Hi Florent,

On Tue, Dec 7, 2010 at 6:06 PM, Florent Balestrieri <fyb at cs.nott.ac.uk> wrote:
>> I would like to prove that this is in fact "the same" as the container
>> type
>> cont ℕ (λ i → ⊤)
>
> I believe that what you want to prove is that the extension of both
> containers are isomorphic.

Yes.

> Unfortunately in your case, the extension of the container you gave is not
> isomorphic to Nat.
> You should use the empty type instead of the unit type for the positions.

Sorry, you are right; it didn't matter much in my case since I am
dealing with n-ary containers, and I specified this container to be
nullary; hence i has type Fin 0, so it doesn't matter what type I
return (there is a missing parameter n though; the exact statement I
would like to prove is:

cNat-simpl : forall {Xs} -> Ext cNat Xs ⇿ Ext (cont ℕ (λ i n -> ⊥)) Xs

where cNat is the container as computed from the universe:

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

> The interpretation of the elements of a container is defined as the
> extension of the container:
>
> Ext : Container -> Set -> Set
> Ext (cont S P) X = Sum S (\i -> P i -> X)
>
> For the container "N = cont Nat (const Empty)"
>
> You get "Ext N X = Sum Nat (const (Empty -> X))" which is isomorphic to Nat.
> (for all set X)

Yes, that would prove my "simple" container (cNat') isomorphic to Nat.
However, the container computed from the generic universe (cNat) uses
this representation for shapes:

(W (⊤ ⊎ ⊤) (PSum (λ s → ⊥) (λ _ → zero ≡ zero)))

so I believe that a proof that

cNat-simpl : forall {Xs} -> Ext cNat Xs ⇿ Ext (cont ℕ (λ i n -> ⊥)) Xs

would involve a proof that Nat is isomorphic (⇿) to its W
representation, above, which I don't think can be done without
extensionality?

Thanks,

Edsko