Optimize proof of `equiv-natural-isomorphism-htpy-map-is-category-Pre…

…category` (#929) Found after discussion on Discord. The optimization is possible because of #873.
UniMath · Nov 21, 2023 · fb2b674 · fb2b674
1 parent faee994
commit fb2b674
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 20 deletions.
diff --git a/src/category-theory/category-of-maps-categories.lagda.md b/src/category-theory/category-of-maps-categories.lagda.md
@@ -61,32 +61,15 @@ module _
     ( natural-isomorphism-map-Precategory C D F G)
   equiv-natural-isomorphism-htpy-map-is-category-Precategory F G =
       ( equiv-right-swap-Σ) ∘e
-      ( equiv-Σ
+      ( equiv-Σ-equiv-base
         ( is-natural-transformation-map-Precategory C D F G ∘ pr1)
         ( ( distributive-Π-Σ) ∘e
           ( equiv-Π-equiv-family
             ( λ x →
               extensionality-obj-Category
                 ( D , is-category-D)
                 ( obj-map-Precategory C D F x)
-                ( obj-map-Precategory C D G x))))
-        ( λ K →
-          equiv-implicit-Π-equiv-family
-            ( λ x →
-              equiv-implicit-Π-equiv-family
-                ( λ y →
-                  equiv-Π-equiv-family
-                    ( λ a →
-                      ( equiv-eq
-                        ( ap-binary
-                          ( λ p q →
-                            coherence-square-hom-Precategory D
-                              ( hom-map-Precategory C D F a)
-                              ( p)
-                              ( q)
-                              ( hom-map-Precategory C D G a))
-                          ( compute-hom-iso-eq-Precategory D (K x))
-                          ( compute-hom-iso-eq-Precategory D (K y)))))))))
+                ( obj-map-Precategory C D G x)))))
 
   extensionality-map-is-category-Precategory :
     (F G : map-Precategory C D) →

diff --git a/src/category-theory/isomorphisms-in-precategories.lagda.md b/src/category-theory/isomorphisms-in-precategories.lagda.md
@@ -175,7 +175,7 @@ module _
     (p : x ＝ y) →
     hom-eq-Precategory C x y p ＝
     hom-iso-Precategory C (iso-eq-Precategory x y p)
-  compute-hom-iso-eq-Precategory refl = refl
+  compute-hom-iso-eq-Precategory p = refl
 ```
 
 ## Properties