From be549d5ad9717111fcb5cb620eef3baf2547cd29 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2016 21:28:07 +0100
Subject: [PATCH] add a comment about the OFE vs COFE situation

---
 algebra/cofe.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/algebra/cofe.v b/algebra/cofe.v
index baef71305..0e6e81a73 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -1,5 +1,24 @@
 From algebra Require Export base.
 
+(** This files defines (a shallow embedding of) the category of COFEs:
+    Complete ordered families of equivalences. This is a cartesian closed
+    category, and mathematically speaking, the entire development lives
+    in this category. However, we will generally prefer to work with raw
+    Coq functions plus some registered Proper instances for non-expansiveness.
+    This makes writing such functions much easier. It turns out that it many 
+    cases, we do not even need non-expansiveness.
+
+    In principle, it would be possible to perform a large part of the
+    development on OFEs, i.e., on bisected metric spaces that are not
+    necessary complete. This is because the function space A → B has a
+    completion if B has one - for A, the metric itself suffices.
+    That would result in a simplification of some constructions, becuase
+    no completion would have to be provided. However, on the other hand,
+    we would have to introduce the notion of OFEs into our alebraic
+    hierarchy, which we'd rather avoid. Furthermore, on paper, justifying
+    this mix of OFEs and COFEs is a little fuzzy.
+*)
+
 (** Unbundeled version *)
 Class Dist A := dist : nat → relation A.
 Instance: Params (@dist) 3.
-- 
GitLab