@@ -90,10 +90,9 @@ Completeness is necessary to take fixed-points.

\begin{thm}[Banach's fixed-point]

\label{thm:banach}

Given an inhabited COFE $\ofe$ and a contractive function $f : \ofe\to\ofe$, there exists a unique fixed-point $\fixp_T f$ such that $f(\fixp_T f)=\fixp_T f$.

Moreover, this theorem also holds if $f$ is just non-expansive, and $f^k$ is contractive for an arbitrary $k$.

\end{thm}

The above theorem also holds if $f^k$ is contractive for an arbitrary $k$.

\begin{thm}[America and Rutten~\cite{America-Rutten:JCSS89,birkedal:metric-space}]

\label{thm:america_rutten}

Let $1$ be the discrete COFE on the unit type: $1\eqdef\Delta\{()\}$.

Here, $\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor, which exists by \thmref{thm:america_rutten}.

Here, $\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor, which exists and is unique up to isomorphism by \thmref{thm:america_rutten}.

We do not need to consider how the object $\iPreProp$ is constructed, we only need the isomorphism, given by: