From c73f0c685bcb0de94ee1cc8cf2b050a6b90996f5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 10 Dec 2017 13:26:11 +0100
Subject: [PATCH] Fix typo in docs: fixpoints can only be taken of
 endo-functions.

---
 docs/algebra.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/algebra.tex b/docs/algebra.tex
index adf798b09..0a9c8687d 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -85,7 +85,7 @@ COFEs are \emph{complete OFEs}, which means that we can take limits of arbitrary
 The function space $\ofe \nfn \cofeB$ is a COFE if $\cofeB$ is a COFE (\ie the domain $\ofe$ can actually be just an OFE).
 
 Completeness is necessary to take fixed-points.
-For once, every \emph{contractive function} $f : \ofe \to \cofeB$ where $\cofeB$ is a COFE and inhabited has a \emph{unique} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$.
+For once, every contractive function $f : \cofe \to \cofe$ where $\cofe$ is a COFE and inhabited has a \emph{unique} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$.
 This also holds if $f^k$ is contractive for an arbitrary $k$.
 Furthermore, by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}, every contractive (bi)functor from $\COFEs$ to $\COFEs$ has a unique\footnote{Uniqueness is not proven in Coq.} fixed-point.
 
-- 
GitLab