From 00f01937da9eab3cbdb16925f79b7f93f923fc82 Mon Sep 17 00:00:00 2001
From: "Max S. New" <maxsnew@gmail.com>
Date: Thu, 28 Nov 2024 03:20:00 -0600
Subject: [PATCH] fix incorrectly named isIsoToIso, add IsoToIsIso (#1173)

---
 Cubical/Foundations/Isomorphism.agda | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/Cubical/Foundations/Isomorphism.agda b/Cubical/Foundations/Isomorphism.agda
index 02a87e861..d1fbf40e2 100644
--- a/Cubical/Foundations/Isomorphism.agda
+++ b/Cubical/Foundations/Isomorphism.agda
@@ -104,14 +104,19 @@ isoToEquiv : Iso A B → A ≃ B
 isoToEquiv i .fst = i .Iso.fun
 isoToEquiv i .snd = isoToIsEquiv i
 
-isoToIsIso : {f : A → B} → isIso f → Iso A B
-isoToIsIso {f = f} fIsIso .Iso.fun = f
-isoToIsIso fIsIso .Iso.inv = fIsIso .fst
-isoToIsIso fIsIso .Iso.rightInv = fIsIso .snd .fst
-isoToIsIso fIsIso .Iso.leftInv = fIsIso .snd .snd
+IsoToIsIso : (f : Iso A B) → isIso (f .Iso.fun)
+IsoToIsIso f .fst = f .Iso.inv
+IsoToIsIso f .snd .fst = f .Iso.rightInv
+IsoToIsIso f .snd .snd = f .Iso.leftInv
+
+isIsoToIso : {f : A → B} → isIso f → Iso A B
+isIsoToIso {f = f} fIsIso .Iso.fun = f
+isIsoToIso fIsIso .Iso.inv = fIsIso .fst
+isIsoToIso fIsIso .Iso.rightInv = fIsIso .snd .fst
+isIsoToIso fIsIso .Iso.leftInv = fIsIso .snd .snd
 
 isIsoToIsEquiv : {f : A → B} → isIso f → isEquiv f
-isIsoToIsEquiv fIsIso = isoToIsEquiv (isoToIsIso fIsIso)
+isIsoToIsEquiv fIsIso = isoToIsEquiv (isIsoToIso fIsIso)
 
 isoToPath : Iso A B → A ≡ B
 isoToPath {A = A} {B = B} f i =