-
Notifications
You must be signed in to change notification settings - Fork 70
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Explore what we want to call "isomorphisms" #1072
Comments
Hey! I'd just like to note that the notion of isomorphisms in precategories is not incoherent. Rather, it is coherent, but the definition is only coherent for set-level structures and doesn't generalize to higher structures without modifications. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
In #1056 (comment) @EgbertRijke raised the question whether we should keep with the type theory convention of having "isomorphisms" be in general maps with structure, or if we should reappropriate it for a well-behaved coherent concept.
For now we have the incoherent "isomorphisms in (large) (pre)categories" (invertible morphisms) and coherent "pointed isomorphisms" (biinvertible maps) are introduced in #1056.
The text was updated successfully, but these errors were encountered: