Free groupoids and final functors

[ncfavier]

Description

Closes #335 in the maximally annoying way, by using the fully correct definition of final functors:

• define the free groupoid on a category and show that it satisfies the universal property of the left biadjoint to the inclusion of groupoids into categories (dual to the core)
• define connected categories as those that are merely inhabited and merely have a zigzag connecting every two objects (ensuring that their free groupoid is connected in the sense of HoTT), prove that this is equivalent to the coequaliser Ob/Hom being contractible
• redefine final functors as those whose comma categories are connected, adapt the existing proofs that composition with a final functor leaves colimits unchanged and that final functors are closed under composition, and give some examples of final functors (full, essentially surjective functors between groupoids; right adjoints; inclusions of terminal objects)

The new definition is much more annoying to work with and I am very much open to improvements to the proofs, particularly the closure under composition of final functors. I couldn't find the argument fully spelt out anywhere (even the nlab handwaves that it "suffices to consider the case of a zigzag of length one"), and I think I understand why...

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

[ncfavier]

This is much, much better than what I came up with!