Generalized Reedy categories, Direct categories

[TOTBWF]

Description

Just some basic definitions about Reedy/direct categories, along with a theorem about reflective subcategories of reedy categories.

Notes

It might be worth omitting "generalized" from both of these definitions, and calling the strict variants "skeletal Reedy" and "skeletal direct". I've opted to keep the same nomenclature as the literature here, but we almost always want to use the generalized versions.

Checklist

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

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

[Lavenza]

Pull request preview

New pages

• Cat.Reedy.Generalized (+331, -0)
• Cat.Direct.Generalized (+94, -0)

Changed pages

• Cat.Morphism.Factorisation.Orthogonal (+187, -0)
• Cat.Morphism.Orthogonal (+66, -2)
• Cat.Morphism.Lifts (+58, -0)
• Data.Wellfounded.Properties (+42, -2)
• Cat.Functor.Reasoning.FullyFaithful (+35, -4)
• Cat.Functor.Properties (+18, -3)
• Cat.Functor.Reasoning (+18, -0)
• Cat.Morphism.Class (+17, -0)