[Agda] Trust me regarding Dan Licata's trick

[Martin Escardo]

On 10/06/13 10:06, Nils Anders Danielsson wrote:
> On 2013-06-07 10:42, Martin Escardo wrote:
>> Anyway, if trustMe does work as a postulate as claimed earlier, why is
>> it needed/useful at all?
>
> Dan Licata gave an explanation earlier in this thread.

Which I didn't fully understand, but never mind.

Now I am convinced that trustMe can't do what I want, and that moreover 
it doesn't make sense to have all elements of the hpropositional 
truncation to be definitionally equal, for the following reason:

Using Dan's trick without trustMe but instead with a postulate

postulate truncation-is-hprop : {X : Set} -> hprop || X ||

we get hpropositional truncation so that the non-dependent elimination 
rule holds definitionally:

truncation-rec : {X P : Set} -> hprop P -> (X -> P) -> (|| X || -> P)
truncation-rec _ f | x | = f x

(The dependent elimination rule truncation-ind also holds 
definitionally, but we don't need it.)

Using this, we can prove

hset-funext : {X : Set} {Y : X -> Set} -> ((x : X) -> hset(Y x)) ->
        (f g : (x : X) -> Y x) -> (∀(x : X) -> f x == g x) -> f == g

where == is propositional equality and hset means that any two proofs of 
equality are equal (i.e. UIP).

http://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/hsetfunext.html

If, moreover, we had that |x|=|x'| held definitionally in ||X|| for all 
x,x':X, with the above proof we would get that any two hset-valued, 
pointwise equal functions would be definitionally equal, which is 
non-sense. Additionally, trustMe would break, and presumably SegFault, 
if we used it to replace the postulate, precisely at the point when we 
tried to use a proof of equality of two functions obtained from 
hset-funext.

So don't trustMe regarding Dan's trick.

In any case, the above says that implementing hpropositional truncation 
in intensional type theory so that canonicity is not lost is at least as 
hard as implementing the axiom of function extensionality for 
hset-valued functions. Something naive such as trustMe won't work.

Best,
Martin