如何将 J 公理转换为固定参数形式？

Question

我试图证明 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' 吗？这在一般情况下是否成立（即，索引可以转换为参数）？

Answer 1

首先，关于true ≡ false -> Empty：如果你只能用J消去成Set0，这是无法证明的，所以你需要一个宇宙多态或大定义。我在这里写一些预备知识：

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

现在，transport 或 subst 是 true ≡ false -> Empty 唯一需要的东西：

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

如果我们只想使用固定的宇宙层次，那就有点复杂了。以下解决方案，有时称为 "contractible singletons"，需要 Σ 类型，但仅此而已：

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 的 beta 规则，即 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)

从哲学上讲，第三个版本是最 "conservative"，因为它只假设 J。 beta 规则的添加并不是一个额外的东西，因为它总是假设（定义上或命题上）适用于 _≡_.

can indices be converted to parameters?

如果你有命题相等性，那么所有索引都可以转换为参数，并使用相等性证明固定在构造函数中。

如何将 J 公理转换为固定参数形式？

How to convert the J axiom to the fixed-argument form?

agda