Search code examples
coq

On the relative strength of some extensional equality axioms

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?

Solution

  • 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.