\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{well-founded coalgebra}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{algebra}{}\paragraph*{{Algebra}}\label{algebra}

[[!include higher algebra - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{connection_with_initial_algebras}{Connection with initial algebras}\dotfill \pageref*{connection_with_initial_algebras} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{wellfounded_relations}{Well-founded relations}\dotfill \pageref*{wellfounded_relations} \linebreak
\noindent\hyperlink{induction_and_recursion}{Induction and recursion}\dotfill \pageref*{induction_and_recursion} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


The notion of \emph{well-founded coalgebra} is due to [[Paul Taylor]] (with antecedents in the work of Gerhard Osius). Our account is largely based on (\hyperlink{Taylor99}{Taylor, section 6.3)}), and on his paper \hyperlink{tTaylor96}{The General Recursion Theorem}, although in some cases we work with slightly different hypotheses.

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

Let $C$ be a [[finitely complete category]], and let $T$ be an [[endofunctor]] on $C$. We will suppose that $T$ is [[taut functor|taut]], i.e., preserves [[pullbacks]] of [[monomorphisms]] (preserves [[limits]] of [[cospans]] in which one of the cospan arrows is [[monomorphism|monic]]). In particular, this implies that $T$ preserves monos. A helpful example to keep in mind is the covariant power-set functor $P: Set \to Set$.

\begin{udef}
Let $\theta: X \to T X$ be a $T$-[[coalgebra for an endofunctor|coalgebra]] structure on $X$. A [[subobject]] $i: U \hookrightarrow X$ in $C$ is $\theta$-\textbf{inductive} if in the pullback

\begin{displaymath}
\itexarray{
H & \stackrel{j}{\to} & X \\ 
\downarrow & & \downarrow^\mathrlap{\theta} \\
T U & \underset{T i}{\to} & T X
}
\end{displaymath}
the map $j$ factors through $i$ (note that $j$ is monic since $T$ preserves monos).

A coalgebra $(X, \theta)$ is \textbf{well-founded} if the only inductive subobject of $X$ is $X$ itself.

\end{udef}
\textbf{Example:} Suppose $X$ is an initial algebra for the endofunctor $T$, with algebra structure map $\alpha: T X \to X$. By Lambek's theorem, $\alpha$ is invertible, so that $X$ carries a coalgebra structure $\theta = \alpha^{-1}: X \to T X$. It is easy to check that an inductive subobject gives a subalgebra $i: U \to X$, but a subalgebra of an initial algebra must be the initial algebra itself. Hence $(X, \theta)$ is well-founded.

Our goal in this article is to show that one can perform inductive arguments and recursive constructions in the abstract context of well-founded coalgebras. An interesting challenge is to make precise what is meant by a recursive construction of a map $\phi: X \to A$, where the problem is to show how to build $\phi$ from the ground up, as it were. Stages in the recursive construction of a morphism will be \emph{partial} maps, defined as usual as spans

\begin{displaymath}
\itexarray{
 & & D & & \\
 &  ^\mathllap{i} \swarrow & & \searrow^\mathrlap{f} \\ 
A & & & & B
}
\end{displaymath}
for which the arrow $i$ is \emph{monic}. Composition of partial maps is effected by span composition, for which we need only finite cocompleteness (we do not need $C$ to be a [[regular category]], as we would if we were composing general relations between $A$ and $B$). Notice that since $T$ preserves the pulling back of monos, it carries partial maps to partial maps and also preserves partial map composition.

We denote a partial map by a dashed arrow

\begin{displaymath}
f: A \dashrightarrow B
\end{displaymath}
(generally without explicitly mentioning the domain $D$ of $f$), or sometimes by a harpoon notation.

\hypertarget{connection_with_initial_algebras}{}\subsubsection*{{Connection with initial algebras}}\label{connection_with_initial_algebras}

One way of constructing the [[initial algebra of an endofunctor]], $(X, \alpha: T X \to X)$, is by constructing first some [[fixed point]] of $T$, that is, an object $Y$ together with an isomorphism $\xi: Y \cong T Y$. (For example, it might be the terminal coalgebra, whose existence is sometimes easy to establish.) Then, inside $Y$ consider the system of well-founded subcoalgebras of $\xi$. The colimit of this system, assuming it exists, will be the initial algebra. (More theory to develop here.)

The connection with initial algebras goes a little further. Firstly, an initial $T$-algebra is a \emph{Peano $T$-algebra} in the sense of the following definition:

\begin{defn}
\label{}\hypertarget{}{}
A $T$-algebra $(X, \alpha: T X \to X)$ is \emph{semi-Peano} if every $T$-subalgebra [[monomorphism|inclusion]] $i: Y \hookrightarrow X$ is an isomorphism, and \emph{Peano} if in addition $\alpha$ is an isomorphism.

\end{defn}
If $X$ is initial and $i: Y \to X$ is a subalgebra, then there is a unique algebra map $r: X \to Y$, and $i r = 1_X: X \to X$ by initiality, whence $i r i = i$ and then $r i = 1_Y: Y \to Y$ as $i$ is monic. Hence initial algebras are semi-Peano, and Peano by Lambek's theorem.

Secondly, a functor $T: E \to E$ induces, for any object $X$ of $E$, a functor between slices $T_\ast: E/X \to E/ T X$, and so if $(X, \theta: X \to T X)$ is a coalgebra, we may form an endofunctor on $E/X$:

\begin{displaymath}
E/X \stackrel{T_\ast}{\longrightarrow} E/ T X \stackrel{\theta^\ast}{\longrightarrow} E/X
\end{displaymath}
and of course the terminal object $1_X: X \to X$ is automatically and uniquely a $\theta^\ast T_\ast$-algebra. The next two propositions then follow immediately from the definitions of inductive subobject and well-founded coalgebra:

\begin{prop}
\label{}\hypertarget{}{}
A subobject $i: U \to X$ of a $T$-coalgebra $(X, \theta)$ is inductive precisely when $i$ is a $\theta^\ast T_\ast$-subalgebra of the terminal object $1_X$ of $E/X$.

\end{prop}
\begin{prop}
\label{}\hypertarget{}{}
A $T$-coalgebra $X$ is well-founded precisely when the terminal $\theta^\ast T_\ast$-algebra $1_X$ is semi-Peano.

\end{prop}
\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

\hypertarget{wellfounded_relations}{}\subsubsection*{{Well-founded relations}}\label{wellfounded_relations}

The prototype of the notion of well-founded coalgebra is a well-founded [[relation]], which is essentially the same thing as a well-founded coalgebra over the covariant power-set functor $P: Set \to Set$. In brief, a binary [[relation]] $\prec$ on a set $X$ corresponds to a coalgebra $\theta: X \to P X$, by saying $y \prec x$ if and only if $y \in \theta(x)$. See [[well-founded relation]] for more information.

Most of the constructions of this article are well-illustrated by checking them against the background of this prototypical case.

\hypertarget{induction_and_recursion}{}\subsection*{{Induction and recursion}}\label{induction_and_recursion}

``One \emph{proves} things by [[induction]]; one \emph{defines} things by [[recursion]].'' This slogan is not mere pedantry; it is meant to underline a difference between these processes.

A [[proof]] by induction, say a proof of a [[property]] or [[predicate]] $R(x)$ where $x$ varies over a domain $X$, proceeds by showing that the subobject $i: U \hookrightarrow X$ defined by $R$ is an inductive subset with respect to a relation on $X$. It follows that $R$ is universally true on $X$, if the relation is well-founded. The same idiom applies more generally to well-founded coalgebras.

A recursive construction on the other hand involves a \emph{dependency} on prior stages of the construction. A typical application is to define a map $f: X \to A$ by recursion with respect to a well-founded relation, where $f(x)$ is specified in three stages:

\begin{itemize}%
\item Consider the collection $\theta(x) = \{y: y \prec x\}$ of all elements preceding $x$;


\item Pass to the values $f(y)$ defined earlier in the construction, giving a subset $P(f)(\theta(x)) = \{f(y): y \prec x\}$ of $A$;


\item Apply a given operation $\phi: P(A) \to A$ to this subset $(P(f) \circ \theta)(x)$, to obtain $f(x)$.



\end{itemize}
In the last step, the operation may be only partially defined on $P(A)$. In fact, the map $f$ itself may be only partially defined; $f(x)$ is defined only if $\phi((P(f) \circ \theta) (x))$ is defined ``when we call for it''.

An inductive argument is used to show that $f$, so far as it is defined, is uniquely determined. The recursive equation that uniquely determines $f$ (to the extent that it exists, of course) is

\begin{displaymath}
f = \phi \circ P(f) \circ \theta.
\end{displaymath}
Letting $\downarrow x$ denote the down-closure of an element $x \in X$ with respect to $\prec$ (and containing $x$), we may then form the set

\begin{displaymath}
\{x \in X: \exists_{g: \downarrow x \to A} (g = \phi \circ P(g) \circ \theta)\}
\end{displaymath}
whence the existence of a map $f: X \to A$ satisfying the recursive equation might indeed be proven by appeal to an inductive argument.

However, notice that this set is defined by a construction in [[dependent type theory]]. For other categories $C$, we might not have the luxury of interpreting dependent types, so there it wouldn't be right to conflate recursion with induction.

It is nevertheless true that one can prove, in rather considerable generality, both an induction principle and recursion theorem for well-founded coalgebras; this will occupy us in the following sections.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[well-founded relation]]

\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item [[Paul Taylor]], \emph{Practical Foundations of Mathematics} , Cambridge University Press (1999).

\end{itemize}
\begin{itemize}%
\item [[Paul Taylor]], \emph{Towards a unified treatment of induction} , I: the general recursion theorem (1996). (\href{http://www.paultaylor.eu/ordinals/towuti.pdf}{pdf})

\end{itemize}
[[!redirects well-founded coalgebras]]



\end{document}