agda – 依赖记录类型的平等

Σ-≡-intro :
  ? {α β}{A : Set α}{B : A → Set β}{a a' : A}{b : B a}{b' : B a'}
  → (Σ (a ≡ a') λ p → subst B p b ≡ b') → (a,b) ≡ (a',b')
Σ-≡-intro (refl,refl) = refl

Σ-≡-elim :
  ? {α β}{A : Set α}{B : A → Set β}{a a' : A}{b : B a}{b' : B a'}
  → (a,b') → Σ (a ≡ a') λ p → subst B p b ≡ b'
Σ-≡-elim refl = refl,refl

我们可以将引入规则专门化并使其适应Rec,并且还可以对它进行调整,并且仅用实际依赖项替换(我使定义更加明确和压缩,因为我的孔类型更加清晰)：

open import Data.Nat
open import Relation.Binary.PropositionalEquality

record Rec : Set where
  constructor rec
  field val : ?
        inc : ? -> ?
        succ : inc 0 ≡ val
open Rec

incR : Rec -> ? -> Rec
incR x m = rec (val x + m) (λ n → inc x n + m) (cong (_+ m) (succ x))

Rec-≡-intro :
  ? {v v' : ?} {i i' : ? → ?}{s : i 0 ≡ v}{s' : i' 0 ≡ v'}(p : v ≡ v')(q : i ≡ i')
  → subst? (λ v i → i 0 ≡ v) p q s ≡ s'
  → rec v i s ≡ rec v' i' s'
Rec-≡-intro refl refl refl = refl

postulate
  ext : ? {α β} → Extensionality α β -- comes from PropositionalEquality
  runit : {n : ?} -> n + 0 ≡ n

我们可以使用Rec-≡-intro来证明Rec的等式：

incR0 : ? x -> incR x 0 ≡ x
incR0 x = Rec-≡-intro
  (runit {val x})
  (ext (λ n → runit {inc x n}))
  ?

剩下的洞有一个非常讨厌的类型,但我们基本上可以忽略它,因为equality的平等证明是命题,i.即相同值之间的所有相等证明都是相等的.换句话说,?是一组：

?-set : {n m : ?}(p p' : n ≡ m) → p ≡ p'
?-set refl refl = refl

incR0 : ? x -> incR x 0 ≡ x
incR0 x = Rec-≡-intro
  (runit {val x})
  (ext (λ n → runit {inc x n}))
  (?-set _ _)

我相信这里的所有证明最终都必须使用一些等同于?-set(或公理K的语句;实际上,dorchard的解决方案仅适用于启用公理K),因为如果我们试图一般地证明漏洞义务,而不参考?那么我们需要一个在强烈的Martin-L?f型理论中无法证明的引理：

lem :
  ? {A : Set}{z : A}{f i : A → A}(q? : f (i z) ≡ (i z))(q? : (λ x → f (i x)) ≡ i)
  → subst? (λ v i → i z ≡ v) q? q? refl ≡ refl
lem q? q? = {!!}

我在MLTT中似乎无法证明,因为我们可以在HoTT中找到反例.

如果我们假设公理K,我们有证据不相关,可以在这里使用：

proof-irrelevance : ? {a} {A : Set a} {x y : A} (p q : x ≡ y) → p ≡ q
proof-irrelevance refl refl = refl

lem :
  ? {A : Set}{z : A}{f i : A → A}(q? : f (i z) ≡ (i z))(q? : (λ x → f (i x)) ≡ i)
  → subst? (λ v i → i z ≡ v) q? q? refl ≡ refl
lem q? q? = proof-irrelevance _ _

但这有点傻,因为现在我们不妨填补我们原来的洞：

incR0 : ? x -> incR x 0 ≡ x
incR0 x = Rec-≡-intro
  (runit {val x})
  (ext (λ n → runit {inc x n}))
  (proof-irrelevance _ _)