Add "accessible" and related notions

[ykawase5048]

I have added "accessble" and several related properties:

• (basic): accessible, ℵ₁-accessible, finitely accessible
• (dual): coaccessible, locally copresentable
• (related to sifted colimits): generalized variety, multialgebraic
• (accessible with some limit): locally multipresentable, locally finitely multipresentable, locally polypresentable
• (multilimits): multilimits, multiterminal object, multicolimits, multiinitial object
• (size): countable, essentially countable

I had expected that non-accessibility of $\mathbf{Set}^{\mathrm{op}}$ would be inferred automatically, but it wasn’t, so I manually assigned the property. Could this be a bug?

---

Comment by Martin: This PR will now be closed because we will merge its copy #97 instead.

[ScriptRaccoon]

Thank you! 🚀

I will have a look at it.

I have resolved the merge conflicts (the main branch changed a bit too much since yesterday) and force pushed the changes. You need to run git pull --rebase to get the current state.

For future PRs: how comfortable are you with resolving merge conflicts yourself?

[ykawase5048]

I have resolved the merge conflicts (the main branch changed a bit too much since yesterday) and force pushed the changes. You need to run git pull --rebase to get the current state.

Thanks!

For future PRs: how comfortable are you with resolving merge conflicts yourself?

I think I can resolve merge conflicts myself, but I’m not deeply familiar with git, so I would of course be very happy if you prefer to handle them!

[ykawase5048]

There is a very interesting issue: It is independent of our foundation, ZFC with two Grothendieck universes, whether the category of free abelian groups is accessible; see [Makkai-Pare, Section5.5] or MathStackExchange. So, we would need to add the third option "undecidable" for properties.

[ScriptRaccoon]

Meta comment: I want to finish some other stuff today first. When that is done, I will come back to this PR, answer your comments, and also have a look at all the new commits (thank you!).

[ykawase5048]

Due to the rebase, commits mentioned in the comments may have become outdated.

[ykawase5048]

Minor comment: In this PR, I noticed that the implication "finite" → "small" was incorrect and removed it, which seems to have caused the smallness of several categories to become missing data...

[ScriptRaccoon]

Shall I fix the merge conflicts?
Also rebasing is necessary.

[ScriptRaccoon]

There is a very interesting issue: It is independent of our foundation, ZFC with two Grothendieck universes, whether the category of free abelian groups is accessible; see [Makkai-Pare, Section5.5] or MathStackExchange. So, we would need to add the third option "undecidable" for properties.

That's crazy. I have created a separate issue. Let's continue to discuss there.

#82

[ScriptRaccoon]

Minor comment: In this PR, I noticed that the implication "finite" → "small" was incorrect and removed it, which seems to have caused the smallness of several categories to become missing data...

My bad! We have "essentially finite => essentially small", right?

Generalizing what I wrote in my other comment: when an implication A ==> B is removed, look for all categories where it is not known anymore if they are B, and decide B for them. Either manually or via a new implication.

[ScriptRaccoon]

Thanks a lot for your massive work on this PR! I have approved it now. @ykawase5048
From here on, I will handle the rest. I will

• fix the merge conflicts
• bundle the commits into fewer commits ("rewrite history"). I don't want to have too much clutter in the main branch.
• try to remove the merge commits (clutter)
• merge the PR (and deploy the app)

Because of the item 2, it may happen that you are not displayed anymore as the only author of the commits, and it may happen (I am not sure!) that I will be the only author. Is that OK for you? If not, I will not rewrite the history.

EDIT: I checked locally, this branch is a big mess and I am not sure if I can merge it without rewriting history

EDIT: I created a clean branch locally, just 12 commits, with all of your work. Let's see if I can assign the ownership to you somehow ...

[ScriptRaccoon]

I created a clean branch locally, just 12 commits, with all of your work. Let's see if I can assign the ownership to you somehow ...

Please have a look @ykawase5048 : #97

[ykawase5048]

Because of the item 2, it may happen that you are not displayed anymore as the only author of the commits, and it may happen (I am not sure!) that I will be the only author. Is that OK for you? If not, I will not rewrite the history.

I don’t think I should be the only author. You should probably be a co-author! Going through all the changes definitely deserves it!

The PR #97 looks fine for me.

[ScriptRaccoon]

Closed because we will merge #97 instead.