The Coq mailing list

[Dimitri Hendriks <diem AT xs4all.nl>]

Does it harm to assume extensional equality of functions in nat -> A 
to be closed under functions in (nat -> A) -> (nat -> A), in other words, 
does an axiom (forall f s t, s == t -> f s == f t) with == extensional 
equality,
lead to inconsistencies? And how to see that it is not provable, if that is 
the case at all? An incomplete proof attempt follows to see what is missing.

--
Dimitri

Section aa.

Variables (A : Set).

Definition eeq (s t : nat -> A) := 
 forall n, s n = t n.

Infix "==" := eeq  (at level 75, no associativity).

Definition shift (s : nat -> A) :=
 fun n => s (S n).

Lemma eeq_congr :
 forall f s t,
 s == t ->
 f s == f t.
intros f s t H n.
revert f.
induction n as [|n IH]; intro f.
2:apply IH with (f := fun s => shift (f s)) .
(*
 A : Set
 s : nat -> A
 t : nat -> A
 H : s == t
 f : (nat -> A) -> nat -> A
 ============================
  f s 0 = f t 0
*)