[Agda] Erasable vs. irrelevant

[Dan Doel]

On Thu, Jan 19, 2012 at 2:21 PM,  <jleivent at comcast.net> wrote:
> Thanks again, Andreas.
>
>> Unless you add an induction axiom (scheme) or at least case distinction,
>> there is no means of definition any function, like addition etc., hence,
>> no computational content in N.
>
> 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.

Your 'weak' discrimination isn't discriminating very interestingly.
What it says is that if suc n = zero, then N is trivial. So of course
it's compatible with a trivial model.

Also, the reason discrimination can't be derived from your rules (plus
the fact that Agda has universes)---which normally it can---is that
you have left out anything specifying the _computational behavior_ of
the induction term. These rules are:

    induction P z s 0       = z
    induction P z s (suc n) = s (induction P z s n)

If you add these to your specification, the trivial type is also no
longer a model (whether or not you also add in a real discrimination
axiom).

-- Dan