Constructing a path with constraints in an isSet t

问题:

I am trying to write a proof for an equality in results of a function with a HIT domain. Because the function is defined over a HIT, the proof of equality also has to handle path cases. In those cases, Agda reports a ton of constraints on the higher-dimensional path I'm required to construct; for example:

Goal: fromList (toList m) ≡ εˡ m i
————————————————————————————————————————————————————————————
i      : I
m      : FreeMonoid A
AIsSet : isSet A
A      : Type ℓ
ℓ      : Level
———— Constraints ———————————————————————————————————————————
(hcomp
 (λ { j ((~ i ∨ i) = i1)
        → (λ { (i = i0) → fromList (toList ε ++ toList a₁)
             ; (i = i1)
                 → cong₂ _·_ (fromList-toList ε) (fromList-toList a₁) (i1 ∧ j)
             })
          _
    ; j (i1 = i0)
        → outS (inS (fromList-homo (toList ε) (toList a₁) (~ i)))
    })
 (outS (inS (fromList-homo (toList ε) (toList a₁) (~ i)))))
  = (?1 (AIsSet = AIsSet₁) (m = a₁) (i = i0) i)
  : FreeMonoid A₁
(fromList-toList a₁ i)
  = (?1 (AIsSet = AIsSet₁) (m = a₁) (i = i1) i)
  : FreeMonoid A₁

However, the HIT in question happens to be a set (in the isSet sense). So, any path I can come up with that has the right endpoints will be indistinguishable from one that also solves the given constraints. So in more concrete terms, suppose I bring two more terms in scope:

fillSquare : isSet' (FreeMonoid A)
rightEndpointsButConstraintsDon'tHold : fromList (toList m) ≡ εˡ m i

How can I use these two definitions to fill the hole?

回答1:

Ideally you'd just be able to write

rightEndpointsButConstraintsDon'tHold j = fillSquare _ _ _ _ i j

but the paths there are not uniquely determined "in the middle" so unification won't solve them.

Luckily there's another cheap way to find them out, let me first fix some definitions:

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything

data FreeMonoid (A : Set) : Set where
  [_]    : A → FreeMonoid A
  ε      : FreeMonoid A
  _*_    : FreeMonoid A → FreeMonoid A → FreeMonoid A
  e^l : ∀ m → ε * m ≡ m

data List (A : Set) : Set where

variable
  A : Set

fromList : List A → FreeMonoid A
toList : FreeMonoid A → List A

fillSquare : isSet' (FreeMonoid A)

from-to : ∀ (m : FreeMonoid A) → fromList (toList m) ≡ m
from-to (e^l m i) j = ?

Our current goal is supposed to answer what happens when we reduce \ i j -> from-to (el^ m i) j, luckily we can rephrase that expression in a way where inference will do what we want.

We ask for the type of cong from-to (e^l m):

PathP (λ i₁ → fromList (toList (e^l m i₁)) ≡ e^l m i₁)
(from-to (ε * m)) (from-to m)

Now we can match it with the type of fillSquare and solve our goal:

from-to (e^l m i) j 
  = fillSquare (from-to (ε * m)) (from-to m) 
               (λ i → fromList (toList (e^l m i))) (e^l m)
               i j

There's still a catch, the recursive call to from-to (ε * m) will not be seen as terminating, but if you expand that using the clauses of from-to for ε and _*_ it should work out.

Btw, the order of the paths in isSet' and Square differ which made this extra confusing, I think I'll open an issue about it.