在 isSet 类型中构造带有约束的路径

Question

我正在尝试为具有 HIT 域的函数的结果中的相等性编写证明。因为函数是在 HIT 上定义的，所以相等性证明也必须处理路径情况。在这些情况下，Agda 报告了我需要构建的高维路径的大量限制；例如：

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₁

但是，有问题的 HIT 恰好是一个集合（在 isSet 意义上）。因此，我能想出的任何具有正确端点的路径都与解决给定约束的路径无法区分。因此，更具体地说，假设我在范围内再引入两个术语：

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

如何使用这两个定义来填补漏洞？

Answer 1

理想情况下你会写

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

但是“中间”的路径不是唯一确定的，因此统一无法解决它们。

幸运的是，还有另一种便宜的方法可以找到它们，让我先修正一些定义：

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 = ?

我们当前的目标应该是回答当我们减少时会发生什么 \ i j -> from-to (el^ m i) j，幸运的是，我们可以改写该表达式，使推理可以做我们想做的事情。

我们要求cong from-to (e^l m)的类型：

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

现在我们可以将它与fillSquare 的类型匹配并解决我们的目标：

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

还有一个问题，对from-to (ε * m) 的递归调用不会被视为终止，但如果您使用from-to 的子句对ε 和_*_ 进行扩展，它应该可以解决。

顺便说一句，isSet' 和 Square 中路径的顺序不同，这让这更加混乱，我想我会打开一个关于它的问题。