Andrej Bauer

Upon a quick reading it looks like we could replace the offending definition with `f'(rat q) = f q`, could we not?

Ugh, we're committed to not reordering theorems. What to do?

I thought humor was not allowed on GitHub.

Your advisor and your PhD committee will be happier with an article than a blog post, trust me.

And an excuse to not write the article at all.

I have in the past used _truth value_ where it was customary to say "propostion". For instance $\Omega$ in a topos is the object of _truth values_, although I heard...

My brain is probably a bit skewed by computer science. I suspect computer scientists don't distinguish much between "proposition" and "boolean formula", but maybe I am just personally sloppy. In...

"Every truth value is either _true_ or _false_" is precisely excluded middle. Intuitionistic logic however only validates "No truth value is different from both _true_ and _false_". This is perhaps...

Now that I think about this, it is not so clear how it cold be done. I was thinking of some sort of "bisection" method. Suppose we introduce new envrionments...

I agree there is no automagic. What is the least amount of manual work that is needed? Also, we need a scheme that protects us from ourselves. Here's a possiblity:...