<div dir="ltr"><div>FWIW this works:</div><div><br></div><div style="margin-left:40px"><span style="font-family:monospace">open import Agda.Builtin.Sigma<br>open import Agda.Builtin.Equality<br><br>_×_ : Set → Set → Set<br>A × B = Σ A λ _ → B<br><br>postulate<br>  A B C : Set<br>  f     : A × B → C<br>  ext   : ∀ {A B : Set} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g<br><br>prf : (λ { (x , y) → f (x , y) }) ≡ (λ { p → f p })<br>prf = ext λ _ → refl</span></div><div><br></div><div>Have you made sure that the pair type you are using has eta equality?</div><div><br></div><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jan 14, 2021 at 2:09 PM James Wood <<a href="mailto:james.wood.100@strath.ac.uk">james.wood.100@strath.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">It might not hold definitionally as written because extended λs are <br>
generative. The first thing I'd try, assuming sufficiently new Agda, is <br>
to remove all the curly braces.<br>
<br>
James<br>
<br>
On 14/01/2021 01:22, Jason -Zhong Sheng- Hu wrote:<br>
> CAUTION: This email originated outside the University. Check before <br>
> clicking links or attachments.<br>
> <br>
> That’s very strange. I would expect this equality to hold <br>
> definitionally. You shouldn’t even need extensionality.<br>
> <br>
> Does agda complain anything if you remove the first two lines entirely?<br>
> <br>
> Thanks,<br>
> <br>
> Jason Hu<br>
> <br>
> *From: *David Banas <mailto:<a href="mailto:capn.freako@gmail.com" target="_blank">capn.freako@gmail.com</a>><br>
> *Sent: *Wednesday, January 13, 2021 8:20 PM<br>
> *To: *Agda mailing list <mailto:<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
> *Subject: *[Agda] How to validate eta-reduction in equational reasoning <br>
> proofs?<br>
> <br>
> Hi all,<br>
> <br>
> Does anyone know how I can get this to work?<br>
> <br>
>                               (λ { (C , A) → (C×A→D (C , A)) })<br>
>                             ≡⟨extensionality (λ C×A → refl) ⟩<br>
>                               (λ { x → (C×A→D x) })<br>
> <br>
> Agda is telling me:<br>
> <br>
>     (λ { (C , A) → C×A→D (C , A) }) C×A != C×A→D C×A of type D<br>
> <br>
>     when checking that the expression refl has type<br>
> <br>
>     (λ { (C , A) → C×A→D (C , A) }) C×A ≡ C×A→D C×A<br>
> <br>
> Thanks,<br>
> <br>
> -db<br>
> <br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>