[Agda] Unbound level variables in rewrite rule

[Jesper Cockx]

Hi Filippo,

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
https://github.com/agda/agda/issues/4020, which has been fixed in the
development version.

-- Jesper

On Fri, Jan 24, 2020 at 3:11 PM Filippo Sestini <
Filippo.Sestini at nottingham.ac.uk> wrote:

> Hi all,
>
> I'm trying to follow this blog post [1] about rewriting rules,
> specifically the part about encoding observational equality.
>
> I'm having trouble with convincing Agda that `cong-λ` is a valid rewrite
> rule. In particular, if I try to typecheck the following bit
>
> {-# OPTIONS --rewriting --prop #-}
>
> module Test where
>
> open import Agda.Primitive
> open import Agda.Builtin.Equality
> open import Agda.Builtin.Equality.Rewrite
>
> variable
>   ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
>
> infix 6 _≅_
> postulate
>   _≅_ : {A : Set ℓ₁} {B : Set ℓ₂} → A → B → Prop (ℓ₁ ⊔ ℓ₂)
>
> postulate
>   cong-λ : {A : Set ℓ₁} {B : Set ℓ₂}
>     → {P : A → Set ℓ₃} {Q : B → Set ℓ₄}
>     → (f : (x : A) → P x) (g : (y : B) → Q y)
>     → ((λ x → f x) ≅ (λ y → g y))
>     ≡ ((x : A) (y : B) (x≅y : x ≅ y) → f x ≅ g y)
> {-# REWRITE cong-λ #-}
>
> Agda complaints that "cong-λ  is not a legal rewrite rule, since the
> following variables are not bound by the left hand side:  ℓ₄, ℓ₃".
>
> 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, ℓ₁, ℓ₂.
>
> Could somebody clarify this for me? I'm on Agda version 2.6.0.1.
>
> Thanks
>
> [1] https://jesper.sikanda.be/posts/hack-your-type-theory.html
>
> --
> Filippo Sestini
>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200124/da57b42e/attachment.html>