[TYPES] Inconsistency and non dependent sum elimination

Param Jyothi Reddy paramr at gmail.com
Mon Jul 30 01:30:03 EDT 2007

This is in the context for impredicative Prop and predicative type
hierarchy. The base type system is PTS. I was reading that in presence of
dependent elimination for sum type, elimination from Prop sort to Type sort
can lead to inconsistency in logic. Would it also hold true if we allow only
non-dependent elimination i.e. eliminating Prop into Type without depedency.

SumDependentCase Rule: (inconsistent)
     C[z] : Type   c1[x] : C[Inj_1(x)]   c2[y] : C[Inj_2(y)]   k : A+B
A + B : Prop

[G, x:A, y:B, z:A+B]
     +~(k, [x:A]c1[x], [y:B]c2[y], [z:A+B]C[z]) : C[k]

SumDependentCase Rule: (consistent??)
     C : Type   c1 : C   c2 : C   k : A+B      A + B : Prop

[G, x:A, y:B, z:A+B]
     +~(k, [x:A]c1, [y:B]c2, z:A+B) : C

Would same be true for dependent Sum (Sigma) type? (instead of using direct
second projection, using a case similar to the one given for Sum case).

Thanks in advance,

More information about the Types-list mailing list