Agda: cannot instantiate metavariable

Question

I'm fairly new to Agda and I'm trying to construct the Interval's lattice. So far I've defined the Lattice datatype as follows:

data 𝕀 : Set where
  ⊤ : 𝕀
  ⊥ : 𝕀
  -∞ : ℤ → 𝕀
  _+∞ : ℤ → 𝕀
  I : (l : ℤ) → (u : ℤ) → {l ≤ u} → 𝕀

and the _⊔𝕀_ operator as:

_⊔𝕀_ : Op₂ 𝕀
⊤ ⊔𝕀 y = ⊤
⊥ ⊔𝕀 y = y
-∞ x ⊔𝕀 ⊤ = ⊤
-∞ x ⊔𝕀 ⊥ = -∞ x
-∞ x ⊔𝕀 -∞ y = -∞ (x ⊔ y)
-∞ x ⊔𝕀 (y +∞) = ⊤
-∞ x ⊔𝕀 I l u = -∞ (x ⊔ u)
(x +∞) ⊔𝕀 ⊤ = ⊤
(x +∞) ⊔𝕀 ⊥ = x +∞
(x +∞) ⊔𝕀 -∞ y = ⊤
(x +∞) ⊔𝕀 (y +∞) = (x ⊓ y) +∞
(x +∞) ⊔𝕀 I l u = (x ⊓ l) +∞
I l u ⊔𝕀 ⊤ = ⊤
I l u {l≤u} ⊔𝕀 ⊥ = I l u {l≤u}
I l u ⊔𝕀 -∞ x = -∞ (u ⊔ x)
I l u ⊔𝕀 (x +∞) = (l ⊓ x) +∞
I l₁ u₁ {l₁≤u₁} ⊔𝕀 I l₂ u₂ {l₂≤u₂} = I (l₁ ⊓ l₂) (u₁ ⊔ u₂) {≤-trans (≤-trans (i⊓j≤i l₁ l₂) l₁≤u₁) ((i≤i⊔j u₁ u₂))}

but when trying to prove commutativity of the operator in the case

⊔𝕀-comm (I l₁ u₁ {l₁≤u₁}) (I l₂ u₂ {l₂≤u₂}) = {!cong₂ I (⊓-comm l₁ l₂) (⊔-comm u₁ u₂)!}

I get the error

Cannot instantiate the metavariable _C_171 to solution
({_ : l ≤ u} → 𝕀) since it contains the variable l
which is not in scope of the metavariable
when checking that the expression I has type ℤ → ℤ → _C_171

which, if I understand correctly, is related to the fact that the I constructor has an implicit argument, nevertheless I have no idea on how to solve the issue.

Answer 1

Indeed the problem is that I's type (l : ℤ) → (u : ℤ) → {l ≤ u} → 𝕀 does not match the type of the first argument to cong₂, A → B → C, because in this case C depends on the first two arguments. You can use one of the dependent congs like dcong₂ instead:

open import Data.Product
open import Data.Product.Properties

⊔𝕀-comm : ∀ x y → x ⊔𝕀 y ≡ y ⊔𝕀 x
⊔𝕀-comm (I l₁ u₁ {l₁≤u₁}) (I l₂ u₂ {l₂≤u₂}) = dcong₂
  (λ (l , u) p → I l u {p})
  (×-≡,≡→≡ (⊓-comm l₁ l₂ , ⊔-comm u₁ u₂))
  (≤-irrelevant _ _)

Or you could prove a helper lemma for this purpose:

cong-I : ∀ {l l' u u' p p'} → l ≡ l' → u ≡ u' → I l u {p} ≡ I l' u' {p'}
cong-I {p = p} {p'} refl refl with ≤-irrelevant p p'
... | refl = refl

⊔𝕀-comm : ∀ x y → x ⊔𝕀 y ≡ y ⊔𝕀 x
⊔𝕀-comm (I l₁ u₁) (I l₂ u₂) = cong-I (⊓-comm l₁ l₂) (⊔-comm u₁ u₂)