Constructing squares with constraints in an isSet type

Question

This is in continuation of this question, based on this answer. Using the technique explained by Saizan, and factoring my fromList-toList proof a bit to avoid the problematic recursion, I managed to fill in all but one cases of fromList-toList. I think it's easiest if I just show everything I have:

{-# OPTIONS --cubical #-}

module _ where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything hiding (assoc)

data FreeMonoid {ℓ} (A : Type ℓ) : Type ℓ where
  [_]  : A → FreeMonoid A
  ε    : FreeMonoid A
  _·_  : FreeMonoid A → FreeMonoid A → FreeMonoid A

  εˡ     : ∀ x      → ε · x ≡ x
  εʳ     : ∀ x      → x · ε ≡ x
  assoc  : ∀ x y z  → (x · y) · z ≡ x · (y · z)

  squash : isSet (FreeMonoid A)

infixr 20 _·_

open import Cubical.Data.List hiding ([_])

module ListVsFreeMonoid {ℓ} {A : Type ℓ} (AIsSet : isSet A) where
  listIsSet : isSet (List A)
  listIsSet = isOfHLevelList 0 AIsSet

  toList : FreeMonoid A → List A
  toList [ x ] = x ∷ []
  toList ε = []
  toList (m₁ · m₂) = toList m₁ ++ toList m₂
  toList (εˡ m i) = toList m
  toList (εʳ m i) = ++-unit-r (toList m) i
  toList (assoc m₁ m₂ m₃ i) = ++-assoc (toList m₁) (toList m₂) (toList m₃) i
  toList (squash m₁ m₂ p q i j) = listIsSet (toList m₁) (toList m₂) (cong toList p) (cong toList q) i j

  fromList : List A → FreeMonoid A
  fromList [] = ε
  fromList (x ∷ xs) = [ x ] · fromList xs

  toList-fromList : ∀ xs → toList (fromList xs) ≡ xs
  toList-fromList [] = refl
  toList-fromList (x ∷ xs) = cong (x ∷_) (toList-fromList xs)

  fromList-homo : ∀ xs ys → fromList xs · fromList ys ≡ fromList (xs ++ ys)
  fromList-homo [] ys = εˡ (fromList ys)
  fromList-homo (x ∷ xs) ys = assoc [ x ] (fromList xs) (fromList ys) ∙ cong ([ x ] ·_) (fromList-homo xs ys)

  fromList-toList-· : ∀ {m₁ m₂ : FreeMonoid A} → fromList (toList m₁) ≡ m₁ → fromList (toList m₂) ≡ m₂ → fromList (toList (m₁ · m₂)) ≡ m₁ · m₂
  fromList-toList-· {m₁} {m₂} p q = sym (fromList-homo (toList m₁) (toList m₂)) ∙ cong₂ _·_ p q

  fromList-toList : ∀ m → fromList (toList m) ≡ m
  fromList-toList [ x ] = εʳ [ x ]
  fromList-toList ε = refl
  fromList-toList (m₁ · m₂) = fromList-toList-· (fromList-toList m₁) (fromList-toList m₂)
  fromList-toList (εˡ m i) = isSet→isSet' squash
    (fromList-toList-· refl (fromList-toList m))
    (fromList-toList m)
    (λ i → fromList (toList (εˡ m i)))
    (λ i → εˡ m i)
    i
  fromList-toList (εʳ m i) = isSet→isSet' squash
    (fromList-toList-· (fromList-toList m) refl)
    (fromList-toList m)
    ((λ i → fromList (toList (εʳ m i))))
    (λ i → εʳ m i)
    i
  fromList-toList (assoc m₁ m₂ m₃ i) = isSet→isSet' squash
    (fromList-toList-· (fromList-toList-· (fromList-toList m₁) (fromList-toList m₂)) (fromList-toList m₃))
    (fromList-toList-· (fromList-toList m₁) (fromList-toList-· (fromList-toList m₂) (fromList-toList m₃)))
    (λ i → fromList (toList (assoc m₁ m₂ m₃ i)))
    (λ i → assoc m₁ m₂ m₃ i)
    i
  fromList-toList (squash x y p q i j) = ?

Sets are groupoids so I thought I can try doing exactly the same in that last case as before, just one dimension higher. But this is where I start failing: for some reason, two of the six faces cannot be constructed using the fact that FreeMonoid is a set. In more concrete terms, in the two missing faces in the code below, if I just try to refine by putting isSet→isSet' squash in the hole (with no more arguments specified), I already get "cannot refine".

Here's my code for the four faces that I managed to fill in:

  fromList-toList (squash x y p q i j) = isGroupoid→isGroupoid' (hLevelSuc 2 _ squash)
    {fromList (toList x)}
    {x}
    {fromList (toList y)}
    {y}
    {fromList (toList (p i))}
    {p i}
    {fromList (toList (q i))}
    {q i}

    {λ k → fromList (toList (p k))}
    {fromList-toList x}
    {fromList-toList y}
    {p}
    {λ k → fromList (toList (squash x y p q k i))}
    {fromList-toList (p i)}
    {fromList-toList (q i)}
    {λ k → squash x y p q k i}
    {λ k → fromList (toList (p (i ∧ k)))}
    {λ k → p (i ∧ k)}
    {λ k → fromList (toList (q (i ∨ ~ k)))}
    {λ k → q (i ∨ ~ k)}

    ?
    f2
    f3
    ?
    f5
    f6
    i
    j
    where
      f2 = isSet→isSet' squash
        (fromList-toList x) (fromList-toList (p i))
        (λ k → fromList (toList (p (i ∧ k)))) (λ k → p (i ∧ k))

      f3 = isSet→isSet' squash
        (fromList-toList y) (fromList-toList (q i))
        (λ k → fromList (toList (q (i ∨ ~ k)))) (λ k → q (i ∨ ~ k))

      f5 = isSet→isSet' squash (fromList-toList x) (fromList-toList y)
        (λ k → fromList (toList (p k)))
        (λ k → p k)

      f6 = isSet→isSet' squash (fromList-toList (p i)) (fromList-toList (q i))
        (λ k → fromList (toList (squash x y p q k i)))
        (λ k → squash x y p q k i)

The reported types of the two missing faces are:

Square 
  (λ k → fromList (toList (p (i ∧ k))))
  (λ k → fromList (toList (p k)))
  (λ k → fromList (toList (squash x y p q k i)))
  (λ k → fromList (toList (q (i ∨ ~ k))))

and

Square 
  (λ k → p (i ∧ k)) 
  p 
  (λ k → squash x y p q k i)
  (λ k → q (i ∨ ~ k))

Of course, I make no claims that the existing four faces are correct.

So I guess my question is either, what are the two missing faces, or alternatively, what are the correct 6 faces?

Answer 1

The six faces are not arbitrary ones between the endpoints, they are given by the type and other clauses of fromList-toList.

To find them out we can use the strategy from the other answer but one dimension higher. First we declare a cube define through conging of fromList-toList:

fromList-toList (squash x y p q i j) = { }0
    where
      r : Cube ? ? ? ? ? ?
      r = cong (cong fromList-toList) (squash x y p q)

We can then ask agda to solve the six ?s by C-c C-s and after a little cleanup we get:

      r : Cube (λ i j → fromList (toList (squash x y p q i j)))
               (λ i j → fromList-toList x j)
               (λ i j → fromList-toList y j)
               (λ i j → squash x y p q i j)
               (λ i j → fromList-toList (p i) j)
               (λ i j → fromList-toList (q i) j)
      r = cong (cong fromList-toList) (squash x y p q)

in this case we are able to use those faces directly as there's no problem with recursion.

  fromList-toList (squash x y p q i j)
    = isGroupoid→isGroupoid' (hLevelSuc 2 _ squash)
               (λ i j → fromList (toList (squash x y p q i j)))
               (λ i j → fromList-toList x j)
               (λ i j → fromList-toList y j)
               (λ i j → squash x y p q i j)
               (λ i j → fromList-toList (p i) j)
               (λ i j → fromList-toList (q i) j)
               i j

By the way, if you are going to prove more equalities by induction it may pay off to implement a more general function first:

elimIntoProp : (P : FreeMonoid A → Set) → (∀ x → isProp (P x))
             → (∀ x → P [ x ]) → P ε → (∀ x y → P x → P y → P (x · y)) → ∀ x → P x

as paths in FreeMonoid A are a proposition.