Formalizing equivalences without tears - cs.LO updates on arXiv.org
cs.LO updates on arXiv.orgarXiv:2408.11501v3 Announce Type: replace Abstract: This expository note describes two convenient techniques in the context of homotopy type theory for proving and formalizing that a given map is an equivalence. The first technique decomposes the map as a series of basic equivalences, while the second refines this approach using the 3-for-2 property of equivalences. The techniques are illustrated by proving a basic result in synthetic homotopy theory.
本文章由 flowerss 抓取自RSS，版权归源站点所有。
查看原文：Formalizing equivalences without tears - cs.LO updates on arXiv.org