[Agda] Unbound level variables in rewrite rule

[Filippo Sestini]

Hi Jesper,

I see! No worries, and many thanks for the reply.

Cheers
-- 
Filippo 

On 1/24/20, 2:35 PM, "Agda on behalf of Jesper Cockx" <agda-bounces at lists.chalmers.se on behalf of Jesper at sikanda.be> wrote:

    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 <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