F-Algebras, Lambek's Lemma, Adamek's theorem, and free monads

[TOTBWF]

Description

This PR defines the displayed category of F-algebras, and proceeds to prove Lambeks's lemma and Adamek's theorem. Additionally, it proves that a left adjoint to the forgetful functor FAlg -> C implies the existence of the free monad on F. It also defines free objects, and shows the subcategory of free objects induces the free relative extension system.

Checklist

Before submitting a merge request, please check the items below:

• [x] I've read the contributing guidelines.
• [x] The imports of new modules have been sorted with support/sort-imports.hs (or nix run --experimental-features nix-command -f . sort-imports).
• [x] All new code blocks have "agda" as their language.

[Lavenza]

Pull request preview

[TOTBWF]

Everything is up to date with the latest branch, but I think @plt-amy needs to mark the change request as resolved.