Are constructors in the plain calculus of constructions disjoint and injective?

Question

Based on this answer, it looks like the calculus of inductive constructions, as used in Coq, has disjoint, injective constructors for inductive types.

In the plain calculus of constructions (i.e., without primitive inductive types), which uses impredicative encodings for types (e.g., ∏(Nat: *).∏(Succ: Nat → Nat).∏(Zero: Nat).Nat), is this still true? Can I always find out which "constructor" was used? Also, is injectivity (as in ∀a b.I a = I b → a = b) provable in Coq with Prop or impredicative Set?

This seems to cause trouble in Idris.

Answer 1

(I am not sure about all the points that you asked, so I am making this answer a community wiki, so that others can add to it.)

Just for completeness, let's use an impredicative encoding of the Booleans as an example. I also included the encodings of some basic connectives.

Definition bool : Prop := forall (A : Prop), A -> A -> A.

Definition false : bool := fun A _ Hf => Hf.

Definition true : bool := fun A Ht _ => Ht. 

Definition eq (n m : bool) : Prop :=
  forall (P : bool -> Prop), P n -> P m.

Definition False : Prop := forall (A : Prop), A.

We cannot prove that true and false are disjoint in CoC; that is, the following statement is not provable:

eq false true -> False.

This is because, if this statement were provable in CoC, we would be able to prove true <> false in Coq, and this would contradict proof irrelevance, which is a valid axiom to add. Here is a proof:

Section injectivity_is_not_provable.

  Variable Hneq : eq false true -> False.   (* suppose it's provable in CoC *)

  Lemma injectivity : false <> true.
  Proof.
  intros Heq.
  rewrite Heq in Hneq.
  now apply (Hneq (fun P x => x)).
  Qed.

  Require Import Coq.Logic.ProofIrrelevance.
  Fact contradiction : Logic.False.
  Proof.
  pose proof (proof_irrelevance bool false true) as H.
  apply (injectivity H).
  Qed.

End injectivity_is_not_provable.