[Agda] Irrelevance and propositional equality

[Andreas Abel]

Hi Alan,

Well, for one, any use of trustMe does not destroy the termination 
property, so you should not be able to write programs that make the type 
checker loop (at least the ideal bug-free implementation of Agda ;-)).

Also, your use of trustMe does not endanger consistency, because any 
closed proof of a == b is refl, hence, requiring a to be identical to b. 
  It does not matter that your proof is irrelevant here.  So, there is 
still no closed proof of 1 == 0 possible with your use of trustMe.

So, I think your foot is safe. ;-)

Actually, this looks like a nice combination of experimental features...

Cheers,
Andreas


On 7/20/11 4:23 PM, Alan Jeffrey wrote:
> I'm currently working on some code where life is remarkably easier if I
> make use of a function which promotes irrelevant propositional
> equalities to relevant ones:
>
> ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
> ≡-relevant a≡b = trustMe
>
> Of course, life would also be remarkably easier if I were to postulate
> false. Am I shooting myself in the foot here?
>
> A.
>

-- 
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/