search

HoTT / book

A textbook on informal homotopy type theory
2.02k stars 359 forks source link

Universal property of the circle #1125

Closed FernandoChu closed 1 year ago

FernandoChu commented 2 years ago

Solves https://github.com/HoTT/book/issues/1123 by defining the quasi-inverses.

mikeshulman commented 2 years ago

Thanks for this!

I wonder whether the derivation of $g \circ f \sim \mathsf{id}$ from the uniqueness principle could stand more explanation? In particular, regarding exactly why we get a $q$ of the dependent identity type mentioned in the uniqueness principle?

FernandoChu commented 1 year ago

Sorry for the delay (github didn't ping me it seems), and thanks for the comments. I've expanded on the suggested point.

FernandoChu commented 1 year ago

I don't think the failing check is because of my changes.