为什么我不能将部分框定义移动到本地绑定中？

Question

作为的后续，我意识到我需要使用异质成分来为部分盒子制作盖子。在这里，我删除了所有不必要的垃圾：

{-# 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 填充它，因为这就是我定义它的原因。但是，这会导致宇宙级错误：

    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ω
when checking that the expression p-faces i has type
(i₁ : I) → Partial (i ∨ ~ i) (P (q i))

但是，如果我将 p-faces 的定义内联到 p 中，它会进行类型检查；请注意，这还包括对 p-faces 的定义进行类型检查（我不需要将其删除），只是 p-faces 的 usage 导致了此类型错误：

    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 的定义中使用 p-faces 有什么问题？在我未经训练的眼中，它看起来像一个正常的定义，永远不会超过 Type₀

Answer 1

我看到你在使用 agda/master!

以下方法也有效

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

随着 --two-level 的引入，comp 和 transp 的类型触发了 universe 多态性的排序赋值问题，所以这里需要一些 eta 扩展来让 Agda 检查lambda 随心所欲。

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

为什么我不能将部分框定义移动到本地绑定中？

Why can't I move a partial box definition into a local binding?

refactoring

referential-transparency

let

agda

cubical-type-theory