Maps of categories, functor categories, and small subprecategories (#794

)

Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>

src/category-theory.lagda.md

@@ -37,6 +37,9 @@ open import category-theory.adjunctions-large-precategories public
 open import category-theory.anafunctors-categories public
 open import category-theory.anafunctors-precategories public
 open import category-theory.categories public
+open import category-theory.category-of-functors public
+open import category-theory.category-of-maps-of-categories public
+open import category-theory.commuting-squares-of-morphisms-in-precategories public
 open import category-theory.coproducts-in-precategories public
 open import category-theory.dependent-products-of-categories public
 open import category-theory.dependent-products-of-precategories public
@@ -47,7 +50,8 @@ open import category-theory.epimorphisms-in-large-precategories public
 open import category-theory.equivalences-of-categories public
 open import category-theory.equivalences-of-large-precategories public
 open import category-theory.equivalences-of-precategories public
-open import category-theory.exponential-objects-in-precategories public
+open import category-theory.exponential-objects-precategories public
+open import category-theory.faithful-functors-precategories public
 open import category-theory.function-categories public
 open import category-theory.function-precategories public
 open import category-theory.functors-categories public
@@ -64,27 +68,36 @@ open import category-theory.isomorphisms-in-large-precategories public
 open import category-theory.isomorphisms-in-precategories public
 open import category-theory.large-categories public
 open import category-theory.large-precategories public
+open import category-theory.maps-categories public
+open import category-theory.maps-precategories public
 open import category-theory.monomorphisms-in-large-precategories public
 open import category-theory.natural-isomorphisms-categories public
 open import category-theory.natural-isomorphisms-large-precategories public
+open import category-theory.natural-isomorphisms-maps-categories public
+open import category-theory.natural-isomorphisms-maps-precategories public
 open import category-theory.natural-isomorphisms-precategories public
 open import category-theory.natural-numbers-object-precategories public
 open import category-theory.natural-transformations-categories public
 open import category-theory.natural-transformations-large-precategories public
+open import category-theory.natural-transformations-maps-categories public
+open import category-theory.natural-transformations-maps-precategories public
 open import category-theory.natural-transformations-precategories public
 open import category-theory.one-object-precategories public
 open import category-theory.opposite-precategories public
 open import category-theory.precategories public
 open import category-theory.precategory-of-functors public
+open import category-theory.precategory-of-maps-of-precategories public
 open import category-theory.pregroupoids public
 open import category-theory.products-in-precategories public
 open import category-theory.products-of-precategories public
 open import category-theory.pullbacks-in-precategories public
 open import category-theory.representable-functors-categories public
 open import category-theory.representable-functors-precategories public
+open import category-theory.representing-arrow-category public
 open import category-theory.sieves-in-categories public
 open import category-theory.slice-precategories public
-open import category-theory.terminal-objects-in-precategories public
+open import category-theory.subprecategories public
+open import category-theory.terminal-objects-precategories public
 open import category-theory.yoneda-lemma-categories public
 open import category-theory.yoneda-lemma-precategories public
 ```