search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

Whitehead's Lemma #1067

Closed owen-milner closed 10 months ago

owen-milner commented 10 months ago

Proof of Whitehead's lemma for truncated spaces (theorem 8.8.3 in the HoTT book).

owen-milner commented 10 months ago

Looking good:-) My comments are mainly just pointers to stuff already in the library.

Thanks!

mortberg commented 10 months ago

Have all comments been resolved? If so I can merge as soon as the CI is finished

mortberg commented 10 months ago

@aljungstrom confirmed that all comments are resolved, so I'll merge now