如何证明元素加法对于三次有限多集是射影？

Question

我正在尝试使用三次标准库中定义的有限多重集的类型：https://github.com/agda/cubical/blob/0d272ccbf6f3b142d1b723cead28209444bc896f/Cubical/HITs/FiniteMultiset/Base.agda#L15

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

我能够复制关于计数可扩展性的证明，我的一个引理表明，您可以从等式两边删除一个元素并保持等式。

类似于这一点：https://github.com/agda/cubical/blob/0d272ccbf6f3b142d1b723cead28209444bc896f/Cubical/HITs/FiniteMultiset/Properties.agda#L183

 remove1-≡-lemma : ∀ {a} {x} xs → a ≡ x → xs ≡ remove1 a (x ∷ xs)
 remove1-≡-lemma {a} {x} xs a≡x with discA a x
 ...                            | yes _   = refl
 ...                            | no  a≢x = ⊥.rec (a≢x a≡x)

我的证明没有使用相同的语法，但是在核心库语法中是

 cons-path-lemma : ∀ {x} xs ys → (x ∷ xs) ≡ (x ∷ ys) → xs ≡ ys

在证明使用remove1-≡-lemma路径的路径上构成的路径，该路径是功能上由remove1 x构成的自变量路径。

这要求值的类型具有可判定的相等性，因为没有remove1就没有意义。但是引理本身并没有提到可判定的相等性，因此我想我会尝试以不作假设的情况来证明这一点。现在已经一周了，我不知所措，因为这似乎“显而易见”，但如此顽固地证明。

我以为我对此直觉可证明的直觉可能来自我的经典数学背景，因此并没有建设性/连续地遵循。

所以我的问题是：在不假设元素类型的情况下，这是否可以证明？如果是这样，证明的总体结构将是什么样子，我很难获得想要同时引入两个FMSet的证明才能工作（因为我主要是在尝试根据需要获取要排队的路径时猜测）。如果没有假设就无法证明这一点，是否有可能证明它在某种程度上等同于必要的假设？

Answer 1

我不能提供证明，而是一个争论，为什么不假设可判定性就可以证明。我认为有限的多集可以表示为函数Fin n -> A，而多集f和g之间的相等性是由置换phi : Fin n ~ Fin n给出的（即Fin n上的可逆函数），使得f o phi = g成立。现在

(a :: f) 0 = a
 (a :: f) (suc i) = f i