Add "locally cartesian closed" property

[varkor]

Note that I have not yet tested these changes locally (I'm currently not a machine on which I can test), but it may be that there is a GitHub Action that tests pull requests. (If not, I should be able to test later today.)

[ScriptRaccoon]

Thank you for the PR! You are first one to contribute. 🎉

I have made some suggestions.

Currently, for 17 categories in the database it is unknown if they are locally cartesian closed. If you know something about these, please add the info:

[
    "category of posets",
    "category of finite sets and bijections",
    "category of finite sets and injections",
    "discrete category on two objects",
    "walking morphism",
    "partial order of natural numbers",
    "partial order [0,1]",
    "partial order of extended natural numbers",
    "partial order of ordinal numbers",
    "category of Z-functors",
    "delooping of an infinite group",
    "delooping of a non-trivial finite group",
    "delooping of the additive monoid of natural numbers",
    "delooping of the additive monoid of ordinal numbers",
    "category of fields",
    "category of small categories",
    "category of combinatorial species"
]

Maybe there are also some implications we can add so that the work is done for us automatically.

[varkor]

I've updated the pull request. I've added the category walking composable pair as well as another property strongly connected, which is used to establish local cartesian closure for some categories. There are probably some obvious missing implications, but it takes time to establish the properties for every single category, and I don't have more time at the moment.

Unfortunately, I'm having trouble getting pnpm to work at the moment, so I still have been unable to test the changes.

[ScriptRaccoon]

Is there any literature about this terminology? I cannot find anything, unfortunately. If there is anything, we should add it in the description.

[ScriptRaccoon]

I've updated the pull request. I've added the category walking composable pair as well as another property strongly connected, which is used to establish local cartesian closure for some categories.

This is great!

I also like that you have added some implications to refactor the properties. This is exactly what CatDat is made for. 🎉

There are probably some obvious missing implications, but it takes time to establish the properties for every single category, and I don't have more time at the moment.

That's ok :)

Unfortunately, I'm having trouble getting pnpm to work at the moment, so I still have been unable to test the changes

No problem. There were indeed some minor issues, I have fixed them in feeebc0 (will be squashed later after your review).

Also, you had removed "inhabited" from an implication which triggered a contradiction in the database. (Good that I have a trigger to check that!) I have added it back in the commit and now the data is consistent again.

I've also made an assumption stronger (f8df03d), which settles lcc for some categories (I think this was actually your intent).

Let me know if you are OK, then I will merge.