[Agda] explicit irrelevance question

[Andreas Abel]

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


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/