我可以简单地证明不等于与函数可扩展性无关:
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 是多态时,如果没有 funext,这似乎无法证明,但当 A = ℕ
或 A = Bool
时,这是否可能?
最佳答案
如果没有 funext,这是无法证明的。我们做了consider changing the definition of the empty type使这些可证明,但它被认为是一种过于侵入性的改变。
关于agda - 如果没有 funext,是否有可能证明不等于无关紧要?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/59891781/