Constructing a path with constraints in an isSet type

Question

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?

Canadianism

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

Khedive

Is there some annotation I can put on from-to so that the termination checker is willing to look a bit deeper, instead of having to inline it? – Canadianism

How does this technique generalize to higher-dimensional cases? For example, suppose my FreeMonoid datatype has a constructor squash: isSet (FreeMonoid A). Then in from-to (squash x y p q i j) k , would I be using fillSquare (not clear how), or would I aim for for a Cube via hLevelSuc 2? – Canadianism

You would do a cube with hLevelSuc 2, you should also look into isOfHLevel→isOfHLevelDep if the type is dependent. – Khedive