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?

Neopythagoreanism

As I understand it, you need to provide a path between paths in the last two clauses there. However, you already have an assertion that FMSet is a set (i.e. homotopy level 0), so all equalities are equal (all paths have paths between them). FMSetElimProp is a proof of this fact. So you can use it anywhere you need an equality between equalities of FMSets. – Flatworm

@Flatworm You interpretation of FMSetElimProp.f is very impressive! Unfortunately, I must be very stupid because I only see a complicated statement there. Could you elaborate in an answer how you arrive at this interpretation? – Neopythagoreanism

I haven't put an answer because I'm not sure of how correct I am! – Flatworm

But basically: in the comm clause of the unitr-++ function, you need to provide an equality of equalities. You can prove this manually (as far as I know), but since you've already specified that FMSet is h-level 0 (that's what adding the trunc constructor to the type does), you don't have to, since all equalities of h-level 0 types are automatically equal. So you just provide a proof of that fact (which is proven already in the cubical library), which is called FMSetElimProp. – Flatworm

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.

Phalarope