add TODO

martinescardo · Sep 4, 2023 · cd2f11a · cd2f11a
1 parent 6530380
commit cd2f11a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/source/Fin/Dedekind.lagda b/source/Fin/Dedekind.lagda
@@ -56,6 +56,6 @@ module _ (pt : propositional-truncations-exist) where
  wconnected-types-are-Dedekind-finite =
   CSB-for-connected-types-without-EM.wconnected-types-are-Dedekind-finite pt
 
-
-
 \end{code}
+
+TODO. Relate this to the other notions of finiteness.