Можно ли доказать, что неравные не имеют значения без текста?

Question

Я могу тривиально доказать, что не равно не имеет отношения к расширению функции:

open import Relation.Binary.PropositionalEquality using (_≢_)
open import Relation.Binary using (Irrelevant)
open import Relation.Nullary.Negation using (contradiction)
open import Axiom.Extensionality.Propositional using (Extensionality)

postulate
  fun-ext : ∀ {ℓ₁ ℓ₂} → Extensionality ℓ₁ ℓ₂

≢-irrelevant : ∀ {a} {A : Set a} → Irrelevant {A = A} _≢_
≢-irrelevant {x} {y} [x≉y]₁ [x≉y]₂ = fun-ext (λ x≈y → contradiction x≈y [x≉y]₁)

Кажется невозможным доказать без символа, когда A - полиморф c, но возможно ли, когда A = ℕ или A = Bool * * 1006

Answer 1

Это не доказуемо без текста. Мы рассмотрели вопрос об изменении определения пустого типа , чтобы сделать их доказуемыми, однако это было сочтено слишком инвазивным изменением.