有限多重集作为 Cubical Agda 中的 HIT

Question

在 Cubical Agda 的标准库中，有 finite multisets 我将其优雅的定义复制如下：

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude

infixr 20 _∷_

data FMSet (A : Set) : Set where
  []    : FMSet A
  _∷_   : (x : A) → (xs : FMSet A) → FMSet A
  comm  : ∀ x y xs → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
  trunc : isSet (FMSet A)

_++_ : ∀ {A : Set} -> FMSet A → FMSet A → FMSet A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
comm x y xs i ++ ys = comm x y (xs ++ ys) i
trunc xs1 xs2 p q i j ++ ys =
  trunc (xs1 ++ ys) (xs2 ++ ys) (cong (_++ ys) p) (cong (_++ ys) q) i j

[] 是右中性元素的证明使用了我不理解的抽象引理 FMSetElimProp.f 。因此，我试图做出直接证明，但我被卡住了。这是我的尝试：

unitr-++ : ∀ {A : Set} (ys : FMSet A) → ys ++ [] ≡ ys
unitr-++ [] = refl
unitr-++ (y ∷ ys) = cong ((y ∷_)) (unitr-++ ys)
unitr-++ (comm x y xs i) = cong₂ {!comm x y!} (unitr-++ xs) refl
unitr-++ (trunc xs1 xs2 p q i j) = {!!}

我走在正确的轨道上吗？我怎样才能完成这个证明？

Answer 1

回答这个问题的两个 SO 问题是 and 。和你一样，我也曾在同样的挫折中挣扎过：如果所有这些类型都是 Sets，为什么我需要写任何东西，更不用说复杂的东西，来证明一些 2 路径？！？！

所以，首先，从第一个链接的答案开始，让我们从

开始

comm x y xs i ++ ys = ?

并询问 Agda 洞的类型是什么。

Goal: comm x y (xs ++ []) i ≡ comm x y xs i

嗯，这听起来很有希望，因为我们只需通过 xs + [] ≡ xs 归纳就知道 comm x y (xs ++ []) ≡ comm x y xs。那么，让我们问一下这究竟会给我们带来什么。将cong (comm x y) (unitr-++ xs)放入洞中，询问其类型：

Have:

PathP
     (λ i → x ∷ y ∷ unitr-++ xs i ≡ y ∷ x ∷ unitr-++ xs i)
     (comm x y (xs ++ [])) (comm x y xs)

然后@Saizan 的回答指示我们生成具有这些面孔的 Square：

isSet→isSet' trunc
  (comm x y (xs ++ []))
  (comm x y xs)
  (λ j → x ∷ y ∷ unitr-++ xs i)
  (λ j → y ∷ x ∷ unitr-++ xs i)

并在其上选择正确的内部点，填充我们的洞：

unitr-++ (comm x y xs i) j = isSet→isSet' trunc
  (comm x y (xs ++ []))
  (comm x y xs)
  (λ j → x ∷ y ∷ unitr-++ xs j)
  (λ j → y ∷ x ∷ unitr-++ xs j)
  j i

对于第二个缺失的子句，即在

unitr-++ (trunc xs1 xs2 p q i j)

按照链接答案的建议，我们可以向 Agda 询问我们想要构建的立方体的面：

r : Cube ? ? ? ? ? ?
r = cong (cong unitr-++) (trunc xs1 xs2 p q)

通过在所有六个面孔中使用 C-c C-s，Agda 告诉我们：

r : Cube (λ i j → trunc xs1 xs2 p q i j ++ [])
         (λ i j → unitr-++ xs1 j)
         (λ i j → unitr-++ xs2 j)
         (λ i j → trunc xs1 xs2 p q i j)
         (λ i j → unitr-++ (p i) j)
         (λ i j → unitr-++ (q i) j)

所以现在我们确切地知道要构建哪个立方体（使用 Sets 也是 Groupoids 的事实，正如 hLevelSuc 2 _ 所见证的那样）：

unitr-++ (trunc xs1 xs2 p q i j) = isGroupoid→isGroupoid' (hLevelSuc 2 _ trunc)
  (λ i j → trunc xs1 xs2 p q i j ++ [])
  (λ i j → unitr-++ xs1 j)
  (λ i j → unitr-++ xs2 j)
  (λ i j → trunc xs1 xs2 p q i j)
  (λ i j → unitr-++ (p i) j)
  (λ i j → unitr-++ (q i) j)
  i
  j

到现在为止，一方面，我们可以为完成而高兴，但另一方面，我们很生气，因为这个答案都是"look at this other answer and do exactly that"，"look at this other answer and do exactly that"，但是当然，如果你能做到这一点，即使你的类型、你的函数和你的函数属性与我问我最初的问题时的不一样，那么这里应该抽象出一些东西，对吧？

而就是 FMSetElimProp 所做的。它实现了上面的所有这些机制，特别是 FMSet，但是对于所有功能和这些功能的所有属性，一口气。所以你不必查看这个答案和两个链接的答案，然后一遍又一遍地做所有这些，实际上在最后它不应该有什么不同，因为所有构建的路径都是路径等价的无论如何。

有限多重集作为 Cubical Agda 中的 HIT

Finite multisets as a HIT in Cubical Agda

proof

agda

multiset

cubical-type-theory

homotopy-type-theory