Finite multisets as a HIT in Cubical Agda

Question

In the standard library of Cubical Agda, there are finite multisets whose elegant definitions I reproduce below:

{-# 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

The proof that [] is a right-neutral element uses the abstract lemma FMSetElimProp.f which I do not understand. Therefore I am trying to make a direct proof, but I am stuck. Here is my attempts:

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) = {!!}

Am I on the right track? How can I finish this proof?

Answer 1

The two SO questions that answer this are this one for comm and this one for trunc. Like you, I've struggled with the same frustration: if all these types are Sets, why do I need to write ANYTHING, let alone something complicated, to prove some 2-paths?!?!

So, first of all, from the first linked answer, let's start at

comm x y xs i ++ ys = ?

and ask Agda what is the type of the hole.

Goal: comm x y (xs ++ []) i ≡ comm x y xs i

Well that sounds promising because we know that comm x y (xs ++ []) ≡ comm x y xs simply by xs + [] ≡ xs inductively. So, let's ask what exactly that would buy us. Put cong (comm x y) (unitr-++ xs) in the hole and ask for its type:

Have:

PathP
     (λ i → x ∷ y ∷ unitr-++ xs i ≡ y ∷ x ∷ unitr-++ xs i)
     (comm x y (xs ++ [])) (comm x y xs)

Then @Saizan's answer instructs us to produce the Square with exactly these faces:

isSet→isSet' trunc
  (comm x y (xs ++ []))
  (comm x y xs)
  (λ j → x ∷ y ∷ unitr-++ xs i)
  (λ j → y ∷ x ∷ unitr-++ xs i)

and choose the right internal point on it, giving us the filling of our hole:

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

For the second missing clause, i.e. in

unitr-++ (trunc xs1 xs2 p q i j) 

following the linked answer's recommendation, we can ask Agda for the faces of the cube we want to construct:

r : Cube ? ? ? ? ? ?
r = cong (cong unitr-++) (trunc xs1 xs2 p q)

By using C-c C-s in all six face holes, Agda tells us:

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)

so now we know exactly which cube to construct (using the fact that Sets are also Groupoids, as witnessed by 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

By now, on one hand, we can be happy that we're done, but on the other hand, we are pissed off because this answer was all "look at this other answer and do exactly that", "look at this other answer and do exactly that", but surely if you can do EXACTLY that, even though your type, and your function, and your function property, are NOT the same as mine was when I asked my original question, then there is something that should be abstracted away here, right?

And that is what FMSetElimProp does. It implements ALL this machinery above, for FMSet specifically, but for all functions and all properties of those functions, in one fell swoop. So you DON'T have to look at this answer and the two linked ones and do all this OVER and OVER and OVER again, when in fact at the end it shouldn't make a difference anyway since all the constructed paths are path-equivalent anyway.