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.

John Major 平等的功能外延

Functional extensionality for John Major's equality

coq

equality

dependent-type