search

agda / cubical

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

Where should `π₁(RP²)` be? #1016

Open ice1000 opened 1 year ago

ice1000 commented 1 year ago

Cubical.HITs.RPn.Base or Cubical.HITs.RPn.Properties?

felixwellen commented 1 year ago

I think Cubical.HITs.RPn.Properties or Cubical.Homotopy.Group is good.