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

[Dan Doel]

On Sunday 19 September 2010 10:13:04 am Jean-Philippe Bernardy wrote:
> On Fri, Sep 17, 2010 at 9:28 AM, Dan Doel <dan.doel at gmail.com> wrote:
> >  subst : (A : Set) => (P : A -> Set) => (x y : A) => x == y -> P x -> P y
> 
> To me subst should live in the area of Propositions:
> 
> subst : (A : Set) -> (P : A -> Prop) -> (x y : A) -> x == y -> P x -> P y
> 
> In that case there is no issue of relevance (the target is in Prop).
> 
> You may want a "converter" though:
> >  conv : (A : Prop) -> (P : A -> Set) -> (x y : A) -> x == y -> P x -> P y
> 
> (_==_ is in Prop)
> 
> In that case I believe that there is no issue of parametricity;
> because P is "irrelevant" in A.

The first of these is (in a sense) a special case of the type I gave. The 
thesis takes 'propositions' to be elements of the squash type:

  data Sq (A : Set) : Set where
    sq : A => Sq A

which has eliminator:

  elimSq : (A : Set) => (P : Sq A -> Set) =>
           ((x : A) => P (sq x)) -> (s : Sq A) -> P s

Using this, and the type for subst I gave above, one can write:

  -- Note that the proof of x == y is irrelevant
  subst' : (A : Set) => (P : A -> Set) => (x y : A) => x == y =>
           Sq (P x) -> Sq (P y)
  subst' A P x y s = elimSq (P x) (Sq (P y))
                            (\Px -> sq (subst A P x y eq Px)) s

The second cannot be written (in the basic EPTS), I think, but I'm not certain 
why you'd want it.

> And, yes, you can have:
> 
> data Nat : Prop where
>   ...
> 
> data Vec (A : Set) : Nat -> Set where
>  ...
> 
> (Because Vec does not analyse Nat indices)

I don't think I believe this explanation given your explanation of the conv 
type. The reason conv was safe was that P itself was irrelevant in its Prop 
parameter, which I presume means that P x is the same type regardless of what 
x is. This is what having P : Sq A -> Set or P : A => Set would accomplish in 
an EPTS, too.

Given the above, and the extended 'proof irrelevant' rules for EPTS, it might 
even be possible to write conv, because it would sort of erase down to:

  conv : (A : Set) => (P : A => Set) => (x y : A) => x == y => P -> P

with x and y erased from the last two bits, because they don't matter. In 
fact, if we switch to squashes:

  conv' : (A : Set) => (P : Sq A -> Set) => (x y : Sq A) => x == y =>
          P x -> P y

Then the proof irrelevant rules should give us that all elements of Sq A are 
equal, so we should just be able to make up a value of x == y even though we 
aren't allowed to look at the one that was passed in (although, working it 
out, it looks like it would require x and y to be relevant *).

But, Vec A n is not the same type regardless of what n is. Vec A 0 has a 
single value [], while Vec A 1 has one value [x] for each value x : A. And:

> So, you can use conv to convert from Vec m to Vec n if m == n.

this is suspect given the rules for proof irrelevant equality: if this Nat : 
Prop is analogous to Sq Nat in an EPTS, then all elements of it are equal. But 
this would be bad, because if 5 == 7 via proof irrelevence, we should be able 
to cast from Vec A 5 to Vec A 7, which isn't what we'd expect.

> My point is the following: the chief benefit of the EPTS is to avoid
> duplication of code
> in Prop/Set. There is a time-tried solution to avoid duplication:
> parametrization. In this instance,
> it means to extend universe polymorphism to parameterize also on the
> "relevant/irrelevant" aspect.
> I believe that this solution is to be attempted before adding
> seemingly ad-hoc constructs.

I don't see what is ad-hoc about EPTS. They are related to modal logics via 
Curry-Howard. And reasoning about "this is around in one phase, but not in a 
later phase" is one sort of thing modal logics are used for.

One might equally argue that tying the erasability of terms to their type 
(which even a parameterized Prop/Set distinction does) is ad-hoc. For 
instance, suppose we have x : Nat : Set, and we need to fill a hole that 
expects a Nat : Prop. An EPTS would allow this due to the modal rules (in 
modal logic, you'd get P -> <>P). What do we do in a type-based solution? 
Introduce a subtyping relation, Nat : Set < Nat : Prop? Or is this just not 
allowed?

> Thanks for you thoughtful answer!

No problem. I'm pretty interested in this stuff.

-- Dan

[*] Proof that all elements of Sq A are equal, given the proof irrelevant CONV 
rule in the thesis:

lemma : (A : Set) => (sx sy : Sq A) -> sx == sy
lemma A sx sy = elim A (\sz -> sx == sz)
                       (/\y -> elim A (\sz -> sz == sq y)
                                      (/\x -> ?)
                                      sx) 
                       sy

? : sq x == sq y = refl, by proof irrelevance.

If the eliminator were parametric in the Sq A terms, it would be exactly what 
we want above, but allowing that is questionable.