有限多重集作为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问题是this one for comm和comm。像您一样，我也同样感到沮丧：如果所有这些类型都是this one for trunc，为什么我需要写任何东西，更不用说复杂的东西了，以证明某些2路径？！？！

因此，首先，从第一个链接的答案开始，>]

trunc
并问Agda孔的类型是什么。 

目标：Set

听起来不错，因为我们知道comm x y xs i ++ ys = ? 简单地归纳为comm x y (xs ++ []) i ≡ comm x y xs i。因此，让我们问一问究竟能买到什么。将comm x y (xs ++ []) ≡ comm x y xs放入孔中并询问其类型：

具有：

xs + [] ≡ xs

然后@Saizan的答案指示我们用这些面孔生成cong (comm x y) (unitr-++ xs)：

PathP
     (λ i → x ∷ y ∷ unitr-++ xs i ≡ y ∷ x ∷ unitr-++ xs i)
     (comm x y (xs ++ [])) (comm x y xs)
并在其上选择正确的内部点，为我们填充了孔：

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

isSet→isSet' trunc
  (comm x y (xs ++ []))
  (comm x y xs)
  (λ j → x ∷ y ∷ unitr-++ xs i)
  (λ j → y ∷ x ∷ unitr-++ xs i)
按照链接的答案的建议，我们可以向Agda询问要构造的立方体的面：

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) 
，阿格达告诉我们：

r : Cube ? ? ? ? ? ?
r = cong (cong unitr-++) (trunc xs1 xs2 p q)
所以现在我们确切地知道要构造哪个多维数据集（使用C-c C-s所见证的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)
也是Set的事实：

Groupoid
[现在，一方面，我们可以为完成而感到高兴，但另一方面，我们很生气，因为这个答案都是“看着另一个答案并准确地做到这一点”，“看着这个其他答案，并完全做到这一点”，但是可以肯定的是，即使您的类型，函数和函数属性与我问我最初的问题时的方法不同，也可以做到这一点。应该在这里抽象出来吧？

并且that

是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

实现了上述所有机制，但一口气实现了所有功能以及这些功能的所有属性。因此，您不必看这个答案和两个链接的答案，然后再进行所有OVER和OVER以及OVER的操作，实际上，最后，它不应该有所作为，因为所有构造的路径都是路径等效的无论如何。