[Agda] trustMe and make my coercion go

[Andreas Abel]

Hi Benja,

I have looked a bit at the theory of primTrustMe.  Actually it is a  
special case of eta-expansion for Leibniz-Equality.

If you replace each term t of type a == a  (for arbitrary a) by refl,  
then primTrustMe is just the identity.
In your example

   coerce foo zero = coerce refl zero = zero

since foo : Nat == Nat.

I have a (fairly theoretical) paper on this on my homepage, it was  
presented at the NBE'09 workshop.  In this paper I show  
normalization.  However, I have only covered a small part of Agda, the  
logical framework bit.  To extend it to a reasonable subset of Agda,  
like data and universes, seems not trivial.

Consistency holds rather directly, since each closed term of type a ==  
a is refl anyway.  Normalization is harder, but I believe it holds.   
There is related work on proof irrelevance by Benjamin Werner (see his  
2008 LMCS paper).  However, I think I have found a gap in the  
normalization proof that is presented there.

On Sep 15, 2010, at 9:56 PM, Benja Fallenstein wrote:
> It occurs to me that the function
>
>> compute-dammit! : {X : Set} → {x y : X} → x == y → x == y
>> compute-dammit! _ = primTrustMe
>
> could be used to make stuck coercions go -- contrived example:
>
>> postulate foo : Nat == Nat
>>
>> test : coerce (compute-dammit! foo) zero == zero
>> test = refl
>
> (I'm using --type-in-type there because Agda doesn't let me use
> primTrustMe on higher levels, but that seems like a detail.)
>
> Now I'm wondering what effect introducing compute-dammit!

Maybe you mean primTrustMe?  compute-dammit! is just a definition so  
it does not change the metatheory.

> would have
> on the metatheory: Does it destroy normalization? Consistency? It
> seems like consistency should be preserved, because in a
> set-theoretical model, compute-dammit! should just be the identity,
> right?
>
> Thanks,
> - Benja

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/