[Agda] Irrelevance and equalities?

[Andreas Abel]

Hi Brandon,

On 30.03.11 3:58 AM, Brandon Moore wrote:
> Might it be nice to define Dec like
>
> data AltDec (P : Set) : Set where
>    yes : P → AltDec P
>    no : .(P → ⊥) → AltDec P
> Then it can be proven that
>
> mutual
>    lemm : {P : Set}(p-uniq : (x y : P) → x ≡ y) → (p q : AltDec P) → p ≡ q
>    lemm p-uniq (yes a) (yes b) rewrite p-uniq a b = refl
>    lemm _ (yes p) (no ¬p) with launder (¬p p); ... | ()
>    lemm _ (no ¬p) (yes p) with launder (¬p p); ... | ()
>    lemm _ (no _) (no _) = refl
>
>    launder : .⊥ → ⊥
>    launder ()
>
> Is there a reason to avoid this, besides irrelevance being
> somewhat new and experimental? Should the with-clause
> work without introducing the "launder" function?

I think if you replace the "with" by a manual auxiliary function, you 
can avoid launder.  Unfortunately, current "with" does not create an 
auxiliary function with irrelevant arguments.  But (\notp p) is only 
welltyped in irrelevant position.

One could think of adding a syntax for irrelevant "with" clauses, e.g.

   lemm _ (yes p) (no ¬p) with .(¬p p); ... | ()

The dot "." allows then irrelevant with-abstraction.

Or "launder" could be part of the standard library, but this is probably 
not a good idea, since there are so many empty types, not just \bot.

Cheers,
Andreas

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