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.
Proof.
    intros H a b f g H'. apply H. exact H'.
Qed.

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?

upvote
  flag
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 https://github.com/HoTT/HoTT/blob/c54a967526bb6293a0802cb2bed32e0b4dbe5cdc/contrib/old/Funext.v#L113-L358 which uses slightly different terminology.

upvote
  flag
Thanks very much Jason ! – Sven Williamson

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