All Questions
Tagged with coq constructive-mathematics
1 question
52
votes
3
answers
7k
views
Function extensionality: does it make a difference? why would one keep it out of the axioms?
Yesterday I was shocked to discover that function extensionality (the statement that if two functions $f$ and $g$ on the same domain satisfy $f\left(x\right) = g\left(x\right)$ for all $x$ in the ...