Isomorphisms in large categories and large precategories (UniMath#791)

fredrik-bakke · Sep 19, 2023 · eda7bb2 · eda7bb2
1 parent cdc008d
commit eda7bb2
Show file tree

Hide file tree

Showing 12 changed files with 1,169 additions and 143 deletions.
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))
 ```