Adjunctions of large categories and some minor refactoring (#854)

This PR introduces adjunctions of large categories and does some minor refactoring. --------- Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
UniMath · Oct 17, 2023 · 786f98a · 786f98a
1 parent 166cdfe
commit 786f98a
Show file tree

Hide file tree

Showing 20 changed files with 1,520 additions and 551 deletions.
diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md
@@ -13,6 +13,7 @@
 ```agda
 module category-theory where
 
+open import category-theory.adjunctions-large-categories public
 open import category-theory.adjunctions-large-precategories public
 open import category-theory.anafunctors-categories public
 open import category-theory.anafunctors-precategories public
@@ -48,6 +49,7 @@ open import category-theory.function-precategories public
 open import category-theory.functors-categories public
 open import category-theory.functors-from-small-to-large-categories public
 open import category-theory.functors-from-small-to-large-precategories public
+open import category-theory.functors-large-categories public
 open import category-theory.functors-large-precategories public
 open import category-theory.functors-precategories public
 open import category-theory.groupoids public
@@ -78,6 +80,7 @@ open import category-theory.natural-isomorphisms-maps-precategories public
 open import category-theory.natural-numbers-object-precategories public
 open import category-theory.natural-transformations-functors-categories public
 open import category-theory.natural-transformations-functors-from-small-to-large-precategories public
+open import category-theory.natural-transformations-functors-large-categories public
 open import category-theory.natural-transformations-functors-large-precategories public
 open import category-theory.natural-transformations-functors-precategories public
 open import category-theory.natural-transformations-maps-categories public