From ef669d8120f9ce2204ee76f36d0e4cb63ea124c1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 4 Aug 2016 11:04:09 +0200
Subject: [PATCH] docs: fix COFE limit axiom
---
docs/algebra.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/algebra.tex b/docs/algebra.tex
index a970524c1..0fa60eac5 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -15,7 +15,7 @@ This definition varies slightly from the original one in~\cite{catlogic}.
\All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{cofe-equiv} \\
\All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{cofe-mono} \\
\All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{cofe-limit} \\
- \All n, c.& \lim(c) \nequiv{n} c(n+1) \tagH{cofe-compl}
+ \All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofe-compl}
\end{align*}
\end{defn}
--
GitLab