Merge branch 'master' into Classifying-invertible-maps

CODINGSTYLE.md

@@ -284,7 +284,7 @@ the `agda-unimath` library:
   need to sort them by hand.
 
 - The library doesn't use
-  [variables](https://agda.readthedocs.io/en/v2.6.3/language/generalization-of-declared-variables.html)
+  [variables](https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html)
   at the moment. All variables are declared either as parameters of an anonymous
   module or in the type specification of a construction.
 

MIXFIX-OPERATORS.md

@@ -2,7 +2,7 @@
 
 This document outlines our choices of conventions for setting precedence levels
 and associativity of
-[mixfix operators in Agda](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html),
+[mixfix operators in Agda](https://agda.readthedocs.io/en/latest/language/mixfix-operators.html),
 and provides guidelines for this.
 
 ## Mixfix operators in Agda
@@ -16,7 +16,7 @@ and mixfix operators in Agda is to make the code more readable by using commonly
 accepted notation for widely used operators.
 
 Mixfix operators can each be assigned a
-[precedence level](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html#precedence).
+[precedence level](https://agda.readthedocs.io/en/latest/language/mixfix-operators.html#precedence).
 This can in principle be any signed fractional value, although we prefer them to
 be non-negative integral values. The higher this value is, the higher precedence
 the operator has, meaning it is evaluated before operators with lower
@@ -32,7 +32,7 @@ is parsed as `x +ℕ (y *ℕ z)`.
 
 In addition to a precedence level, every mixfix operator can be defined to be
 either left or right
-[associative](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html#associativity).
+[associative](https://agda.readthedocs.io/en/latest/language/mixfix-operators.html#associativity).
 It can be beneficial to define associativity of operators, to avoid excessively
 parenthesized expressions. The parenthization should, however, never be omitted
 when this can make the code more ambiguous or harder to read.

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