CODEWITHSUNDEEP
coqequalitydependent-type
Bob
Bob

Reputation: 1743

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?

Upvotes: 3

Views: 177

Answers (1)

András Kovács
András Kovács

Reputation: 30103

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.

Upvotes: 5

Related Questions