coq - John Major 平等的功能外延

Question

John Major 等式是否可以证明函数外延性(可能依赖于安全公理)？

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.

如果不是，将其假设为公理是否安全？

Answer 1

它可以从通常的函数扩展性得到证明。

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.