Agda中如何在函数定义中复用with抽象提供的信息？

你定义的区间类型𝕀如下：

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

在实现⊓𝕀（下确界）算子时，针对-∞ x ⊓𝕀 (y +∞)的情况，你已经通过inspect拿到了(y ≤ᵇ x) ≡ true的见证y≤x≡tt，只需直接将这个见证传入≤ᵇ⇒≤即可生成y ≤ x的序关系见证，填补代码中的洞：

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

更简洁的写法（无需inspect） #

其实可以省略inspect，直接利用with模式匹配的上下文信息。当分支匹配到true时，当前上下文中y ≤ᵇ x ≡ true可由refl直接证明，因此代码可简化为：

-∞ x ⊓𝕀 (y +∞) with y ≤ᵇ x
... | false = ⊥
... | true = I y x {≤ᵇ⇒≤ refl}

原理是≤ᵇ⇒≤的类型应为∀ {m n} → (m ≤ᵇ n) ≡ true → m ≤ n，它接受布尔相等的见证，输出对应的序关系证明。无论是inspect生成的y≤x≡tt还是with分支下的refl，都满足这个参数的类型要求。

内容的提问来源于stack exchange，提问作者dec