Sync with my development repo. Add new material: "concrete bicategories" and
"bicategory of categories". Change sublocale declarations related to
functor/natural transformation/natural isomorphism to avoid issues with
global interpretations reported by Filip Smola, 2/2/2021.