proof - 有限多集作为 Cubical Agda 中的 HIT
问题描述
在 Cubical Agda 的标准库中,有一些有限的多重集,我在下面重现了它们的优雅定义:
{-# OPTIONS --cubical --safe #-}
open import Cubical.Foundations.Prelude
infixr 20 _∷_
data FMSet (A : Set) : Set where
[] : FMSet A
_∷_ : (x : A) → (xs : FMSet A) → FMSet A
comm : ∀ x y xs → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
trunc : isSet (FMSet A)
_++_ : ∀ {A : Set} -> FMSet A → FMSet A → FMSet A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
comm x y xs i ++ ys = comm x y (xs ++ ys) i
trunc xs1 xs2 p q i j ++ ys =
trunc (xs1 ++ ys) (xs2 ++ ys) (cong (_++ ys) p) (cong (_++ ys) q) i j
[]
作为右中性元素的证明使用了FMSetElimProp.f
我不理解的抽象引理。因此,我试图直接证明,但我被卡住了。这是我的尝试:
unitr-++ : ∀ {A : Set} (ys : FMSet A) → ys ++ [] ≡ ys
unitr-++ [] = refl
unitr-++ (y ∷ ys) = cong ((y ∷_)) (unitr-++ ys)
unitr-++ (comm x y xs i) = cong₂ {!comm x y!} (unitr-++ xs) refl
unitr-++ (trunc xs1 xs2 p q i j) = {!!}
我在正确的轨道上吗?我怎样才能完成这个证明?
解决方案
回答这个问题的两个 SO 问题是this 一个 forcomm
和this 一个 fortrunc
。和你一样,我也遇到了同样的挫折:如果所有这些类型都是Set
s,为什么我需要写任何东西,更不用说复杂的东西来证明一些 2 路径?!?!
所以,首先,从第一个链接的答案开始,让我们从
comm x y xs i ++ ys = ?
并问阿格达什么是洞的类型。
目标:
comm x y (xs ++ []) i ≡ comm x y xs i
comm x y (xs ++ []) ≡ comm x y xs
好吧,这听起来很有希望,因为我们只是通过xs + [] ≡ xs
归纳知道这一点。所以,让我们问一下这到底会给我们带来什么。放入cong (comm x y) (unitr-++ xs)
孔中并询问其类型:
有:
PathP (λ i → x ∷ y ∷ unitr-++ xs i ≡ y ∷ x ∷ unitr-++ xs i) (comm x y (xs ++ [])) (comm x y xs)
然后@Saizan 的回答指示我们Square
用这些面孔制作:
isSet→isSet' trunc
(comm x y (xs ++ []))
(comm x y xs)
(λ j → x ∷ y ∷ unitr-++ xs i)
(λ j → y ∷ x ∷ unitr-++ xs i)
并在其上选择正确的内部点,填充我们的洞:
unitr-++ (comm x y xs i) j = isSet→isSet' trunc
(comm x y (xs ++ []))
(comm x y xs)
(λ j → x ∷ y ∷ unitr-++ xs j)
(λ j → y ∷ x ∷ unitr-++ xs j)
j i
对于第二个缺失的子句,即在
unitr-++ (trunc xs1 xs2 p q i j)
按照链接答案的建议,我们可以向 Agda 询问我们要构建的立方体的面:
r : Cube ? ? ? ? ? ?
r = cong (cong unitr-++) (trunc xs1 xs2 p q)
通过C-c C-s
在所有六个面孔中使用,Agda 告诉我们:
r : Cube (λ i j → trunc xs1 xs2 p q i j ++ [])
(λ i j → unitr-++ xs1 j)
(λ i j → unitr-++ xs2 j)
(λ i j → trunc xs1 xs2 p q i j)
(λ i j → unitr-++ (p i) j)
(λ i j → unitr-++ (q i) j)
所以现在我们确切地知道要构造哪个立方体(使用Set
s 也是Groupoid
s 的事实,由 见证hLevelSuc 2 _
):
unitr-++ (trunc xs1 xs2 p q i j) = isGroupoid→isGroupoid' (hLevelSuc 2 _ trunc)
(λ i j → trunc xs1 xs2 p q i j ++ [])
(λ i j → unitr-++ xs1 j)
(λ i j → unitr-++ xs2 j)
(λ i j → trunc xs1 xs2 p q i j)
(λ i j → unitr-++ (p i) j)
(λ i j → unitr-++ (q i) j)
i
j
到现在为止,一方面,我们可以很高兴我们已经完成了,但另一方面,我们很生气,因为这个答案都是“看看这个另一个答案并做到这一点”,“看看这个另一个答案并做到这一点”,但如果你能做到这一点,即使你的类型、你的函数和你的函数属性与我问我最初的问题时的不同,那么肯定有一些事情应该是在这里抽象出来,对吧?
这就是它的FMSetElimProp
作用。它FMSet
一举实现了上述所有这些机制,特别是针对所有功能和这些功能的所有属性。因此,您不必查看这个答案和两个链接的答案,然后一遍又一遍地做所有这些,而实际上,由于所有构造的路径都是路径等效的,因此最终它不应该有所作为反正。
推荐阅读
- regex - 正则表达式包含不应该匹配的匹配
- function - 基于返回类型的 Fortran 泛型函数
- r - 无法分配大小为 2928.7 Gb 的向量
- tensorflow - UnimplementedError: Fused conv implementation 目前不支持分组卷积
- sql - 如何更新从其数据源设置为在 Oracle Apex 中查看的记录?
- javascript - 如何在单击提交时从 Django 中的数据库中获取数据?
- prometheus - PromQL 中具有时间偏移的两个指标之间的差异
- data-structures - 双数组特里与三重数组特里
- phpmyadmin - phpMyAdmin 不显示登录表单
- java - 如何调度 JSP 页面?