Facts about Adjoints

[TOTBWF]

Description

The following PR proves a bunch of random facts about adjoints. The most notable results are:

• A characterization of when a left/right adjoint is full or faithful
• A characterization of when a right adjoint is conservative
• All of Borceux 3.6

This requires a bit of machinery to set up: in particular, we need a bit of theory about strong monos. In light of this,
I've factored out a lot of the proofs about strong epis into general results about orthogonal maps. I've also done a
naming/API standardization pass on StrongEpi, and renamed it to Strong.Epi to make Strong.Mono a bit more
well organized.

There are also a bunch of misc. reasoning combinator additions, including Cat.Natural.Reasoning.

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.

If your change affects many files without adding substantial content, and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title with chore:.

[Lavenza]

Pull request preview

New pages

• Cat.Functor.Adjoint.Epireflective (+405, -0)
• Cat.Functor.Adjoint.Properties (+228, -0)
• Cat.Morphism.Strong.Mono (+173, -0)
• Cat.Functor.Adjoint.Conservative (+132, -0)
• Cat.Natural.Reasoning (+126, -0)

Changed pages

• Cat.Morphism.Orthogonal (+250, -18)
• Cat.Morphism (+155, -0)
• Cat.Morphism.Strong.Epi (+70, -59)
• Cat.Functor.Adjoint.Reflective (+46, -59)
• Cat.Functor.Properties (+99, -0)
• Cat.Reasoning (+58, -0)
• Borceux (+33, -12)
• Cat.Univalent.Rezk.Universal (+7, -32)
• Cat.Functor.Reasoning (+31, -0)
• Cat.Diagram.Separator.Strong (± 8)
• Cat.Functor.Morphism (+7, -5)

[TOTBWF]

The best order to review this in is probably:

• *.Morphism and *.Reasoning
• Cat.Morphism.StrongEpi rename
• Cat.Adjoint.Properties
• Cat.Adjojnt.Epireflective
• Cat.Adjoint.Conservative

[plt-amy]

I think this should be ∘-is-strong-mono?

[TOTBWF]

Yeah, probably. We'd need to rename strong-epi-∘ as well.

[TOTBWF]

Ok we also have monic-∘ and epic-∘; would be good to do, but perhaps out of scope?