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

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 就没有意义。但是引理本身并没有提到可判定的平等，所以我想我会尝试证明它而不把它作为一个假设。一周后的现在，我已经无计可施了，因为这看起来很“明显”，但又很难证明。

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

所以我的问题是:如果不假设元素类型，这是否可以证明？如果是这样的话，证明的一般结构是什么样子的，我很难获得想要同时归纳两个 FMSets 的证明来工作(因为我在尝试让路径根据需要排列时主要是猜测)。如果它在没有假设的情况下无法证明，是否可以证明它在某种形式上等同于必要的假设？

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 来获得 psi 0 到 phi 0。然而，这个案例分析是在 Fin n 上进行的。

我认为通过交换相邻元素来表示置换群只是对这个问题的一种不方便的表示。