From 2c4d6d13f1d60ab2cf334cd6a5255b4df418216c Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 8 Feb 2024 11:40:01 +0100
Subject: [PATCH] improve comment

---
 .../AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda   | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda
index 6884fbadb3..2981254b26 100644
--- a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda
+++ b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda
@@ -282,9 +282,9 @@ module _ {ℓ : Level} where
                                      (CompOpenDistLattice .F-ob ⟦ U ⟧ᶜᵒ)
     compOpenDownHom U = CompOpenDistLattice .F-hom (compOpenGlobalIncl U)
 
-    -- termination issues!!!
-    -- I don't understand what's going on???
     module _ {U V : CompactOpen X} (V≤U : V ≤ U) where
+      -- We need this separate definition to avoid termination checker issues,
+      -- but we don't understand why.
       private
         compOpenDownHomFun : (A : CommRing ℓ)
                            → ⟦ V ⟧ᶜᵒ .F-ob A .fst