‘`hcomp`’的形象是图像的‘`hcomp`’吗？

Question

我正在努力填补以下程序中剩下的一个漏洞：

{-# 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 (doubleComp-faces (λ _ → base) (λ _ → base) i) (loop i) 
!=
fun NS-Iso (hcomp (doubleComp-faces (λ _ → N) W i) (E i))

Answer 1

我发现答案基本上是肯定的！

让我们在NS-Iso .rightInv (loop i)中为我们的目标添加一个本地绑定，以便监视以下类型：

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

因为我们有

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

goal的类型可归纳为：

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

现在到了关键的一步，对我的问题的实际答案：我们能把推入 E ∙ W**?**吗？

让我们在直接定义fun NS-Iso的点和路径之间或通过cong _ refl = refl知道其值的地方绘制波浪线

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

fun NS-Iso E ∙ W是内盒的盖子，是的，的图像确实是外盒的盖子。

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

以图形形式：

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

因此，我们现在可以减少fun NS-Iso应用程序：

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

我们最终可以用一个库函数doubleCompPath-filler来解决这个问题。

完整的代码：

  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

我不知道为什么我需要eta-展开goal和step1，但除此之外，Agda不承认它们满足边界条件。