The loop of any circle is nontrivial

UniMath / agda-unimath

The agda-unimath library

https://unimath.github.io/agda-unimath/

MIT License

211 stars 67 forks source link

The loop of any circle is nontrivial #1115

Closed EgbertRijke closed 2 months ago

EgbertRijke commented 2 months ago

This PR shows that the loop on any circle is nontrivial. I also changed "fundamental cover" to "universal cover" because that seemed to be the conventional name.

fredrik-bakke commented 2 months ago

Yay!

EgbertRijke commented 2 months ago

Lol this is not a milestone :P

fredrik-bakke commented 2 months ago

I will merge this without having the comments resolved so that I can use the result. Thanks again! :)