Modules over monoids and total category of monoids (#2079)

As part of an internship I am doing with @benediktahrens, I added the
definitions of modules (and the category $`\mathrm{Mod}(R)`$ they form)
over some monoid $`R`$ in a fixed monoidal category $`\mathcal{C}`$,
some general examples of modules and a (partial) proof that the category
of modules (over some fixed monoid) inherits its colimits from the base
category $`\mathcal{C}`$.

Benedikt suggested me to file a PR with my (partial) proofs to have
feedback on how the code could be improved. I have tried to stick with
the style guide.

The proof of colimits in $`\mathrm{Mod}(R)`$ is not fully written yet
(what remains should be quickly proven), but getting feedback on how
code could be improved should help me quite a bit for the rest of the
proof. Also, this proof required some general lemmas on colimits that I
added to the `Colimits.v` file.

---------

Co-authored-by: Niels van der Weide <nnmvdw@gmail.com>

Revert "biequiv for universe types"

This reverts commit c3ba9a6.

Move RezkCompletion and rezk_completion to the folder RezkCompletions (…

…#1930)

I used the plural `RezkCompletions` for the folder and file, because I
think the subpackage is about objects of this form in general. Of
course, the completion is unique, but here we do not know that yet.
Resolves #1927

the STLC example in the actegorical setting, with Church numerals (#1869

)

simply-typed lambda calculus represented through a multi-sorted binding
signature, with inductive and with coinductive interpretation, over base
category HSET (this continues the rudimentary example presentation in PR
#1844 in addressing and establishing naturality) and over an abstract
category

construction of the typed Church numerals, including the Church numeral
for infinity in the coinductive interpretation (with its characteristic
fixed-point equation)

---------

Co-authored-by: Ralph Matthes <rmatthes@users.noreply.github.com>

Extending the biequivalence by Clairambault and Dybjer to local prope…

…rties (#1862)

This PR contains an extension of the biequivalence by Clairambault and
Dybjer to include local properties of categories. Currently, the example
of this is given by lextensive categories, so we get a biequivalence
between the bicategory of univalent lextensive categories and democratic
full comprehension categories with ∑, extensional identity, empty types,
and sum types.

A comment was outdated (#1793)

The comment didn't get updated once the proof of the missing statement
was added.

Definitions of natural transformations between sections (#1682)

Defines natural transformations between sections of displayed categories
(such that its components lie over identity in the base category).

Change displayed functor notation. (#1660)

This PR replaces # with \# (or \sharp) for application of displayed functors on morphisms.

Merge pull request #1539 from nmvdw/slices-and-more-lims

Another example of a comprehension bicategory

Merge pull request #1449 from rmatthes/sequeltoPR1426

one more occurrence of forgotten renaming