dec's questions

我对 Agda 还不熟悉，正在尝试构建 Interval 的格子。到目前为止，我已经将 Lattice 数据类型定义如下：

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

并且_⊔𝕀_运算符为：

_⊔𝕀_ : 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₂))}

但在试图证明以下情况下运算符的交换性时

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

我得到了错误

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

如果我理解正确的话，这与I构造函数具有隐式参数有关，但我不知道如何解决这个问题。

我正在尝试构建具有如下定义的数据类型的区间格：

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

为了在某​​些情况下在区间上定义 ⊓𝕀 (glb) 运算符，我必须进行模式匹配i ≤ᵇ j以定义运算符的适当值，尽管我不确定如何在案例定义中重用模式匹配提供的信息。

特别是在

-∞ x ⊓𝕀 (y +∞) with (y ≤ᵇ x) | inspect (y ≤ᵇ_) x
... | false | [ y≤x≡ff ] = ⊥
... | true | [ y≤x≡tt ] = I y x {≤ᵇ⇒≤ {!!}}

我有一个证人，(y ≤ᵇ x) ≡ true但我不知道如何使用它来结合它，≤ᵇ⇒≤以产生证人y ≤ x