如何证明元素加法对于立方有限多集是单射的?

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

如果phi : Fin (suc n) ~ Fin (suc n)证明a :: f = a :: g你可以构造一个psi : Fin n ~ Fin n来证明f = g。如果是phi 0 = 0则psi n = phi (suc n)否则您必须通过将phi^-1 0分配给phi 0来获取psi。然而，这个案例分析是Fin n的。

我认为通过交换相邻元素来表示排列组只是这个问题的一个不方便的表示。