[Agda] using irrelevant field

[Sergei Meshveliani]

This is about "converting an irrelevant value to relevant".

On Tue, 2014-03-18 at 14:37 +0100, Andreas Abel wrote:
> The example is rejected since the proof x/=0 is irrelevant in 
> (subEl x x/=0), but f expects it to be relevant.
> 
> The fix 2. is correct.
> 
> The other way to fix it is of course to just drop the second argument to 
> f, since it is unused anyway.
> 
> Probably your example is too simplistic, you want to do something more 
> advanced with irrelevance!?


Yes.

(1) Most function _condition_ arguments in any mathematical library need
to be irrelevant.  

(2) It is desirable 
   a) to include irrelevant things to the language standard,
   b) to use irrelevant things in Standard library.

(3) My DoCon-A library currently uses irrelevant things, but not
everywhere, so far (I fear of possible complications).

The approach (3) causes that sometimes I need to convert a thing to
relevant.
Here is a contrived example:

--------------------------------------------------------------------
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
open import Data.Product using (_,_; Σ)
open import Data.Nat     using (ℕ; suc)

record Nonzero : Set where  constructor subEl
                            field  elem   : ℕ
                                   .proof : elem ≢ 0
Nonzero' : Set
Nonzero' = Σ ℕ (\x → x ≢ 0)  -- relevant version  

suc≢0 : ∀ {n} → suc n ≢ 0
suc≢0 {suc n} ()
suc≢0 {0}     ()

nz' : Nonzero'               -- example of using Nonzero'
nz' = (1 , suc≢0)

toRelevant : Nonzero → Nonzero'
toRelevant (subEl x x≢0) =  (x , x≢0)
--------------------------------------------------------------------

It is not type-checked.

So far, I agree `relevant' and `irrelevant' parts this way:
in the intersection I change a relevant argument in a signature to
irrelevant. And repeat this by transitivity until the checker is
satisfied. 
(In this approach, Nonzero' needs to be removed). 

Is there possible another way to agree the `relevant' and `irrelevant'
parts?
In particular, what to do with the above example?

Thanks,

------
Sergei