[Agda] Help with With-permutations.

[Apostolis Xekoukoulotakis]

Hello, I have something similar to the below :

```
open import Relation.Binary.PropositionalEquality

data A : Set where
  a1 : A
  a2 : A



fun : A → A
fun a1 = a2
fun a2 = a1

bun : A → A
bun a1 = a2
bun a2 = a1

cun : A → A
cun a with fun a
cun a | a1 = a1
cun a | a2 = a1

gun : (a : A) → cun a ≡ a1 → A
gun a c with fun a
gun a c | a1 with bun a
gun a c | a1 | a1 = a1
gun a c | a1 | a2 = a1
gun a c | a2 = a1

dun : (a : A) → cun a ≡ a1 → A
dun a c with bun a
dun a c | a1 with fun a
dun a c | a1 | a1 = a1
dun a c | a1 | a2 = a1
dun a c | a2 = a1

--qun : (a : A) → (c : cun a ≡ a1) → gun a c ≡ dun a c
--qun a c with fun a
--... | z = ?


pun : (a : A) → (c : cun a ≡ a1) → gun a c ≡ dun a c
pun a c with bun a
pun a c | a1 with fun a
pun a c | a1 | a1 with bun a
pun a c | a1 | a1 | a1 = refl
pun a c | a1 | a1 | a2 = refl
pun a c | a1 | a2 = refl
pun a c | a2 with fun a
pun a c | a2 | a1 with bun a
pun a c | a2 | a1 | a1 = refl
pun a c | a2 | a1 | a2 = refl
pun a c | a2 | a2 = refl

```

Could someone explain to me why qun returns an error?

In my code, I have pun in the type of the function I am working on and I
also have problems with with abstraction there.
Given gun and dun, is there a way to simplify pun, possibly removing the
second bun abstraction?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171012/2d7fa013/attachment.html>