<div dir="ltr">Hi all,<br><div><br></div><div>Does anyone know how I can get this to work?</div><div><br></div><div><font face="monospace">                             (λ { (C , A) → (C×A→D (C , A)) })<br>                           ≡⟨ extensionality (λ C×A → refl) ⟩<br>                             (λ { x → (C×A→D x) })<br></font></div><div><br></div><div>Agda is telling me:</div><div><br></div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><font face="monospace">(λ { (C , A) → C×A→D (C , A) }) C×A != C×A→D C×A of type D</font></div><div><font face="monospace">when checking that the expression refl has type</font></div><div><font face="monospace">(λ { (C , A) → C×A→D (C , A) }) C×A ≡ C×A→D C×A</font></div></blockquote><div><br></div><div>Thanks,</div><div>-db</div><div><br></div></div>