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?

functional extensionality. – ScarletAmaranth