I think it would be nice to add proper adjoint relationships for functors to the database. For example, the free group functor can be marked as left adjoint to the forgetful functor for groups. This relationship can then be displayed on the functor detail pages.
But the deduction system should also be able to make use of these relationships. For example, one theorem could say that the left adjoint of a fully faithful functor is essentially surjective (in fact, the counit is an isomorphism), and this conclusion should be generated automatically.
This issue has been created by Martin via the submission form on http://localhost:5173/functors
I think it would be nice to add proper adjoint relationships for functors to the database. For example, the free group functor can be marked as left adjoint to the forgetful functor for groups. This relationship can then be displayed on the functor detail pages.
But the deduction system should also be able to make use of these relationships. For example, one theorem could say that the left adjoint of a fully faithful functor is essentially surjective (in fact, the counit is an isomorphism), and this conclusion should be generated automatically.
This issue has been created by Martin via the submission form on http://localhost:5173/functors