[Agda] Unbound level variables in rewrite rule

[Filippo Sestini]

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.