fixfix

UniMath · Nov 11, 2023 · 9cb4528 · 9cb4528
1 parent e3e2835
commit 9cb4528
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 7 deletions.
diff --git a/src/category-theory/epimorphisms-in-large-precategories.lagda.md b/src/category-theory/epimorphisms-in-large-precategories.lagda.md
@@ -59,7 +59,7 @@ module _
 module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : Large-Precategory α β) {l1 l2 : Level} (l3 : Level)
-  {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2}
+  (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2)
   (f : iso-Large-Precategory C X Y)
   where
 

diff --git a/src/category-theory/monomorphisms-in-large-precategories.lagda.md b/src/category-theory/monomorphisms-in-large-precategories.lagda.md
@@ -59,7 +59,7 @@ module _
 module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : Large-Precategory α β) {l1 l2 : Level} (l3 : Level)
-  {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2}
+  (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2)
   (f : iso-Large-Precategory C X Y)
   where
 

diff --git a/src/group-theory/epimorphisms-groups.lagda.md b/src/group-theory/epimorphisms-groups.lagda.md
@@ -63,10 +63,9 @@ module _
   (H : Group l2) (f : iso-Group G H)
   where
 
-  is-epi-iso-Group :
-    is-epi-Group l3 G H (hom-iso-Group G H f)
+  is-epi-iso-Group : is-epi-Group l3 G H (hom-iso-Group G H f)
   is-epi-iso-Group =
-    is-epi-iso-Large-Precategory Group-Large-Precategory l3 {G} {H} f
+    is-epi-iso-Large-Precategory Group-Large-Precategory l3 G H f
 ```
 
 ### A group homomorphism is surjective if and only if it is an epimorphism

diff --git a/src/group-theory/monomorphisms-groups.lagda.md b/src/group-theory/monomorphisms-groups.lagda.md
@@ -56,8 +56,7 @@ module _
   (H : Group l2) (f : iso-Group G H)
   where
 
-  is-mono-iso-Group :
-    is-mono-Group l3 G H (hom-iso-Group G H f)
+  is-mono-iso-Group : is-mono-Group l3 G H (hom-iso-Group G H f)
   is-mono-iso-Group =
     is-mono-iso-Large-Precategory Group-Large-Precategory l3 G H f
 ```