fredrik-bakke
commented
6 months ago 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.
In https://github.com/UniMath/agda-unimath/pull/1056#discussion_r1519953433 @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.