search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
44 stars 12 forks source link

equivalences are embeddings #102

Closed jonalfcam closed 1 year ago

jonalfcam commented 1 year ago

For a few things I want to do, it will be useful to have the statement that equivalences are embeddings in the HoTT section of the library. I'm working on this now.

emilyriehl commented 1 year ago

If I understand what you want correctly, this is there already:

https://rzk-lang.github.io/sHoTT/hott/04-half-adjoint-equivalences.rzk/#equivalences-are-embeddings

jonalfcam commented 1 year ago

Thanks. I have no idea how I missed this.

jonalfcam commented 1 year ago

I''ll close this out.