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?

[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]

I think we can strengthen the implication

(
	'locally_presentable_thin',
	'["locally presentable", "self-dual"]',
	'["thin"]',
	'This follows from <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Thm. 1.64.',
	FALSE
)

now, or rather state that Thm. 1.64 in its original form: locally presentable + locally copresentable => thin

EDIT. Oh you already did that! Nice. Then ignore my comment.

[ykawase5048]

@ScriptRaccoon
Is there anything that needs to be modified in this PR?