Equivalences are closed under "transfinite composition"

UniMath / agda-unimath

The agda-unimath library

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

MIT License

219 stars 70 forks source link

Closed VojtechStep closed 5 months ago

VojtechStep commented 5 months ago

if a sequential diagram consists of equivalences, then injection maps into its colimit are also equivalences
as a corollary, sequential colimits of sequential diagrams of contractible types are contractible

Progress towards #1080