[Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)

[Dan Licata]

Hi Conor,

On Mar25, Conor McBride wrote:
> Indeed (1) is what I had in mind. Please do bear in mind that
> (2) is not so far from (1). Consider
> 
> foo : true == true -> true == true
> foo x = ?
> 
> moo : foo == id
> moo = ?
> 
> How you fill in the foo hole will determine *whether* you can
> fill in the moo hole.

That's only because ==/Refl is the wrong notion of propositional
equality for negative types, though.  Which is a valid complaint given
that I was asking about adding a feature to agda today.  But with the
right notion of propositional equality, making the "wrong"
propositionally equal choice during inference would never change
provability, I think.

> >> In the Epigram 2 core, we've done
> >>it by separating Prop and Set explicitly, as a
> >>universe a la Tarski with an explicit decoder
> >>
> >>  Prf : Prop -> Set
> >
> >Actually, I'm curious about this setup.  Does Prop only give codes for
> >Sets that already have 0 or 1 inhabitants,

Thanks for the detailed reply!  These insights into the design of
epigram are always interesting and enlightening.  I think I understand
what's going on a little better now.

One high-level question:

> A key design criterion is to ensure that proofs are
> really erasable at run time. 

Is there a reason irrelevance should be related to erasability?
Irrelevance isn't a necessary condition for erasability (e.g., if you
have a Vec and you don't compute with the length, you might erase it,
but you don't want the Vec to be indexed by an irrelevant Nat!).

And an example like 

 (X : Set) -> ((x y : X) -> x == y) -> Squash X -> X

shows that you might want an irrelevant type (all elements of Squash X
are definitionally equal) that is not erasable (just because they're all
equal, doesn't mean I can come up with one out of thin air).

So why bundle the two concepts together?  I believe that it's a useful
thing to do, because you

> get away with a remarkably liberal property:
> 
>   Consistent propositional postulates preserve canonicity
>   of closed computation in sets.

which gives you the freedom to add whatever axioms you want to Prf,
without giving them computational behavior.  

But is there a deeper reason why irrelevance (there is at most one term
of a type definitionally) and erasability (not needing to pass the
term at run-time) are intertwined?  This aspect of prop/set distinctions
has always puzzled me.

-Dan