The Coq mailing list

[���� <hskiowa AT kaist.ac.kr>]

Dear coq-club:

 

I am cautious about assuming the following:

 

Axiom fun_eq : forall (A B : Type) (f g: A -> B) (a : A), (forall a : A, f a = g a) -> f = g.

 

<or>

 

Parameter realize : forall {A:Type}, (A->Prop)->A.
Axiom realization : forall {A:Type} (P:A->Prop), (exists! x:A, P x) -> P (realize P).

(* Note that "unique existence (exists!)" is assumed instead of "mere existence (exist).")

 

What are expected dangers of assuming each?

 

 

Sincerely,

 

Hyung Sun Kim