Merge remote-tracking branch 'agda-unimath/master' into functor-categ…

…ories
fredrik-bakke · Sep 19, 2023 · 7955721 · 7955721
2 parents d1a36f7 + eda7bb2
commit 7955721
Show file tree

Hide file tree

Showing 16 changed files with 1,177 additions and 147 deletions.
diff --git a/scripts/preprocessor_git_metadata.py b/scripts/preprocessor_git_metadata.py
@@ -89,7 +89,7 @@ def get_author_element_for_file(filename, include_contributors, contributors):
             author['displayName']
             for author in sorted_authors_from_raw_shortlog_lines(raw_authors_git_output, contributors)
         ]
-        attribution_text = f'<p><i>Content created by {format_multiple_authors_attribution(author_names)}</i></p>'
+        attribution_text = f'<p><i>Content created by {format_multiple_authors_attribution(author_names)}.</i></p>'
 
     file_log_output = subprocess.run([
         'git', 'log',

diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md
@@ -57,6 +57,7 @@ open import category-theory.groupoids public
 open import category-theory.homotopies-natural-transformations-large-precategories public
 open import category-theory.initial-objects-in-precategories public
 open import category-theory.isomorphisms-in-categories public
+open import category-theory.isomorphisms-in-large-categories public
 open import category-theory.isomorphisms-in-large-precategories public
 open import category-theory.isomorphisms-in-precategories public
 open import category-theory.large-categories public

diff --git a/src/category-theory/epimorphisms-in-large-precategories.lagda.md b/src/category-theory/epimorphisms-in-large-precategories.lagda.md
@@ -64,41 +64,41 @@ module _
   where
 
   is-epi-iso-Large-Precategory :
-    is-epi-Large-Precategory C l3 X Y (hom-iso-Large-Precategory C X Y f)
+    is-epi-Large-Precategory C l3 X Y (hom-iso-Large-Precategory C f)
   is-epi-iso-Large-Precategory Z g h =
     is-equiv-is-invertible
       ( λ P →
         ( inv
           ( right-unit-law-comp-hom-Large-Precategory C g)) ∙
           ( ( ap
             ( λ h' → comp-hom-Large-Precategory C g h')
-            ( inv (is-section-hom-inv-iso-Large-Precategory C X Y f))) ∙
+            ( inv (is-section-hom-inv-iso-Large-Precategory C f))) ∙
             ( ( inv
               ( associative-comp-hom-Large-Precategory C
                 ( g)
-                ( hom-iso-Large-Precategory C X Y f)
-                ( hom-inv-iso-Large-Precategory C X Y f))) ∙
+                ( hom-iso-Large-Precategory C f)
+                ( hom-inv-iso-Large-Precategory C f))) ∙
               ( ( ap
                 ( λ h' →
                   comp-hom-Large-Precategory
                     ( C)
                     ( h')
-                    ( hom-inv-iso-Large-Precategory C X Y f))
+                    ( hom-inv-iso-Large-Precategory C f))
                 ( P)) ∙
                 ( ( associative-comp-hom-Large-Precategory C
                   ( h)
-                  ( hom-iso-Large-Precategory C X Y f)
-                  ( hom-inv-iso-Large-Precategory C X Y f)) ∙
+                  ( hom-iso-Large-Precategory C f)
+                  ( hom-inv-iso-Large-Precategory C f)) ∙
                   ( ( ap
                     ( comp-hom-Large-Precategory C h)
-                    ( is-section-hom-inv-iso-Large-Precategory C X Y f)) ∙
+                    ( is-section-hom-inv-iso-Large-Precategory C f)) ∙
                     ( right-unit-law-comp-hom-Large-Precategory C h)))))))
       ( λ p →
         eq-is-prop
           ( is-set-type-hom-Large-Precategory C X Z
             ( comp-hom-Large-Precategory C g
-              ( hom-iso-Large-Precategory C X Y f))
+              ( hom-iso-Large-Precategory C f))
             ( comp-hom-Large-Precategory C h
-              ( hom-iso-Large-Precategory C X Y f))))
+              ( hom-iso-Large-Precategory C f))))
       ( λ p → eq-is-prop (is-set-type-hom-Large-Precategory C Y Z g h))
 ```
diff --git a/src/category-theory/functors-categories.lagda.md b/src/category-theory/functors-categories.lagda.md
@@ -120,7 +120,9 @@ module _
 
   map-obj-functor-Category : functor-Category → obj-Category C → obj-Category D
   map-obj-functor-Category =
-    map-obj-functor-Precategory (precategory-Category C) (precategory-Category D)
+    map-obj-functor-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
 
   map-hom-functor-Category :
     (F : functor-Category) →