Agda中Lambda表达式带大括号与不带的差异及HoTT引理报错问题

核心区别 #

• 带大括号的Lambda：模式匹配Lambda
  λ {(tr u) → refl} 是Agda的模式匹配Lambda语法，专门用于解构归纳类型的元素。它会直接匹配归纳类型的构造子（这里tr是命题截断|| P ||的唯一构造子tr : P → || P ||），将构造子包裹的参数绑定到u上。这种写法要求目标类型必须是归纳类型，且模式需在命题唯一性保证下覆盖所有可能的元素。

• 不带大括号的Lambda：普通参数绑定
  λ (tr u) → refl 是普通Lambda的嵌套参数写法，相当于尝试把输入参数当作函数tr的参数来推导u。但tr是归纳类型的构造子（是从P到|| P ||的引入规则），并非可反向调用的函数——你不能把|| P ||类型的元素传给tr（tr的参数是P类型），因此Agda会因类型不匹配报错。

结合引理3.9.1的证明问题分析 #

引理要证明的是 ∀ {n : Level} {P : Set n} → isMereProposition P → P ≃ || P ||，其中|| P ||是命题截断类型（归纳类型，构造子为tr）。

报错代码的问题 #

unique-choice {n} {P} PisProp = ⟨ tr , ⟨ ⟨ inverse-tr , (λ (tr u) → refl) ⟩ , 
                                          ⟨ inverse-tr , (λ u → refl) ⟩ ⟩ ⟩ where
                                          inverse-tr : || P || → P
                                          inverse-tr = λ (tr u) → u

这里存在两个关键错误：

1. inverse-tr = λ (tr u) → u：试图用普通Lambda解构|| P ||的元素，但tr是构造子而非可调用函数，无法通过(tr u)的写法从|| P ||类型中提取u，必须用模式匹配完成归纳类型的解构。
2. λ (tr u) → refl：同理，无法把|| P ||类型的元素当作tr的参数，类型不匹配直接触发报错。

正确代码的原理 #

unique-choice {n} {P} PisProp = ⟨ tr , ⟨ ⟨ inverse-tr , (λ {(tr u) → refl}) ⟩ , 
                                          ⟨ inverse-tr , (λ u → refl) ⟩ ⟩ ⟩ where
                                          inverse-tr : || P || → P
                                          inverse-tr = λ {(tr u) → u}

这段代码通过模式匹配Lambda解决了问题：

• inverse-tr = λ {(tr u) → u}：匹配|| P ||的构造子tr，正确提取出内部的P类型元素u，完全符合归纳类型的解构规则。
• λ {(tr u) → refl}：通过模式匹配得到u后，结合isMereProposition P的条件，可推导出tr u与tr (inverse-tr (tr u))相等，因此能合法返回refl。

内容的提问来源于stack exchange，提问作者Werner Germán Busch