Weak FunExt implies FunExt

[thchatzidiamantis]

Converse direction for #73. Also added a naive-funext axiom.

[emilyriehl]

The code looks good but the exposition could be improved. Start the new section with some text that explains what you are planning to do and how the proof will go. The citation to Rijke doesn't appear to be in the right place. If you are formalizing a specific result in that book, then you can use the title="blah" tag immediately before the definition that corresponds to that result. Here it appears you are citing an entire section, so I would do this in the body of the comment and not with a title.

Can we come up with a better name for "WeirdFunExt". Similarly how should I interpret the name of the first term you define? Feel free to ask questions about this on the zulip.

[thchatzidiamantis]

Changes to the exposition. I did not make any name changes on my own, I would be happy to discuss and rename as appropriate.

[emilyriehl]

We need a better name for WeirdFunExt, but let's fix this later.