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?
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.