<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Thanks, Ulf!<div class="">After changing my product type definition to match yours, I am unstuck. :)</div><div class=""><br class=""></div><div class="">Originally, I’d written:</div><div class=""><br class=""></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class=""><font face="Menlo" class="">data _×_ (A : Set) (B : Set) : Set where</font></div></div><div class=""><div class=""><font face="Menlo" class=""> _,_ : A → B → (A × B)</font></div></div></blockquote><div class=""><div class=""><br class=""></div><div class="">I guess there was something more I needed to do, in order to have this type play nicely with the rest of the system?</div><div class=""><br class=""></div><div class="">Now (using your product type), I’m able to complete the proof in a single step and without invoking extensionality:</div><div class=""><br class=""></div></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class=""><div class=""><font face="Menlo" class="">117 begin</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">118 <font color="#9aa60d" class="">(λ { C→A⇒D (C , A) → C→A⇒D C · A })</font></font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">119 (λ C₁ → ƛ (λ A₁ → C×A→D (C₁ , A₁)))</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">120 ≡⟨⟩</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">121 C×A→D</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">122 ∎</font></div></div></div></blockquote><div class=""><div class=""><br class=""></div><div class="">However, I’m getting the following warning, related to the highlighted code above (line 118):</div><div class="">(Note that <i class="">column</i> numbers below are inaccurate.)</div><div class=""><br class=""></div></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class=""><div class=""><font face="Menlo" class="">Sort _78 [ at ###.agda:118,31-64 ]</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">_79 : _78 [ at ###.agda:118,31-64 ]</font></div></div></div><div class=""><div class=""><div class=""><font face="Menlo" class="">_81 : _79 [ at ###.agda:118,31-64 ]</font></div></div></div></blockquote><div class=""><div class=""><br class=""></div><div class="">Do you know why?</div><div class=""><br class=""></div><div class="">Thanks,</div><div class="">-db</div><div class=""><br class=""></div><div><br class=""><blockquote type="cite" class=""><div class="">On Jan 14, 2021, at 6:02 AM, Ulf Norell <<a href="mailto:ulf.norell@gmail.com" class="">ulf.norell@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">FWIW this works:</div><div class=""><br class=""></div><div style="margin-left:40px" class=""><span style="font-family:monospace" class="">open import Agda.Builtin.Sigma<br class="">open import Agda.Builtin.Equality<br class=""><br class="">_×_ : Set → Set → Set<br class="">A × B = Σ A λ _ → B<br class=""><br class="">postulate<br class=""> A B C : Set<br class=""> f : A × B → C<br class=""> ext : ∀ {A B : Set} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g<br class=""><br class="">prf : (λ { (x , y) → f (x , y) }) ≡ (λ { p → f p })<br class="">prf = ext λ _ → refl</span></div><div class=""><br class=""></div><div class="">Have you made sure that the pair type you are using has eta equality?</div><div class=""><br class=""></div><div class="">/ Ulf<br class=""></div></div><br class=""><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" class="">james.wood.100@strath.ac.uk</a>> wrote:<br class=""></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 class="">
generative. The first thing I'd try, assuming sufficiently new Agda, is <br class="">
to remove all the curly braces.<br class="">
<br class="">
James<br class="">
<br class="">
On 14/01/2021 01:22, Jason -Zhong Sheng- Hu wrote:<br class="">
> CAUTION: This email originated outside the University. Check before <br class="">
> clicking links or attachments.<br class="">
> <br class="">
> That’s very strange. I would expect this equality to hold <br class="">
> definitionally. You shouldn’t even need extensionality.<br class="">
> <br class="">
> Does agda complain anything if you remove the first two lines entirely?<br class="">
> <br class="">
> Thanks,<br class="">
> <br class="">
> Jason Hu<br class="">
> <br class="">
> *From: *David Banas <mailto:<a href="mailto:capn.freako@gmail.com" target="_blank" class="">capn.freako@gmail.com</a>><br class="">
> *Sent: *Wednesday, January 13, 2021 8:20 PM<br class="">
> *To: *Agda mailing list <mailto:<a href="mailto:agda@lists.chalmers.se" target="_blank" class="">agda@lists.chalmers.se</a>><br class="">
> *Subject: *[Agda] How to validate eta-reduction in equational reasoning <br class="">
> proofs?<br class="">
> <br class="">
> Hi all,<br class="">
> <br class="">
> Does anyone know how I can get this to work?<br class="">
> <br class="">
> (λ { (C , A) → (C×A→D (C , A)) })<br class="">
> ≡⟨extensionality (λ C×A → refl) ⟩<br class="">
> (λ { x → (C×A→D x) })<br class="">
> <br class="">
> Agda is telling me:<br class="">
> <br class="">
> (λ { (C , A) → C×A→D (C , A) }) C×A != C×A→D C×A of type D<br class="">
> <br class="">
> when checking that the expression refl has type<br class="">
> <br class="">
> (λ { (C , A) → C×A→D (C , A) }) C×A ≡ C×A→D C×A<br class="">
> <br class="">
> Thanks,<br class="">
> <br class="">
> -db<br class="">
> <br class="">
> <br class="">
> _______________________________________________<br class="">
> Agda mailing list<br class="">
> <a href="mailto:Agda@lists.chalmers.se" target="_blank" class="">Agda@lists.chalmers.se</a><br class="">
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">
> <br class="">
<br class="">
_______________________________________________<br class="">
Agda mailing list<br class="">
<a href="mailto:Agda@lists.chalmers.se" target="_blank" class="">Agda@lists.chalmers.se</a><br class="">
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">
</blockquote></div>
_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></blockquote></div><br class=""></div></body></html>