refactor isomorphisms in small (pre-)categories

fredrik-bakke · Sep 20, 2023 · d9a8a02 · d9a8a02
1 parent f47cf60
commit d9a8a02
Show file tree

Hide file tree

Showing 18 changed files with 1,130 additions and 617 deletions.
diff --git a/src/category-theory/categories.lagda.md b/src/category-theory/categories.lagda.md
@@ -157,7 +157,7 @@ module _
       ( iso-Precategory (precategory-Category C) x y)
       ( iso-eq-Precategory (precategory-Category C) x y)
       ( is-category-Category C x y)
-      ( is-set-iso-Precategory (precategory-Category C) x y)
+      ( is-set-iso-Precategory (precategory-Category C))
 
   obj-Category-1-Type : 1-Type l1
   pr1 obj-Category-1-Type = obj-Category C

diff --git a/src/category-theory/dependent-products-of-precategories.lagda.md b/src/category-theory/dependent-products-of-precategories.lagda.md
@@ -122,7 +122,9 @@ module _
       ( i)
   pr2 (pr2 (is-fiberwise-iso-is-iso-Π-Precategory f is-iso-f i)) =
     htpy-eq
-      ( is-retraction-hom-inv-is-iso-hom-Precategory (Π-Precategory I C) is-iso-f)
+      ( is-retraction-hom-inv-is-iso-hom-Precategory
+        ( Π-Precategory I C)
+        ( is-iso-f))
       ( i)
 
   fiberwise-iso-iso-Π-Precategory :
@@ -149,7 +151,9 @@ module _
   pr2 (pr2 (is-iso-Π-is-fiberwise-iso-Precategory f is-fiberwise-iso-f)) =
     eq-htpy
       ( λ i →
-        is-retraction-hom-inv-is-iso-hom-Precategory (C i) (is-fiberwise-iso-f i))
+        is-retraction-hom-inv-is-iso-hom-Precategory
+          ( C i)
+          ( is-fiberwise-iso-f i))
 
   iso-Π-fiberwise-iso-Precategory :
     ((i : I) → iso-Precategory (C i) (x i) (y i)) →
@@ -202,9 +206,10 @@ module _
     is-equiv-is-invertible
       ( iso-Π-fiberwise-iso-Precategory)
       ( λ e →
-        eq-htpy (λ i → eq-type-subtype (is-iso-hom-Precategory-Prop (C i)) refl))
+        eq-htpy
+          ( λ i → eq-type-subtype (is-iso-prop-hom-Precategory (C i)) refl))
       ( λ e →
-        eq-type-subtype (is-iso-hom-Precategory-Prop (Π-Precategory I C)) refl)
+        eq-type-subtype (is-iso-prop-hom-Precategory (Π-Precategory I C)) refl)
 
   equiv-fiberwise-iso-iso-Π-Precategory :
     ( iso-Precategory (Π-Precategory I C) x y) ≃