Is it possible to extract the second element of Sigma on the calculus of constructions with simple inconsistent axioms?

Question

It seems to be impossible to extract the second element of Sigma on the Calculus of Constructions. Moreover, it seems like there is no known, simple way to extend the Calculus of Constructions with dependent eliminations without losing consistency. How can one, thus, exploit a simple but inconsistent axiom (such as Type : Type or unrestricted recursion such as μ) to extract the second element of Sigma?

That is, given the following Sigma constructor:

Sigma =
  λ A : *
  λ B : A -> *
  λ a : A
  λ b : B
  λ Data : *
  λ Sigma :
    ∀ fst : A
    ∀ snd : B fst
    Data
  Sigma a b

In a language equivalent to the Calculus of Constructions, except with Type : Type or some other simple inconsistent axiom, is it possible to implement a function that, given a term such as Sigma Nat (\x -> Nat) 3 6, extracts the second value, 6?

Answer 1

In the context of a type theory such as Martin-Löf type theory or the Calculus of Constructions, by "inconsistency" we usually mean logical inconsistency: being able to derive a term contra of type forall T : Type, T. In this case, any other type T becomes inhabited: it suffices to apply contra to it.

Unfortunately, in most type theories, being inhabited tells us nothing about convertibility, or definitional equality, because there is no type expresses that two terms x and y are convertible. This means that there is no way of deriving terms

fst : Sigma A B -> A
snd : forall s : Sigma A B, B (fst s)

such that fst (Sigma _ _ x y) simplifies to x and snd (Sigma _ _ x y) simplifies to y by appealing to a logical contradiction. (I have abused notation a bit and used Sigma for both the constructor and the type.) You can, however, use contra to postulate the existence of fst and snd and assert that the corresponding equations hold propositionally.

In plain CoC, we say that two terms x1 and x2 are propositionally equal if there is a term of type

forall T, T x1 -> T x2

(This is sometimes known as Leibniz equality: two terms are equal if every predicate that holds of the first one holds of the second one.) Stating a similar for snd is somewhat more complicated, because snd (Sigma _ _ x y) and y do not have the same types (the former is of type B (fst (Sigma _ _ x y)), while the latter is of type B x). We can remedy this by asserting simplification lemmas for fst and snd simultaneously:

forall (T : forall x : A, B x -> Type),
  T (fst (Sigma _ _ x y)) (snd (Sigma _ _ x y)) -> 
  T x y

Edit

Concerning your comment: since convertibility usually cannot be expressed with a type, we need to modify its definition in the type theory to have a true sigma type with first and second projections -- a more delicate operation than simply positing that certain axioms hold. There are some systems that allow this, such as Dedukti, a proof checker developed at Inria.