refactoring - 为什么我不能将部分框定义移动到本地绑定中?
问题描述
作为对此的后续,我意识到我需要使用异质组合来为部分盒子制作盖子。在这里,我删除了所有不必要的杂物:
{-# OPTIONS --cubical #-}
module _ where
open import Cubical.Core.Everything
open import Cubical.Foundations.Everything
postulate
A : Type
P : A → Type
PIsProp : ∀ x → isProp (P x)
prove : ∀ x → P x
x y : A
q : x ≡ y
a = prove x
b = prove y
prf : PathP (λ i → P (q i)) a b
prf = p
where
b′ : P y
b′ = subst P q a
r : PathP _ a b′
r = transport-filler (λ i → P (q i)) a
-- a b
-- ^ ^
-- | |
-- refl | | PIsProp y _ _
-- | |
--- a ---------> b′
-- r
p-faces : (i j : I) → Partial (i ∨ ~ i) (P (q i))
p-faces i j (i = i0) = a
p-faces i j (i = i1) = PIsProp y b′ b j
p : PathP (λ i → P (q i)) a b
p i = comp (λ j → P (q i)) ? (r i)
所以这里唯一剩下的漏洞是在 的定义中p
。当然,我想用 来填充它p-faces i
,因为这就是我定义它的原因。但是,这会导致 Universe 级别的错误:
p : PathP (λ i → P (q i)) a b
p i = comp (λ j → P (q i)) (p-faces i) (r i)
Agda.Primitive.SSet ℓ-zero != Agda.Primitive.SSetω
检查表达式
p-faces i
是否具有类型时(i₁ : I) → Partial (i ∨ ~ i) (P (q i))
但是,如果我内联p-faces
into的定义p
,它会进行类型检查;请注意,这还包括类型检查p-faces
(我不需要删除它)的定义,它只是导致这种类型错误的用法:p-faces
p : PathP (λ i → P (q i)) a b
p i = comp (λ j → P (q i)) (λ { j (i = i0) → a; j (i = i1) → PIsProp y b′ b j }) (r i)
p-faces
在 的定义中使用 有什么问题p
?在我未经训练的眼睛看来,它看起来像是一个永远不会超过的正常定义Type₀
解决方案
我看到你正在使用 agda/master!
以下内容也可以
p i = comp (λ j → P (q i)) (\ j -> p-faces i j) (r i)
随着--two-level
类型的引入comp
并transp
触发了宇宙多态性的排序分配问题,因此这里需要一些 eta 扩展来让 Agda 按照它想要的排序检查 lambda。
希望我们能尽快找到更好的解决方案。
推荐阅读
- javascript - 单击链接不起作用,而复制粘贴链接正常工作
- sql - 在我的查询中添加一个包含行数的列
- karate - 如果 json 字段具有特殊字符作为点,则访问 json 字段值
- c++ - 集合 vs 无序集合!哪个更好用?
- php - Mysql 没有返回任何行
- node.js - 使用带有反应的 Node.js Npm 包
- php - PHP 正则表达式在最后一次检查中部分失败
- python - 关于一个具体例子的for循环的一个简单问题
- sql-server - 错误:启用历史记录表时“无法继续执行,因为会话处于终止状态”
- java - 在 Android 上不使用 Dropbox API 从 Dropbox 下载 APK