agda - 在isSet类型中构造具有约束的正方形

这是基于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) = ?

集合是类群，因此我想我可以在最后一种情况下尝试与以前完全相同，只是高一维。但这就是我开始失败的地方：由于某种原因，不能使用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))

当然，我不声称现有的四个面孔是正确的。

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

最佳答案

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

为了找到它们，我们可以使用其他答案中的策略，但要高一个维度。首先，我们通过cong的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问题，经过一些清理后，我们得到：

      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中的路径是一个命题。

关于agda - 在isSet类型中构造具有约束的正方形，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/57775932/