1

我正在尝试为具有 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

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

4

1 回答 1

2

理想情况下你只能写

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-tofor的子句扩展它ε，_*_它应该可以解决。

顺便说一句，路径的顺序isSet'和Square不同使得这更加令人困惑，我想我会打开一个关于它的问题。

于 2019-08-26T07:48:59.533 回答