[Agda] Erasable vs. irrelevant

[Adam Gundry]

Hi Jonathan,

On 19/01/12 19:21, jleivent at comcast.net wrote:
> See the enclosed module.  So, even with induction and cases, it still
> looks to me like it is erasable - or, as you say, that there is no
> computational content in N.  It is surprising to me that so much
> about the naturals could be devoid of computational content.  I have
> a hard time believing that this is correct - but I don't see anything
> wrong with it.

The only thing wrong with it is that you haven't axiomatised the natural
numbers. You have this:

> record N-Erasable : Set₁ where
>   field
>     N         : Set
>     Ø         : N
>     1+        : N → N
>     1+inject  : ∀{n₁ n₂ : N} → 1+ n₁ ≡ 1+ n₂ → n₁ ≡ n₂
>     Ø1+choice : ∀(n : N) → n ≡ Ø ⊎ ∃ λ n' → n ≡ 1+ n'
>     induction : ∀(P : N → Set) → P Ø → (∀{n : N} → P n → P (1+ n)) → ∀(n' : N) → P n'
>     weak-disc : ∀{n : N} → 1+ n ≡ Ø → ∀(n₁ n₂ : N) → n₁ ≡ n₂

which is modelled by the unit type, as you demonstrate. But you are
missing an axiom to say that one is not equal to zero:

disc : {n : N} → 1+ n ≡ Ø → ⊥

With this axiom (even though it has no "computational content" in some
sense), the unit type is no longer a model. Your weak-disc is too weak,
precisely because it is satisfied by the unit type as well as the naturals.

Hope this helps,

Adam