[Exercise 1.13] Solved double negation of excluded middle

[HyunggyuJang]

Using intuitionistic De Morgan's law.

[mikeshulman]

This is a perfectly good solution, of course. But I also like the direct solution, and if we include one I'd like to also include the other. Would you feel like writing out the direct solution too? If not, I can try to find the time.

[HyunggyuJang]

Like https://github.com/HoTT/HoTT/pull/1652/commits/cfbe48305dc45d7d8ad595d20a6034c6f8af11f6?

[HyunggyuJang]

Or is it okay with let the original solution as it is, and add newly added direct one with different name for comparison?

[mikeshulman]

Thanks! I was thinking of keeping them both with different names.

[HyunggyuJang]

Thanks! I was thinking of keeping them both with different names.

Got it!

[HyunggyuJang]

I’ll fix alignment issue in a minute.

[HyunggyuJang]

Done