From cca16810dd13273f00377a4696ae11ec9245c852 Mon Sep 17 00:00:00 2001
From: Martin Escardo <m.escardo@cs.bham.ac.uk>
Date: Mon, 21 Oct 2024 09:41:25 +0100
Subject: [PATCH] compatibility condition is actually data

---
 source/InjectiveTypes/Sigma.lagda | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/source/InjectiveTypes/Sigma.lagda b/source/InjectiveTypes/Sigma.lagda
index 0ea1c7b1e..e3db8641e 100644
--- 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