EPIT-2020
EPIT-2020 copied to clipboard
HoTT
EPIT 2020 - Spring School on Homotopy Type Theory
Including a solution for the last exercise (using quite a few lemmas from the library though).
Add solution for lemma `set_not_set`. The proof is based on a slightly different version of the lemma `two_equiv_two` that was already proven. Remark: This solution compiles with Coq 8.13.1 and...
Link copied from [Zulip](https://hott.zulipchat.com/#narrow/stream/283194-EPIT-2020-School-on-HoTT/topic/youtube.20channel/near/234120113).
