[Agda] Irrelevance and equalities?

[Nicolas Pouillard]

Hi,

On Thu, 31 Mar 2011 08:28:20 +0200, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 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.

I came across the same issue recently and made a new use of the following type:

record Irr {a} (A : Set a) : Set a where
  constructor irr
  field
    .cert : A

open Irr public

This type already appeared multiple times here with various names...

Then the code becomes:

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

In short having Irr in the standard library and documenting this idiom would
be nicer than many launder functions and/or having "with ." clauses.

All the best,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr