[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Sequents and entailment rather than implication and universal quantification. coherent mathematics The problem is with infinite sets: one could prove function extensionality for functions with domain a finite set. Same goes with choice. I don't believe in function extensionality, or the existence of function sets, dependent function sets, universal quantification, implication, and negation anymore. category: redirected to nlab