1

作为对此的后续，我意识到我需要使用异质组合来为部分盒子制作盖子。在这里，我删除了所有不必要的杂物：

{-# 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-facesinto的定义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₀

4

1 回答 1

1

我看到你正在使用 agda/master！

以下内容也可以

p i = comp (λ j → P (q i)) (\ j -> p-faces i j) (r i)

随着--two-level类型的引入comp并transp触发了宇宙多态性的排序分配问题，因此这里需要一些 eta 扩展来让 Agda 按照它想要的排序检查 lambda。

希望我们能尽快找到更好的解决方案。

于 2020-08-10T07:49:18.913 回答