Is the image of a `hcomp` the `hcomp` of images?

Question

I am trying to fill the remaining one hole in the following program:

{-# OPTIONS --cubical #-}
module _ where

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

data S1 : Type where
  base : S1
  loop : base ≡ base

data NS : Type where
  N : NS
  S : NS
  W : S ≡ N
  E : N ≡ S

module _ where
  open Iso

  NS-Iso : Iso NS S1
  NS-Iso .fun N = base
  NS-Iso .fun S = base
  NS-Iso .fun (W i) = base
  NS-Iso .fun (E i) = loop i
  NS-Iso .inv base = N
  NS-Iso .inv (loop i) = (E ∙ W) i
  NS-Iso .leftInv N = refl
  NS-Iso .leftInv S = sym W
  NS-Iso .leftInv (W i) = λ j → W (i ∨ ~ j)
  NS-Iso .leftInv (E i) = λ j → compPath-filler E W (~ j) i
  NS-Iso .rightInv base = refl
  NS-Iso .rightInv (loop i) = ?

The type of the hole is:

fun NS-Iso (inv NS-Iso (loop i)) ≡ loop i

inv NS-Iso (loop i) of course definitionally equal to (E ∙ W) i, but what is then fun NS-Iso ((E ∙ W) i)? Is there some kind of homomorphism / continuity / similar property with which I can use the definitions of fun NS-Iso (E i) and fun NS-Iso (W i) to figure out what it is?

Since fun NS-Iso (E i) = loop i and fun NS-Iso (W i) = base, I thought this might be a valid filling (pun intended) of the hole:

  NS-Iso .rightInv (loop i) = λ j → compPath-filler loop (refl {x = base}) (~ j) i

But that gives a type error:

hcomp (doubleComp-faces (λ _ → base) (λ _ → base) i) (loop i) 
!=
fun NS-Iso (hcomp (doubleComp-faces (λ _ → N) W i) (E i))

Answer 1

I have found that the answer is, basically, yes!

Let's add a local binding of our goal in NS-Iso .rightInv (loop i) just to keep an eye on the type:

  NS-Iso .rightInv (loop i) = goal
    where
      goal : (fun NS-Iso ∘ inv NS-Iso) (loop i) ≡ loop i
      goal = ?

Since we have

  NS-Iso .inv (loop i) = (E ∙ W) i

the type of goal reduces to:

      step1 : fun NS-Iso ((E ∙ W) i) ≡ loop i

And now comes the crucial step, the actual answer to my question: can we push in fun NS-Iso into E ∙ W?

Let's draw wavy lines between the points and paths where fun NS-Iso is directly defined, or where we know its value by cong _ refl = refl:

      base                                   base
        ^  ~                                ~  ^
        |     ~                          ~     |
        |        ~                    ~        |
        |          N                N          |
        |          ^                ^          |
   refl | ~~~ refl |                |  W ~~~~~ | refl
        |          |                |          |
        |          N -------------> S          |
        |        ~         E          ~        |
        |     ~            ~             ~     |
        |  ~               ~                ~  |
      base --------------------------------> base
                         loop

E ∙ W is the lid of the inner box, and it turns out yes, its image by fun NS-Iso is indeed the lid of the outer box:

      step2 : (cong (fun NS-Iso) E ∙ (cong (fun NS-Iso) W)) i ≡ loop i

In graphical form:

                           ?
      base - - - - - - - - - - - - - - - - - > base
        ^  ~                                ~  ^
        |     ~                          ~     |
        |        ~        E ∙ W       ~        |
        |          N - - - - - - -> N          |
        |          ^                ^          |
   refl | ~~~ refl |                |  W ~~~~~ | refl
        |          |                |          |
        |          N -------------> S          |
        |        ~         E          ~        |
        |     ~            ~             ~     |
        |  ~               ~                ~  |
      base -------------------------------> base
                         loop

So we can reduce the fun NS-Iso applications now:

      step3 : (loop ∙ (λ _ → base)) i ≡ loop i

which we can finally solve with a library function doubleCompPath-filler.

The complete code:

  NS-Iso .rightInv (loop i) = goal
    where
      step3 : (loop ∙ (λ _ → base)) i ≡ loop i
      step3 = cong (λ p → p i) (symP (ompPath-filler loop (λ _ → base)))

      step2 : (cong (fun NS-Iso) E ∙ (cong (fun NS-Iso) W)) i ≡ loop i
      step2 = step3

      step1 : fun NS-Iso ((E ∙ W) i) ≡ loop i
      step1 j = step2 j

      goal : (fun NS-Iso ∘ inv NS-Iso) (loop i) ≡ loop i
      goal j = step1 j

I don't know why I needed to eta-expand goal and step1, but otherwise Agda doesn't recognize that they meet the boundary conditions.