The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

I am curious about the general question of: given a type in the
Calculus of Inductive Constructions, does there exist a unique term of
that type? And moreover, if there does, how to prove this in Coq?

Here is a simple example (in Coq 8.1 syntax), based on id_t, the type of
the polymorphic identity function id (Definition id (a:Type) (x:a) :
a := x.)

Definition id_t := forall (a : Type), a -> a.

(* This is not allowed:
Definition weird : id_t := fun (a : Set) (x : a) => match a with nat =>
0 | _ => x end. *)

Lemma uniqueness_of_id : exists! f:id_t, True.

I posit that all functions having type id_t must either:

a) be equal to id as defined above (note that I am assuming functional
extensional equality), or

b) be of the same form as "weird" above, and hence disallowed.

and hence uniqueness_of_id is true in CiC.

However, how would I prove this in Coq?

Would I need any axioms other than those in the Coq standard library?

Thanks,
-- 
Robin