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

Question

在 Cubical Agda 的标准库中，有一些有限的多重集，我在下面重现了它们的优雅定义：

{-# 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 问题是一个 forcomm和一个 fortrunc。和你一样，我也曾在同样的挫折中挣扎：如果所有这些类型都是Sets，为什么我需要写任何东西，更不用说复杂的东西来证明一些 2 路径？！？！

\n\n

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

\n\n

comm x y xs i ++ ys = ?\n

\n\n

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

\n\n

\n

目标：comm x y (xs ++ []) i \xe2\x89\xa1 comm x y xs i

\n

\n\n

嗯，这听起来很有希望，因为我们comm x y (xs ++ []) \xe2\x89\xa1 comm x y xs只需通过xs + [] \xe2\x89\xa1 xs归纳就知道这一点。那么，让我们问问这到底会给我们带来什么。放入cong (comm x y) (unitr-++ xs)孔中并询问其类型：

\n\n

\n

有：

\n\n

PathP\n     (\xce\xbb i \xe2\x86\x92 x \xe2\x88\xb7 y \xe2\x88\xb7 unitr-++ xs i \xe2\x89\xa1 y \xe2\x88\xb7 x \xe2\x88\xb7 unitr-++ xs i)\n     (comm x y (xs ++ [])) (comm x y xs)\n

\n

\n\n

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

\n\n

isSet\xe2\x86\x92isSet\' trunc\n  (comm x y (xs ++ []))\n  (comm x y xs)\n  (\xce\xbb j \xe2\x86\x92 x \xe2\x88\xb7 y \xe2\x88\xb7 unitr-++ xs i)\n  (\xce\xbb j \xe2\x86\x92 y \xe2\x88\xb7 x \xe2\x88\xb7 unitr-++ xs i)\n

\n\n

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

\n\n

unitr-++ (comm x y xs i) j = isSet\xe2\x86\x92isSet\' trunc\n  (comm x y (xs ++ []))\n  (comm x y xs)\n  (\xce\xbb j \xe2\x86\x92 x \xe2\x88\xb7 y \xe2\x88\xb7 unitr-++ xs j)\n  (\xce\xbb j \xe2\x86\x92 y \xe2\x88\xb7 x \xe2\x88\xb7 unitr-++ xs j)\n  j i\n

\n\n

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

\n\n

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

\n\n

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

\n\n

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

\n\n

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

\n\n

r : Cube (\xce\xbb i j \xe2\x86\x92 trunc xs1 xs2 p q i j ++ [])\n         (\xce\xbb i j \xe2\x86\x92 unitr-++ xs1 j)\n         (\xce\xbb i j \xe2\x86\x92 unitr-++ xs2 j)\n         (\xce\xbb i j \xe2\x86\x92 trunc xs1 xs2 p q i j)\n         (\xce\xbb i j \xe2\x86\x92 unitr-++ (p i) j)\n         (\xce\xbb i j \xe2\x86\x92 unitr-++ (q i) j)\n

\n\n

Set所以现在我们确切地知道要构造哪个立方体（使用s 也是s的事实Groupoid，如 所见证的hLevelSuc 2 _）：

\n\n

unitr-++ (trunc xs1 xs2 p q i j) = isGroupoid\xe2\x86\x92isGroupoid\' (hLevelSuc 2 _ trunc)\n  (\xce\xbb i j \xe2\x86\x92 trunc xs1 xs2 p q i j ++ [])\n  (\xce\xbb i j \xe2\x86\x92 unitr-++ xs1 j)\n  (\xce\xbb i j \xe2\x86\x92 unitr-++ xs2 j)\n  (\xce\xbb i j \xe2\x86\x92 trunc xs1 xs2 p q i j)\n  (\xce\xbb i j \xe2\x86\x92 unitr-++ (p i) j)\n  (\xce\xbb i j \xe2\x86\x92 unitr-++ (q i) j)\n  i\n  j\n

\n\n

到目前为止，一方面，我们可以很高兴我们已经完成了，但另一方面，我们很生气，因为这个答案都是“看看这个另一个答案，然后照做”，“看看这个另一个答案”回答并完全做到这一点”，但如果你能完全做到这一点，即使你的类型、你的函数和你的函数属性与我问原来的问题时的不一样，那么应该有一些东西被抽象到这里了，对吧？

\n\n

事实就是如此FMSetElimProp。FMSet它一举实现了上述所有这些机制，特别是针对所有功能和这些功能的所有属性。因此，您不必查看这个答案和两个链接的答案，并一遍又一遍地重复所有这些，而事实上，最终它不应该产生任何影响，因为所有构造的路径都是路径- 无论如何都是等价的。

\n