Agda 证明类型是一个集合，不再适用于立方 Agda

Question

所以我正在 Agda 中实现一些（大部分）HoTT 定义。为了检查类型是否是我定义的集合：

isSet : ∀ (A : Set) → Set
isSet A = ∀ {x y : A} (p q : (x ≡ y)) → (p ≡ q)

证明 Σ(x :a) P x 是一个集合（当 P x 是时）在“正常”（不导入立方）agda 中工作得很好：

Σ-isSet : ∀ {A : Set} (P : A → Set) → (∀ (x : A) → isSet (P x)) → isSet (∃[ z ] (P z))
Σ-isSet {A} P φ {x} {y} refl refl = refl

但是当我导入立方 agda （因为我需要它来定义 HIT）时，证明不再起作用：

Cannot split on argument of non-datatype x ≡ y
when checking that the pattern refl has type x ≡ y

发生什么事了？证明是否不正确，或者在使用立方 agda 时是否需要使用不同的运算符？谢谢！

Answer 1

第一个问题是你的证明依赖于公理 K 并且没有类型检查

--without-K

。公理 K 本质上说每种类型都是一个集合，因此您的引理在该设置中微不足道也就不足为奇了。

事实上，你的引理在 HoTT 中是错误的：你需要 both

A

和

P

都是集合（族）才能得出

Σ A P

是集合的结论。这是一个很好的练习：给出类型

A

和集合族

P : A → Type

的示例，使得

Σ A P

不是集合。

第二个问题是，cubic Agda 使用 path types 而不是归纳身份类型，因此你无法在

refl

上进行模式匹配。

A

中的路径本质上是区间类型

I → A

之外的函数，在端点

i0

和

i1

处具有指定值。路径类型支持与

refl

（

--without-K

）上以

J

形式的模式匹配提供的消除原则基本相同的消除原则，但其在

refl

上的计算规则仅适用于另一条路径，而不适用于其他路径。定义上。

在立方 Agda 中，通常会证明更普遍的结果，即 Σ 保留 h 能级：如果

A

是 n 型且

P

是 n 型族，则

Σ A P

是 n 型。例如，请参阅 1lab 或 cubical。

---

顺便说一句，在使用 HoTT 时，您可以将

Set

重命名为

Type

以避免混淆：

{-# OPTIONS --no-import-sorts #-}
open import Agda.Primitive renaming (Set to Type; Setω to Typeω)

大多数立方体/HoTT 库都会为您完成此操作。