Почему я не могу переместить частичное определение блока в локальную привязку? - PullRequest
Новая
       87

Почему я не могу переместить частичное определение блока в локальную привязку?

1 голос
/ 07 августа 2020

В продолжение этого , я понял, что мне нужно использовать гетерогенную композицию, чтобы сделать крышку для частичной коробки. Здесь я удалил весь ненужный мусор: 

{-# 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ω

при проверке того, что выражение p-faces i имеет тип 

(i₁ : I) → Partial (i ∨ ~ i) (P (q i))

Однако, если Я вставляю определение p-faces в 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₀

1 Ответ

1 голос
/ 10 августа 2020

Я вижу, вы используете agda / master!

Следующее также могло бы работать

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

с введением --two-level типов comp и transp вызывают проблему с назначением сортировки для полиморфизма юниверса, поэтому здесь необходимо некоторое расширение eta, чтобы позволить Agda проверить лямбду нужного вида.

Надеюсь, мы скоро найдем лучшее решение .

...