Cubical Agda中包含序的反对称性证明补全求助

以下是针对依赖对场景的完整可运行代码，同时解释hcomp的核心用法：

基础模块导入 #

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything

场景1：命题值函数的包含序反对称性 #

（这是依赖对的典型案例，A → Prop属于Σ Type (λ A → A → Type)的实例）

定义包含序 #

_⊆_ : {A : Type} → (P Q : A → Prop) → Type
P ⊆ Q = ∀ a → P a → Q a

手动用hcomp补全反对称性证明 #

如果不用现成的propExt，我们可以直接用hcomp构造命题间的相等路径：

-- 用hcomp实现Prop间的等价转化为相等
propEq : {X : Type} → isProp X → {Y : Type} → isProp Y → (X → Y) → (Y → X) → X ≡ Y
propEq isPropX isPropY f g =
  hcomp
    (λ i → λ {
      (i = i0) → λ x → f x  -- 区间起点约束：映射为f
    ; (i = i1) → λ y → g y  -- 区间终点约束：映射为g
    })
    (λ x → x)  -- 初始映射：恒等函数，利用Prop的唯一性自动适配约束

最终反对称性实现 #

⊆-antisym : {A : Type} → (P Q : A → Prop) → P ⊆ Q → Q ⊆ P → P ≡ Q
⊆-antisym P Q P⊆Q Q⊆P = funExt λ a → propEq (snd (P a)) (snd (Q a)) (P⊆Q a) (Q⊆P a)

场景2：Σ类型元素的包含序反对称性 #

假设每个依赖类型都是偏序，我们需要证明互相包含的Σ元素相等：

定义偏序结构 #

record Poset (A : Type) : Type where
  field
    _≤_ : A → A → Type
    ≤-refl : ∀ a → a ≤ a
    ≤-trans : ∀ a b c → a ≤ b → b ≤ c → a ≤ c
    ≤-antisym : ∀ a b → a ≤ b → b ≤ a → a ≡ b

Σ类型上的包含序定义 #

Σ-⊆ : {A : Type} → (B : A → Type) → (∀ a → Poset (B a)) → (x y : Σ A B) → Type
Σ-⊆ B B-poset x y = Σ (p : proj₁ x ≡ proj₁ y) (λ p → Poset._≤_ (B-poset (proj₁ x)) (proj₂ x) (transport p (proj₂ y)))

补全Σ类型的反对称性证明 #

Σ-⊆-antisym : {A : Type} → (B : A → Type) → (B-poset : ∀ a → Poset (B a)) →
              ∀ x y → Σ-⊆ B B-poset x y → Σ-⊆ B B-poset y x → x ≡ y
Σ-⊆-antisym B B-poset x y (p , x≤y) (q , y≤x) =
  ΣPath p (Poset.≤-antisym (B-poset (proj₁ x)) (proj₂ x) (transport p (proj₂ y)) x≤y (transport (sym p) y≤x))

hcomp核心用法解释 #

在Cubical Agda中，hcomp的作用是根据区间上的约束粘合元素/路径，其核心参数逻辑：

1. 第一个参数：指定约束生效的区间面（比如i0对应路径起点，i1对应路径终点）
2. 第二个参数：定义每个区间面上的元素约束（比如起点必须是函数f，终点必须是函数g）
3. 第三个参数：提供初始元素，Cubical会自动补全约束之间的路径

以区间类型的偏序反对称性为例，hcomp的典型应用：

≤-antisym : ∀ i j → i ≤ j → j ≤ i → i ≡ j
≤-antisym i j i≤j j≤i = hcomp (λ k → λ { (i0 = i) → j≤i k ; (i1 = i) → i≤j k }) i

这里通过hcomp将i≤j和j≤i两个方向的路径粘合，最终得到i≡j的路径。

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