[Agda] An agsy-mmetry proof

[Sebastian Hanowski]

Hej,


I've bought myself a computer again. One of the first things i installed 
was Agda.
My dependently typoed programming had gotten a bit rusty, so i tried to warm
up with this:

     Eq : (A : Set) -> A -> A -> Set1
     Eq A a b = (P : A -> Set) -> P a -> P b

     reflEq : {A : Set} -> (a : A) -> Eq A a a
     reflEq a = \P x -> x

     symEq : {A : Set} -> (a b : A) -> Eq A a b -> Eq A b a
     symEq a b q = \P p -> q (\x -> P x -> P a) (\y -> y) p

Since there was no one else around, i asked agsy too how to fill this hole

     symEq a b q = \P p -> q (\x -> P x -> P a) ? p

and i got something like this

     symEq a b q = \P p -> q (\x -> P x -> P a) (q (\_ -> P a)) p

Funny enough i can't reproduce it, however it wasn't me, because i couldn't
have thought of it. That's why i pressed the 'Like' button.


Cheers,
Sebastian