The Coq mailing list

[Ralph Matthes <Ralph.Matthes AT irit.fr>]

Le vendredi 25 novembre 2011 à 15:00 +0100, Dimitri Hendriks a écrit :
> 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.

In my work on Coq formalizations of logic for nested datatypes, I saw no
harm in restricting the lemmas to functionals that preserve extensional
equality. The examples I considered afterwards met this restriction, and
so nothing was lost. Of course, it would be nicer to "live" in a
universe where this is taken for granted, see e.g. the work on
observational type theory. My point here is that computer-aided proof
developments do not suffer so much if they are based on several
technical assumptions that one might wish to get rid of once and for
all.

Best regards,    Ralph Matthes