How to prove element addition is injective for a cubical finite multi set?

Question

I'm playing around with the type of finite multisets as defined in the cubical standard library here: 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)

I was able to reproduce the proofs for count extensionality and one of my lemmas I showed that you can remove a element from both sides of an equality and keep the equality.

It was similar to this one: 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)

My proofs weren't using the same syntax but in the core libraries syntax it was

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

where the proof is using remove1-≡-lemma path composed on both side of a path which is the argument path functionally composed with remove1 x.

This requires the type of the values to have decidable equality as remove1 doesn't make sense without it. But the lemma itself doesn't mention decidable equality, and so I thought I would try to prove it without having that as a hypothesis. Its now a week later and I'm at my wits end because this seems so 'obvious' but so stubborn to prove.

I'm thinking that my intuition about this being provable may be coming from my classical math background, and so it doesn't follow constructively/contiuously.

So my question is: Is this provable with no assumptions on the element type? If so what would the general structure of the proof look like, I have had trouble getting proofs that want to induct over the two FMSets simultaneously to work (as I'm mostly guessing when trying to get paths to line up as necessary). If it is not provable with no assumptions, is it possible to show that it is equivalent in some form to the necessary assumptions?

Answer 1

I can't offer a proof but an argument why it should be provable without assuming decidability. I think finite multisets can be represented as functions Fin n -> A and equality between multisets f and g is given by a permutation phi : Fin n ~ Fin n, (that is invertible functions on Fin n) such that f o phi = g. Now

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

If phi : Fin (suc n) ~ Fin (suc n) proves that a :: f = a :: g you can construct a psi : Fin n ~ Fin n which proves that f = g. If phi 0 = 0 then psi n = phi (suc n) otherwise you have to obtain psi by assigning phi^-1 0 to phi 0. However this case analysis is on Fin n.

I think representing the permutation group by swapping adjacent elements is just an inconvenient representation for this problem.