Равенство по зависимым типам записей

Как правило, равенство сигм эквивалентно сигме равенств:

Σ-≡-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' , 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}))
  ?

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

ℕ-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; действительно, решение Дорчарда работает только с включенной аксиомой K), потому что, если мы попытаемся доказать обязательность отверстия в целом, без ссылки на ℕ, тогда нам понадобится лемма, которая недоказуема в интенсиональной теории типа Мартина-Лёфа:

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 _ _)

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

Rec-cong : {x y : Rec}
    -> (val x ≡ val y)
    -> ((λ {n} -> inc x {n}) ≡ (λ{n} -> inc y {n}))
    -> (succ x ≅ succ y)
    -> x ≡ y
Rec-cong {x} {y}  prf1 prf2 prf3 with prf1 | prf2 | prf3
Rec-cong {x} {.x} prf1 prf2 prf3      refl | refl | refl = refl

incR0 : forall {x : Rec} -> incR x 0 ≡ x
incR0 {x} = Rec-cong {incR x 0} {x} (incRVal {x}) (incRinc {x}) (incRsucc {x})

Я приветствовал бы лучшее решение!