[Agda] Proof irrelevance and self-realizing formulas

[wren ng thornton]

Thorsten Altenkirch wrote:
> Hi Andrej,
> 
> > Let us temporarily forget the interpretation
> >
> > "P is proof irrelevant" = "all proofs of P are equal"
> >
> > because we don't like equality of proofs.
> 
> Why?

I believe that's a presupposition: people who care about 
proof-irrelevance are people who don't like equality of proofs.

At least that's the case for all the discussions I've seen on the topic. 
The need to discuss or determine (in)equality between different proofs 
of the same theorem can lead to difficulties. The desire for 
proof-irrelevance is the desire to escape those difficulties, which 
means finding some way of abandoning proof equality.


> > An alternative
> > interpretation of "P is proof irrelevant" is:
> >
> > "Anything that can be computed using a proof p : P, can also be
> > computed without it."
> >
> > The extreme case of this is that an inhabitant of P can be computed
> > without using p, i.e., an inhabitant of P can be constructed out of
> > thin air, provided P has inhabitants.
> 
> How do we explain that we are using the fact that p has inhabitants w.o. 
> looking at them?
> 
> I mean this is exactly what is achieved by saying P has at most one 
> proof, hence there is no information in knowing that proof.

That's the idea. The difficulties mentioned above happen because we *do* 
have information in knowing the proof, but we don't want it (we only 
want to know *that* P is inhabited, without knowing how or by what). 
Proof-irrelevance is a way of erasing that information, which in turn 
erases a lot of fiddly details.

-- 
Live well,
~wren