The category of extensible structures

[avekens]

One result of the discussion in #1507 was the "category of extensible structures", which is already availabe in set.mm since March 2020 (in AV#s mathbox). Gérard proposed to move the corresponding subsection "The category of extensible structures" into the main body of set.mm. Meanwhile, I provided additional definitions and theorems for category theory (according to [Adamek]) which I think are quite useful (I have used or will use them in the context of Rings).

I would propose to move the whole section "Categories (extension)" of my mathbox into the main body of set.mm. Is there any objection against it? I think this would be in the spirit of David: looking at his recent contribution graph, it can be seen that the number of theorems in the mathboxes grow much faster than the number of theorems in the main body...

@nmegill @digama0 @benjub @tirix @david-a-wheeler what do you think?

[tirix]

I would agree with that. Even if the "category of extensible structures" is not a standard notion, I think it's useful in our own set.mm development. The other theorems from Adamek developed by Alexander completely make sense.

[nmegill]

Extensible structures are already nonstandard, and embedding them into categories seems weird. :) But I'll agree to move it up if no one else objects to it.

I think this would be in the spirit of David: looking at his recent contribution graph, it can be seen that the number of theorems in the mathboxes grow much faster than the number of theorems in the main body...

Well, I think usefulness and merit should be the main considerations. We already have the convention of moving things up when they are needed by 2 or more people. That is actually a requirement if we want to keep mathboxes independent.

Perhaps a large number of mathbox theorems can suggest a review of mathbox material, but I don't think it should necessarily be a goal in itself to import to theorems just to reduce the number. For example, while I haven't decided its fate yet, I don't anticipate that my mathbox will ever be part of the main set.mm because it's just too obscure a topic. And there are many theorems in other mathboxes that will never be imported for various reasons, for example, if they use a new axiom.

For cases like yours where there is no 2nd user, a review by several people as you have requested seems the right thing to do.

[benjub]

The section "Categories (extension)" contains some good work by @avekens (bravo!). OTOH, I'm not a fan, as you know, of extensible structures. So it's best for me to let others decide what is best concerning moving to Main.

Side remark: "essential uniqueness" means "uniqueness up to a unique isomorphism making the relevant diagram commute". For initial and terminal objects, you actually have uniqueness up to a unique isomophism. Existence of an isomorphism is not enough to grant "essential uniqueness". So there should be a strengthening of ~initoeu1 where the conclusion reads something like E! f f e. ( A ( Iso ` C ) B ).

[avekens]

By now, there is no objection, but also no clear vote for the proposal by the current reviewers (see comments above). I still want to ask, however, @digama0 and @david-a-wheeler for their opinion. If there is still no objection within the next days, I'll move the whole section "Categories (extension)" of my mathbox into the main body of set.mm.

@nmegill I fully agree that it cannot be a goal to move everything sometime from the mathboxes into the main body. I myself have experimental material in my mathbox which will/should never be moved into the main body.

[avekens]

Done with #1659