improve comment

agda · Feb 8, 2024 · 2c4d6d1 · 2c4d6d1
1 parent 73cc74a
commit 2c4d6d1
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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