在 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

但是那里的路径不是唯一确定的"in the middle"所以统一不会解决它们。

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

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 中的路径顺序不同，这让这变得更加混乱，我想我会打开一个关于它的问题。

在 isSet 类型中构建具有约束的路径

Constructing a path with constraints in an isSet type

agda

homotopy-type-theory

cubical-type-theory