compatibility condition is actually data

martinescardo · Oct 21, 2024 · cca1681 · cca1681
1 parent 1c016f5
commit cca1681
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/source/InjectiveTypes/Sigma.lagda b/source/InjectiveTypes/Sigma.lagda
@@ -140,6 +140,9 @@ InjectiveTypes.MathematicalStructures.
 
 \end{code}
 
+NB. Notice that our compatibility condition is data rather than
+property. TODO. Should we call it compatibility data?
+
 That this compatibility condition is sufficient but not necessary is
 illustrated in the file InjectiveTypes.InhabitednessTaboo, with the
 type of pointed types (which is injective) shown to be equivalent to a