[Agda] trustMe and make my coercion go

[Benja Fallenstein]

Hi Andreas,

On Thu, Sep 16, 2010 at 5:18 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> In my remarks about consistency and normalization I had eta-equality for
> Leibniz equality in mind (where primTrustMe is not needed).  In this
> context, you would have postulates instead of primTrustMe, so having
>
>  p : true == false
>  p = primTrustMe
>
> is the same as
>
>  postulate p : true == false

Thanks for the reply, I think I now understand your first message
better, too! :-) So with eta equality for _==_, compute-dammit! is not
needed, because the coercions it gets unstuck aren't stuck in the
first place. If (p q : x == y), and x definitionally equals y, then p
def. equals q def. equals refl; and (looking at the "making Agda see
more" slides, which I'd looked at earlier but still haven't fully
assimilated), if x does not def. equal y, then p def. equals q def.
equals *. Nice.

Thanks,
- Benja