在 isSet 类型中构造带有约束的正方形

Question

这是this question 的延续，基于this answer。使用 Saizan 解释的技术，并考虑我的 fromList-toList 证明以避免有问题的递归，我设法填写了所有 fromList-toList 的案例。我认为如果我只展示我所拥有的一切是最简单的：

{-# OPTIONS --cubical #-}

module _ where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything hiding (assoc)

data FreeMonoid {ℓ} (A : Type ℓ) : Type ℓ where
  [_]  : A → FreeMonoid A
  ε    : FreeMonoid A
  _·_  : FreeMonoid A → FreeMonoid A → FreeMonoid A

  εˡ     : ∀ x      → ε · x ≡ x
  εʳ     : ∀ x      → x · ε ≡ x
  assoc  : ∀ x y z  → (x · y) · z ≡ x · (y · z)

  squash : isSet (FreeMonoid A)

infixr 20 _·_

open import Cubical.Data.List hiding ([_])

module ListVsFreeMonoid {ℓ} {A : Type ℓ} (AIsSet : isSet A) where
  listIsSet : isSet (List A)
  listIsSet = isOfHLevelList 0 AIsSet

  toList : FreeMonoid A → List A
  toList [ x ] = x ∷ []
  toList ε = []
  toList (m₁ · m₂) = toList m₁ ++ toList m₂
  toList (εˡ m i) = toList m
  toList (εʳ m i) = ++-unit-r (toList m) i
  toList (assoc m₁ m₂ m₃ i) = ++-assoc (toList m₁) (toList m₂) (toList m₃) i
  toList (squash m₁ m₂ p q i j) = listIsSet (toList m₁) (toList m₂) (cong toList p) (cong toList q) i j

  fromList : List A → FreeMonoid A
  fromList [] = ε
  fromList (x ∷ xs) = [ x ] · fromList xs

  toList-fromList : ∀ xs → toList (fromList xs) ≡ xs
  toList-fromList [] = refl
  toList-fromList (x ∷ xs) = cong (x ∷_) (toList-fromList xs)

  fromList-homo : ∀ xs ys → fromList xs · fromList ys ≡ fromList (xs ++ ys)
  fromList-homo [] ys = εˡ (fromList ys)
  fromList-homo (x ∷ xs) ys = assoc [ x ] (fromList xs) (fromList ys) ∙ cong ([ x ] ·_) (fromList-homo xs ys)

  fromList-toList-· : ∀ {m₁ m₂ : FreeMonoid A} → fromList (toList m₁) ≡ m₁ → fromList (toList m₂) ≡ m₂ → fromList (toList (m₁ · m₂)) ≡ m₁ · m₂
  fromList-toList-· {m₁} {m₂} p q = sym (fromList-homo (toList m₁) (toList m₂)) ∙ cong₂ _·_ p q

  fromList-toList : ∀ m → fromList (toList m) ≡ m
  fromList-toList [ x ] = εʳ [ x ]
  fromList-toList ε = refl
  fromList-toList (m₁ · m₂) = fromList-toList-· (fromList-toList m₁) (fromList-toList m₂)
  fromList-toList (εˡ m i) = isSet→isSet' squash
    (fromList-toList-· refl (fromList-toList m))
    (fromList-toList m)
    (λ i → fromList (toList (εˡ m i)))
    (λ i → εˡ m i)
    i
  fromList-toList (εʳ m i) = isSet→isSet' squash
    (fromList-toList-· (fromList-toList m) refl)
    (fromList-toList m)
    ((λ i → fromList (toList (εʳ m i))))
    (λ i → εʳ m i)
    i
  fromList-toList (assoc m₁ m₂ m₃ i) = isSet→isSet' squash
    (fromList-toList-· (fromList-toList-· (fromList-toList m₁) (fromList-toList m₂)) (fromList-toList m₃))
    (fromList-toList-· (fromList-toList m₁) (fromList-toList-· (fromList-toList m₂) (fromList-toList m₃)))
    (λ i → fromList (toList (assoc m₁ m₂ m₃ i)))
    (λ i → assoc m₁ m₂ m₃ i)
    i
  fromList-toList (squash x y p q i j) = ?

集合是 groupoids，所以我想我可以尝试在最后一种情况下做与以前完全相同的事情，只是高一维。但这就是我开始失败的地方：由于某种原因，无法使用FreeMonoid 是一个集合这一事实来构造六个面中的两个。更具体地说，在下面代码中缺少的两个面中，如果我只是尝试通过将isSet→isSet' squash 放入孔中来进行细化（没有指定更多参数），我已经得到“无法细化”。

这是我设法填写的四个面孔的代码：

  fromList-toList (squash x y p q i j) = isGroupoid→isGroupoid' (hLevelSuc 2 _ squash)
    {fromList (toList x)}
    {x}
    {fromList (toList y)}
    {y}
    {fromList (toList (p i))}
    {p i}
    {fromList (toList (q i))}
    {q i}

    {λ k → fromList (toList (p k))}
    {fromList-toList x}
    {fromList-toList y}
    {p}
    {λ k → fromList (toList (squash x y p q k i))}
    {fromList-toList (p i)}
    {fromList-toList (q i)}
    {λ k → squash x y p q k i}
    {λ k → fromList (toList (p (i ∧ k)))}
    {λ k → p (i ∧ k)}
    {λ k → fromList (toList (q (i ∨ ~ k)))}
    {λ k → q (i ∨ ~ k)}

    ?
    f2
    f3
    ?
    f5
    f6
    i
    j
    where
      f2 = isSet→isSet' squash
        (fromList-toList x) (fromList-toList (p i))
        (λ k → fromList (toList (p (i ∧ k)))) (λ k → p (i ∧ k))

      f3 = isSet→isSet' squash
        (fromList-toList y) (fromList-toList (q i))
        (λ k → fromList (toList (q (i ∨ ~ k)))) (λ k → q (i ∨ ~ k))

      f5 = isSet→isSet' squash (fromList-toList x) (fromList-toList y)
        (λ k → fromList (toList (p k)))
        (λ k → p k)

      f6 = isSet→isSet' squash (fromList-toList (p i)) (fromList-toList (q i))
        (λ k → fromList (toList (squash x y p q k i)))
        (λ k → squash x y p q k i)

两个缺失人脸的报告类型为：

Square 
  (λ k → fromList (toList (p (i ∧ k))))
  (λ k → fromList (toList (p k)))
  (λ k → fromList (toList (squash x y p q k i)))
  (λ k → fromList (toList (q (i ∨ ~ k))))

和

Square 
  (λ k → p (i ∧ k)) 
  p 
  (λ k → squash x y p q k i)
  (λ k → q (i ∨ ~ k))

当然，我并没有声称现有的四张脸是正确的。

所以我想我的问题是，两个缺失的面孔是什么，或者，正确的 6 个面孔是什么？

Answer 1

这六个面不是端点之间的任意面，它们由fromList-toList的类型和其他子句给出。

要找出它们，我们可以使用另一个答案中的策略，但维度更高。首先我们通过conging 的fromList-toList 声明一个立方体定义：

fromList-toList (squash x y p q i j) = { }0
    where
      r : Cube ? ? ? ? ? ?
      r = cong (cong fromList-toList) (squash x y p q)

然后我们可以让 agda 用C-c C-s 解决六个?s，经过一点清理后我们得到：

      r : Cube (λ i j → fromList (toList (squash x y p q i j)))
               (λ i j → fromList-toList x j)
               (λ i j → fromList-toList y j)
               (λ i j → squash x y p q i j)
               (λ i j → fromList-toList (p i) j)
               (λ i j → fromList-toList (q i) j)
      r = cong (cong fromList-toList) (squash x y p q)

在这种情况下，我们可以直接使用这些面孔，因为递归没有问题。

  fromList-toList (squash x y p q i j)
    = isGroupoid→isGroupoid' (hLevelSuc 2 _ squash)
               (λ i j → fromList (toList (squash x y p q i j)))
               (λ i j → fromList-toList x j)
               (λ i j → fromList-toList y j)
               (λ i j → squash x y p q i j)
               (λ i j → fromList-toList (p i) j)
               (λ i j → fromList-toList (q i) j)
               i j

顺便说一句，如果你要通过归纳证明更多的等式，那么首先实现一个更一般的函数可能会有所回报：

elimIntoProp : (P : FreeMonoid A → Set) → (∀ x → isProp (P x))
             → (∀ x → P [ x ]) → P ε → (∀ x y → P x → P y → P (x · y)) → ∀ x → P x

FreeMonoid A 中的路径是一个命题。