[Agda] explicit irrelevance question

[Sergei Meshveliani]

Thanks to people!
My last attempt was   ... | no x/=0 = irrel-f x x≉0 x/=0

But I needed to guess to transpose the pair  x≉0 x/=0
!
(the checker even reports a certain hint about this, I needed to look
into the report more closely).

Regards,

------
Sergei



On Mon, 2014-10-20 at 00:39 +0300, Andreas Abel wrote:
> Sergei, I managed to finish your proof using irrel-f (see below).
> 
> On 19.10.2014 19:06, Sergei Meshveliani wrote:
> > --------------------------------------------------------------
> > open import Level            using (_⊔_)
> > open import Function         using (case_of_)
> > open import Relation.Nullary using (Dec; yes; no; ¬_)
> > open import Relation.Binary  using (module IsEquivalence;
> >                                      module DecSetoid; DecSetoid)
> > open import Relation.Binary.PropositionalEquality as PE using (_≡_)
> > open import Data.Empty using (⊥-elim)
> >
> >
> > module _ {α α=} (A : DecSetoid α α=) (0# : DecSetoid.Carrier A)
> >    where
> >    open DecSetoid A using (_≈_; _≟_; isEquivalence)
> >                                      renaming (Carrier to C)
> >    open IsEquivalence isEquivalence renaming (refl to ≈refl)
> >
> >    record Foo : Set (α ⊔ α=)
> >      where
> >      field f       : (x : C) → ¬ x ≈ 0# → C
> >            irrel-f : (x : C) → (nz nz' : ¬ x ≈ 0#) → f x nz ≈ f x nz'
> >
> >      g : C → C
> >      g x  with x ≟ 0#
> >      ...             | yes _  = x
> >      ...             | no x≉0 = f x x≉0
> >
> >      g=f-if : ∀ x → (x≉0 : ¬ x ≈ 0#) → g x ≈ f x x≉0
> >      g=f-if x x≉0  with x ≟ 0#
> >      ...                      | yes x=0 = ⊥-elim (x≉0 x=0)
> >      ...                      | no x/=0 = ≈refl
> >                                           -- ?
> > -----------------------------------------------------------------
>      ...                      | no x/=0 = irrel-f x x/=0 x≉0
> 
>