[Agda] trustMe and make my coercion go

[Benja Fallenstein]

Hi Andreas,

On Wed, Sep 15, 2010 at 11:00 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> I have looked a bit at the theory of primTrustMe.  Actually it is a special
> case of eta-expansion for Leibniz-Equality.

Right, because the type checker checks the definitional equality
before reducing primTrustMe to refl, so you can't put refl into types
that don't contain it already -- e.g., in (\(q : Top == Bottom) ->
coerce (compute-dammit! q) unit), the coercion would not go, because
the primTrustMe would not reduce to refl. I guess that makes the
effect on the metatheory much less drastic...

> I have a (fairly theoretical) paper on this on my homepage, it was presented
> at the NBE'09 workshop.

Thanks, I'll have to try whether I can follow it :-)

> On Sep 15, 2010, at 9:56 PM, Benja Fallenstein wrote:
>> 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

No, I mean what the effect would be of introducing a constant with the
behavior of compute-dammit!, which could be implemented in Agda by the
definition I gave (i.e., through a module that exposes
compute-dammit!, but not primTrustMe).

Actually, with this context I'm not really sure what you mean by,

> Consistency holds rather directly, since each closed term of type a == a is refl anyway.

After all, if you introduce primTrustMe itself, true == false is inhabited, so:

resp : {X : Set} → (F : X → Set)
     → {x y : X} → x == y → F x ==₁ F y
resp f refl = refl₁

bad : ⊥
bad = coerce (resp (\b → if b then ⊤ else ⊥) (primTrustMe {Bool}
{true} {false})) unit

Could you elaborate a little there? :-)

Thanks again,
- Benja