Timeline for What the differences between equivalence in HoTT and isomorphism in category？
Current License: CC BY-SA 4.0
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 19 at 10:39 | vote | accept | Hu_R | ||
| Aug 19 at 10:38 | comment | added | Hu_R | Oh, thanks a lot. I get it. Isomorphism/Equivalence is actually a function property, so we use function to define it. And in HoTT, the inhabitants of type is-isomorphism($f$) is non-uniqueness, so it has to use two functions $g$ and $h$. | |
| Aug 19 at 9:43 | history | answered | Naïm Favier | CC BY-SA 4.0 |