Here's a request for some new material in the HoTT file on equivalences that might be a fun exercise for someone.
In the section on Invertible maps we define a type has-inverse and later in the section Invertible map data we define map-inverse-has-inverse. It would be nice to define has-inverse-map-inverse-has-inverse showing that this map has an inverse (proving that having an inverse is symmetric).
Then it would be great to apply to this to prove that section-is-equiv and retraction-is-equiv are equivalences. One of these will likely be easier than the other by the particular method we used to show that equivalences are invertible maps. But not we have homotopy-section-retraction-is-equiv showing that the two maps are homotopic, so once one is an equivalence the other is as well by is-equiv-homotopy or is-equiv-rev-homotopy.
emilyriehl
commented
1 year ago
Here's a request for some new material in the HoTT file on equivalences that might be a fun exercise for someone.
In the section on Invertible maps we define a type
has-inverseand later in the section Invertible map data we definemap-inverse-has-inverse. It would be nice to definehas-inverse-map-inverse-has-inverseshowing that this map has an inverse (proving that having an inverse is symmetric).Then it would be great to apply to this to prove that
section-is-equivandretraction-is-equivare equivalences. One of these will likely be easier than the other by the particular method we used to show that equivalences are invertible maps. But not we havehomotopy-section-retraction-is-equivshowing that the two maps are homotopic, so once one is an equivalence the other is as well byis-equiv-homotopyoris-equiv-rev-homotopy.I'm happy to chat about this further.