导入Cubical Agda后，HoTT集合证明失效问题求助

问题根源 #

普通Agda中的等式x ≡ y是归纳数据类型，唯一构造子为refl，因此可以直接对refl做模式匹配。但Cubical Agda将等式实现为路径类型（Path Type）——这是一个原语类型而非归纳数据类型，因此无法通过refl模式匹配拆分参数，这就是报错Cannot split on argument of non-datatype x ≡ y的直接原因。

另外，普通Agda默认启用唯一性恒等原理（UIP），这使得你无需额外前提就能通过简单的refl匹配完成证明；但Cubical Agda中UIP并非默认成立，证明需要更严谨的路径操作。

解决方法：使用Cubical特有的路径操作 #

在Cubical环境下，需要借助路径转换、运输（transport）等原语来完成Σ类型的集合性证明。以下是修正后的实现：

open import Cubical.Foundations.Prelude

-- 保持你原有的isSet定义
isSet : ∀ (A : Set) → Set
isSet A = ∀ {x y : A} (p q : x ≡ y) → p ≡ q

-- 修正后的Σ-isSet：需要额外要求A是集合（Cubical中UIP不默认成立）
Σ-isSet : ∀ {A : Set}
        → isSet A
        → (P : A → Set)
        → (∀ x → isSet (P x))
        → isSet (Σ A P)
Σ-isSet isSetA P isSetP {x , px} {y , py} p q =
  let
    -- 将Σ类型的路径拆分为A分量的路径 + P分量的依赖路径
    (p₁ , p₂) = ΣPath≡PathΣ p
    (q₁ , q₂) = ΣPath≡PathΣ q

    -- 证明A分量的两条路径相等
    p₁≡q₁ : p₁ ≡ q₁
    p₁≡q₁ = isSetA p₁ q₁

    -- 利用路径相等将p₂运输到q₁的上下文，再证明与q₂相等
    p₂-transport : transport (λ i → P (p₁≡q₁ i)) p₂ ≡ q₂
    p₂-transport = isSetP _ (transport (λ i → P (p₁≡q₁ i)) p₂) q₂
  in
    -- 将分量的相等组合回Σ类型的路径相等
    ΣPath≡PathΣ⁻¹ (p₁≡q₁ , p₂-transport)

关键说明 #

1. Σ路径转换：ΣPath≡PathΣ是Cubical库提供的原语，用于将Σ类型的路径(x,px)≡(y,py)转换为一对路径：A分量的普通路径x≡y，以及P分量的依赖路径transport P p px ≡ py（transport用于将px沿着路径p运输到y的上下文）。
2. 集合性前提：Cubical中必须明确要求A是集合（即isSet A），因为UIP不再默认成立，无法像普通Agda那样省略该前提。

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