Как преобразовать аксиому J в форму с фиксированным аргументом? - PullRequest
Новая
       10

Как преобразовать аксиому J в форму с фиксированным аргументом?

0 голосов
/ 26 января 2019

Я пытался доказать, что true ≡ false -> Empty предполагает аксиому J. Он определяется как: 

J : Type
J = forall 
  {A : Set} 
  {C : (x y : A) → (x ≡ y) → Set} → 
  (c : ∀ x → C x x refl) → 
  (x y : A) → 
  (p : x ≡ y) → 
  C x y p

Моя попытка прошла так: 

bad : J → true ≡ false -> Empty
bad j e = j Bool (λ { true _ _ => Unit; false _ _ => Empty }) _

Теперь, чтобы продолжить доказательство, мне понадобился термин c : ∀ x -> C x x refl. Поскольку я создал C, он становится c : ∀ x -> (λ { true _ _ => Unit; false _ _ => Empty } x x refl. Тогда я застрял. c не может уменьшаться дальше, потому что мы не знаем значение x. Я не смог завершить это доказательство. Но есть другая версия J: 

J' : Type
J' = forall 
  {A : Set} 
  {x : A}
  {C : (y : A) → (x ≡ y) → Set} → 
  (c : C x refl) → 
  (y : A) → 
  (p : x ≡ y) → 
  C y p

С этим, эта проблема решена, потому что t может быть исправлено, чтобы быть true. Это уменьшает аргумент c до Unit, который мы можем предоставить. Мой вопрос: можем ли мы конвертировать предыдущую версию в более позднюю? То есть мы можем построить термин fix_x : J → J'? В общем ли это (т.е. можно ли преобразовать индексы в параметры)?

1 Ответ

0 голосов
/ 26 января 2019

Во-первых, в отношении true ≡ false -> Empty: это недоказуемо, если вы можете исключить только в Set0 с помощью J, поэтому вам нужно универсальное полиморфное или большое определение. Я пишу некоторые предварительные замечания здесь: 

{-# OPTIONS --without-K #-}

open import Relation.Binary.PropositionalEquality
open import Level

data Bool : Set where true false : Bool
data Empty : Set where
record Unit : Set where
  constructor tt

JTy : ∀ {i j} → Set _
JTy {i}{j} =
  {A   : Set i}
  (P   : (x y : A) → (x ≡ y) → Set j) →
  (pr  : ∀ x → P x x refl) →
  {x y : A} →
  (p   : x ≡ y) →
  P x y p

J : ∀ {i}{j} → JTy {i}{j}
J P pr {x} refl = pr x

J₀ = J {zero}{zero}

Теперь true ≡ false -> Empty или subst - единственная необходимая вещь для *1009*: 

transp : ∀ {i j}{A : Set i}(P : A → Set j){x y} → x ≡ y → P x → P y
transp P = J (λ x y _ → P x -> P y) (λ _ px → px)

true≢false : true ≡ false → Empty
true≢false e = transp (λ {true → Unit; false → Empty}) e tt

Рассматривая теперь доказательство указанного J' из J, я знаю о трех решениях, и каждое использует различные особенности из теории окружения.

Самое простое - использовать вселенные для абстрагирования по индуктивному мотиву: 

JTy' : ∀ {i j} → Set _
JTy' {i}{j} =
  {A  : Set i}
  {x  : A}
  (P  : ∀ y → x ≡ y → Set j)
  (pr : P x refl)
  {y  : A}
  (p  : x ≡ y)
  → P y p

JTy→JTy' : (∀ {i j} → JTy {i}{j}) → ∀ {i}{j} → JTy' {i}{j}
JTy→JTy' J {i} {j} {A} {x} P pr {y} e =
  J (λ x y e → (P : ∀ y → x ≡ y → Set j) → P x refl → P y e)
     (λ x P pr → pr) e P pr

Если мы хотим использовать только фиксированный уровень вселенной, то это немного сложнее. Следующее решение, иногда называемое «стягиваемыми синглетонами», нуждается в Σ -типах, но больше ничего: 

open import Data.Product

JTy→JTy'withΣ : JTy {zero}{zero} → JTy' {zero}{zero}
JTy→JTy'withΣ J {A} {x} P pr {y} e =
  J (λ {(x , r) (y , e) _ → P x r → P y e})
    (λ _ px → px)
    (J (λ x y e → (x , refl) ≡ (y , e))
       (λ _ → refl)
       e)
    pr

Существует решение, которое даже не требует Σ -s, но требует бета-правила для J, которое говорит, что J P pr {x} refl = pr x. Неважно, является ли это правило определенно или просто пропозициональным равенством, но конструкция проще, когда оно определенно, так что давайте сделаем это. Обратите внимание, что я не использую никакой вселенной, кроме Set0. 

transp₀ = transp {zero}{zero}

transp2 : ∀ {A : Set}{B : A → Set}(C : ∀ a → B a → Set)
        {x y : A}(e : x ≡ y){b} → C x b → C y (transp₀ B e b)
transp2 {A}{B} C {x}{y} e {b} cxb =
  J₀ (λ x y e → ∀ b → C x b → C y (transp₀ B e b)) (λ _ _ cxb → cxb) e b cxb

JTy→JTy'noΣU : JTy' {zero}{zero}
JTy→JTy'noΣU {A} {x} P pr {y} e =
    transp₀ (P y) (J₀ (λ x y e → transp₀ (x ≡_) e refl ≡ e) (λ _ → refl) e)
      (transp2 {A} {λ y → x ≡ y} P e pr)

С философской точки зрения третья версия является наиболее "консервативной", поскольку она предполагает только J. Добавление бета-правила на самом деле не является дополнительной вещью, поскольку предполагается, что оно всегда (определенно или пропозиционально) для _≡_.

можно ли преобразовать индексы в параметры?

Если у вас есть пропозициональное равенство, то все индексы могут быть преобразованы в параметры и зафиксированы в конструкторах с использованием доказательств равенства.

...