[Agda] Re: [Coq-Club] Re: Universe Polymorphism

[Jean-Philippe Bernardy]

On Thu, Sep 16, 2010 at 8:28 PM, Dan Doel <dan.doel at gmail.com> wrote:
> (I'm copying the Agda list with this, since the conversation may be of
> interest there, too.)

Indeed, thanks.

> Including extending the erasure/irrelevance stuff to inductive types,
> erasability analysis (which may or may not be what you asked for later in your
> mail), and thoughts on proof irrelevance (although, I'm personally not
> convinced that this sort of erasability captures that notion precisely).

Can I ask you to elaborate on why you think that erasability does not
mean irrelevance? I happen to have the opposite belief:

proof irrelevance = structure of the proof irrelevant in the
computational interpretation


>> - PTS rules can be used to forbid your embed function, if you put
>> Level outside of the Set tower.
>> If TLevel is the sort of Level, then just do not add rules like (Set
>> i, Level, Level).

Thank you Andreas :)

> Yeah, that's true. The theme of the EPTS papers/thesis, though, is that
> irrelevance/erasability/parametricity should not (necessarily) be intrinsic to
> types; it should be based on use.

To make sure, even in Coq, Props are NOT intrinsically relevant. Consider

f : Prop -> Prop

the argument of 'f' is not relevant in its result. The irrelevance is
only wrt. Set.

> So, I thought it would be similarly nice if
> one could make universe polymorphism always parametric while not making any
> types intrinsically irrelevant.

Why would that be? The intention for Levels is that they are /always/
irrelevant with
respect to programs.

Cheers,
JP.