Given the following axioms:

Definition Axiom1 : Prop := forall (a b:Type) (f g: a -> b),
    (forall x, f x = g x) -> f = g.

Definition Axiom2 : Prop := forall (a:Type) (B:a -> Type) (f g: forall x, B x),
    (forall x, f x = g x) -> f = g.

One can easily show that Axiom2 is a stronger axiom than Axiom1:

Theorem Axiom2ImpAxiom1 : Axiom2 -> Axiom1.
    intros H a b f g H'. apply H. exact H'.

Does anyone know if (within the type theory of Coq), these two axioms are in fact equivalent or whether they are known not to be. If equivalent, is there a simple Coq proof of the fact?

Look into functional extensionality. – ScarletAmaranth

1 Answers 11

up vote 2 down vote accepted

Yes, the two axioms are equivalent; the key is to go through fun x => existT B x (f x) and fun x => existT B x (g x), though there's some tricky equality reasoning that has to be done. There's a nearly complete proof at which uses slightly different terminology.

Thanks very much Jason ! – Sven Williamson

Not the answer you're looking for? Browse other questions tagged or ask your own question.