立方Agda构造NS与S1同构时hcomp性质及证明洞填充问题

hcomp经过函数映射后的像，是否等于对hcomp各组成部分分别映射后再构造hcomp得到的结果？

正在补全如下开启立方类型论选项的Agda程序中剩余的唯一证明洞：

{-# 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) = ?

当前证明洞的类型为：

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

根据定义可知inv NS-Iso (loop i)等价于(E ∙ W) i，待明确两个问题：

• fun NS-Iso ((E ∙ W) i)的实际计算结果是什么
• 是否存在同态、连续性或相关性质，可以通过已知的fun NS-Iso (E i)、fun NS-Iso (W i)定义直接推导上述结果

已知两个路径的映射结果：

• fun NS-Iso (E i) = loop i
• fun NS-Iso (W i) = base

曾尝试使用如下代码填充证明洞：

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

该写法触发类型错误，错误提示两边的hcomp项不匹配：

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

内容的提问来源于stack exchange，提问作者Cactus