Coq类型论中两类外延相等公理的等价性问询

First, let's recap the axioms you've defined, along with the theorem you already proved showing Axiom2 implies Axiom1:

Your Axioms and Existing Proof #

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.

(* You already showed Axiom2 is stronger than Axiom1 *)
Theorem Axiom2ImpAxiom1 : Axiom2 -> Axiom1.
Proof. intros H a b f g H'. apply H. exact H'. Qed.

The Core Answer #

Absolutely! These two axioms are equivalent in Coq's type theory. The reverse implication (Axiom1 → Axiom2) can be proven cleanly with a clever use of sigma types to bridge dependent and non-dependent function types.

Concise Proof of Axiom1 → Axiom2 #

Here's a straightforward proof that doesn't require extra library imports:

Theorem Axiom1ImpAxiom2 : Axiom1 -> Axiom2.
Proof.
  intros H a B f g pointwise_eq.
  (* Wrap dependent function outputs into a sigma type to create non-dependent functions *)
  let sigma := {x : a & B x} in
  pose (f' := fun x => existT _ x (f x)) : a -> sigma;
  pose (g' := fun x => existT _ x (g x)) : a -> sigma.
  
  (* Prove f' and g' are pointwise equal *)
  assert (f'_eq_g' : forall x, f' x = g' x).
  { intros x. simpl. rewrite pointwise_eq. reflexivity. }
  
  (* Apply Axiom1 to get equality of the non-dependent functions *)
  apply H in f'_eq_g'.
  
  (* Unpack the equality to recover f = g *)
  extensionality x.
  inversion f'_eq_g'.
  reflexivity.
Qed.

How This Works #

The key trick is converting dependent functions f and g into non-dependent counterparts (f' and g') by pairing each input x with its corresponding output f x/g x using a sigma type ({x : a & B x}). Once we have non-dependent functions, Axiom1 gives us their equality. We then use the extensionality tactic (or manual inversion if you prefer) to extract the equality of the original dependent functions from that result.

内容的提问来源于stack exchange，提问作者Sven Williamson