From fb2b6740b798912b62e6761bee8a783d0c81943c Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 21 Nov 2023 19:15:06 +0100
Subject: [PATCH] Optimize proof of
 `equiv-natural-isomorphism-htpy-map-is-category-Precategory` (#929)

Found after discussion on Discord. The optimization is possible because
of #873.
---
 .../category-of-maps-categories.lagda.md      | 21 ++-----------------
 .../isomorphisms-in-precategories.lagda.md    |  2 +-
 2 files changed, 3 insertions(+), 20 deletions(-)

diff --git a/src/category-theory/category-of-maps-categories.lagda.md b/src/category-theory/category-of-maps-categories.lagda.md
index 660aa85375..1226b6f854 100644
--- a/src/category-theory/category-of-maps-categories.lagda.md
+++ b/src/category-theory/category-of-maps-categories.lagda.md
@@ -61,7 +61,7 @@ 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
@@ -69,24 +69,7 @@ module _
               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
index a8c2a3b935..155a360e41 100644
--- 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