Search code examples
coqequalitydependent-type

Functional extensionality for John Major's equality

Is functional extensionality provable for John Major's equality (possibly relying on safe axioms)?

Goal forall A (P:A->Type) (Q:A->Type)
(f:forall a, P a) (g:forall a, Q a),
(forall a, JMeq (f a) (g a)) -> JMeq f g.

If not, is it safe to assume it as an axiom?

Solution

  • It's provable from usual function extensionality.

    Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.JMeq.

Theorem jmeq_funext
   A (P : A -> Type) (Q : A -> Type)
   (f : forall a, P a)(g : forall a, Q a)
   (h : forall a, JMeq (f a) (g a)) : JMeq f g.
Proof.
  assert (pq_eq : P = Q).
    apply functional_extensionality.
    exact (fun a => match (h a) with JMeq_refl => eq_refl end).
  induction pq_eq.
  assert (fg_eq : f = g).
    apply functional_extensionality_dep.
    exact (fun a => JMeq_rect (fun ga => f a = ga) eq_refl (h a)).
  induction fg_eq.    
  exact JMeq_refl.
Qed.