search

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
378 stars 22 forks source link

The concept of homotopy type #185

Open marcbezem opened 1 year ago

marcbezem commented 1 year ago

Should be clarified somewhere in the book, currently Appendix B.3.

DanGrayson commented 1 year ago

Or we should not use it. The use most people in our field put it to conflicts with the classical definition, and equivalence class of spaces modulo homotopy equivalence.

bidundas commented 1 year ago

I agree that ”homotopy type” should have as small a place in the text as possible.

A thing I liked about univalence is that it made my colloquialism ”up to deformation” (which I’ve always favored when giving popularizations) into something precise.

Bjorn

On Jul 1, 2023, at 18:06, Daniel R. Grayson @.***> wrote:

Or we should not use it. The use most people in our field put it to conflicts with the classical definition, and equivalence class of spaces modulo homotopy equivalence.

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.