<div dir="ltr"><div>Hi Filippo,</div><div><br></div><div>I'm sorry, I should probably have mentioned in the blog post that you should use the development version of 2.6.1 for some of the examples. Specifically, the problem you run into seems to be <a href="https://github.com/agda/agda/issues/4020">https://github.com/agda/agda/issues/4020</a>, which has been fixed in the development version.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jan 24, 2020 at 3:11 PM Filippo Sestini <<a href="mailto:Filippo.Sestini@nottingham.ac.uk">Filippo.Sestini@nottingham.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">Hi all,<br>
<br>
I'm trying to follow this blog post [1] about rewriting rules, specifically the part about encoding observational equality.<br>
<br>
I'm having trouble with convincing Agda that `cong-λ` is a valid rewrite rule. In particular, if I try to typecheck the following bit<br>
<br>
{-# OPTIONS --rewriting --prop #-}<br>
<br>
module Test where<br>
<br>
open import Agda.Primitive<br>
open import Agda.Builtin.Equality<br>
open import Agda.Builtin.Equality.Rewrite<br>
<br>
variable<br>
  ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level<br>
<br>
infix 6 _≅_<br>
postulate<br>
  _≅_ : {A : Set ℓ₁} {B : Set ℓ₂} → A → B → Prop (ℓ₁ ⊔ ℓ₂)<br>
<br>
postulate<br>
  cong-λ : {A : Set ℓ₁} {B : Set ℓ₂}<br>
    → {P : A → Set ℓ₃} {Q : B → Set ℓ₄}<br>
    → (f : (x : A) → P x) (g : (y : B) → Q y)<br>
    → ((λ x → f x) ≅ (λ y → g y))<br>
    ≡ ((x : A) (y : B) (x≅y : x ≅ y) → f x ≅ g y)<br>
{-# REWRITE cong-λ #-}<br>
<br>
Agda complaints that "cong-λ  is not a legal rewrite rule, since the following variables are not bound by the left hand side:  ℓ₄, ℓ₃".<br>
<br>
I'm a bit confused since the rule is copied verbatim from the blog post. But in any case, I don't really understand what is the problem here, or why ℓ₄, ℓ₃ are an issue but not, say, ℓ₁, ℓ₂.<br>
<br>
Could somebody clarify this for me? I'm on Agda version 2.6.0.1.<br>
<br>
Thanks<br>
<br>
[1] <a href="https://jesper.sikanda.be/posts/hack-your-type-theory.html" rel="noreferrer" target="_blank">https://jesper.sikanda.be/posts/hack-your-type-theory.html</a><br>
<br>
-- <br>
Filippo Sestini<br>
<br>
<br>
<br>
<br>
<br>
This message and any attachment are intended solely for the addressee<br>
and may contain confidential information. If you have received this<br>
message in error, please contact the sender and delete the email and<br>
attachment. <br>
<br>
Any views or opinions expressed by the author of this email do not<br>
necessarily reflect the views of the University of Nottingham. Email<br>
communications with the University of Nottingham may be monitored <br>
where permitted by law.<br>
<br>
<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>