构建者是否在Agda中脱节？(或如何反驳inj 1 x≡inj₂y)

Question

我需要一个更多的引理来证明这inj? x ? inj? y是荒谬的,作为关于?Agda中不相交联合类型()的更大定理的一部分.

这个结果将直接来自两个构造函数?,即inj?和inj?不相交.那是阿格达的情况吗？我该如何证明？

这是完整的引理:

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Sum


lemma : ? {a b} {A : Set a} {B : Set b} {x : A} {y : B} ? ¬ inj? x ? inj? y
lemma eq = ?

Answer 1

数据类型构造函数是不相交的.我会说这是阿格达类型系统元理论中的一个定理.

您可以尝试使用eq证明(C-c C-c),并且Agda会发现矛盾:

lemma : ? {a b} {A : Set a} {B : Set b} {x : A} {y : B} ? ¬ inj? x ? inj? y
lemma ()

这种快乐的类型检查.