Structured isomorphism

Stream: Is there code for X?

[Robin Carlier]

Given F : C ⥤ D and d : D, we have CostructuredArrow F d for the category of maps F.obj c ⟶ d. I don’t see anything like StructuredIso to bundle the data of an isomorphism F.obj c ≅ d, did I miss it?
I’d rather not define such thing as a full subcategory of (Co)structured arrows where the map has an IsIso instance, because I’d like to keep the isomorphism as data.

[Robin Carlier]

(I guess there is the option of looking at CostructuredArrows on the functor on groupoid cores induced by F, but my experience with Core has been pretty bad so far).

[Joël Riou]

I do not think we have this category. The best is probably to introduce a new structure.

[Robin Carlier]

Well, StructuredIso it is then
(Also, regarding Core, I feel things would be better if it was a one-element field less centered about defeq abuse on its Hom field, should I also do that at some point?)

[Kim Morrison]

Robin Carlier said:

Well, StructuredIso it is then
(Also, regarding Core, I feel things would be better if it was a one-element field less centered about defeq abuse on its Hom field, should I also do that at some point?)

Yes, please!

[Robin Carlier]

Will try to do that within the week then.

[Robin Carlier]

Actually, it was easier than expected, #24987. Automation seems to like it better.
I did not expect file#CategoryTheory/Core to be a leaf file. I think I might as well go with structured arrows on Core for the StructuredIso structure.