$W$-Types in Categories of Coalgebras

TL;DR

This paper develops a method to construct $W$-types within categories of coalgebras for cartesian comonads, extending previous constructions in presheaf and gluing toposes.

Contribution

It introduces a generalized construction of $W$-types applicable to coalgebras for cartesian comonads, broadening the scope of existing theories.

Findings

Constructed $W$-types in coalgebra categories for cartesian comonads

Unified previous $W$-type constructions in presheaf and gluing toposes

Extended the applicability of $W$-types in categorical frameworks

Abstract

We construct $W$-types in the category of coalgebras for a cartesian comonad. It generalizes the constructions of $W$-types in presheaf toposes and gluing toposes.

Equations

$$PR$$

$$\leavevmode\hbox to80.97pt{\vbox to38.71pt{\pgfpicture\makeatletter\hbox{\hskip 40.48256pt\lower-25.49854pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{\offinterlineskip{}{}{{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-40.48256pt}{-8.65971pt}\pgfsys@invoke{ }\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip 13.90968pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-9.60414pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathcal{E}/I}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip 13.90968pt\hfil&\hfil\hskip 38.57286pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.26735pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathcal{E}/J}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip 14.57289pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}{{{{}}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{{{}{}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{{{}}}{{{}}}}{{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-12.4632pt}{2.45137pt}\pgfsys@lineto{10.73682pt}{2.45137pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.9368pt}{2.45137pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.30905pt}{6.19302pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{f_{!}}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{{{}{}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{{{}}}{{{}}}}{{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-12.4632pt}{-14.7708pt}\pgfsys@lineto{10.73682pt}{-14.7708pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.9368pt}{-14.7708pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.7535pt}{-21.98466pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{f_{*}}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{11.13678pt}{-6.15971pt}\pgfsys@lineto{-12.06323pt}{-6.15971pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-12.26321pt}{-6.15971pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@rect{-5.90627pt}{-11.88885pt}{10.48611pt}{11.45828pt}\pgfsys@fill\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.7535pt}{-8.375pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{f^{*}}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\quad f_{!}\dashv f^{*}\dashv f_{*}$$

$$I$$

$$g^{\ast }{g}_{\ast }{h}^{\ast }K$$

$$+:\mathcal{E}/A\times \mathcal{E}/B\to \mathcal{E}/(A+B)$$

$$F_{G}R{U}_H$$

$$GR$$

$$\mathcal{E}/A$$

$$F_{G_{\beta }}{\Pi }_f^{\mathcal{E}}{U}_{G_{\alpha }}$$

$${\mathcal{E}}_G$$

$$PA$$

$${\mathcal{E}}_G$$

$$1$$

$$(I,\iota )$$

$$P_{f,g,h}$$

$$\mathcal{E}/C_0$$

$${\mathcal{E}}_1/K_1$$

$$X$$

$$PW$$

$$X$$

$$P_0{X}_0$$

$$PX$$

$$P_{0}X$$

$$i^{\ast }{P}_0{X}_0$$

Full text

1 Introduction

$W$-type is an important feature of Martin-Löf’s dependent type theory [Mar82, NPS90] and allows us to define a wide range of inductive types. Its categorical counterpart is the initial algebra for a polynomial endofunctor [MP00, GH04].

In this paper we construct $W$-types in the category of coalgebras for a cartesian comonad. This is a generalization of the constructions of $W$-types in presheaf toposes and Freyd cover given by Moerdijk and Palmgren [MP00] and gluing $\Pi W$-pretoposes given by van den Berg [Ber06].

In Section 2 we review the notion of $W$-type. In Section 3 we describe pushforwards in the category of coalgebras for a cartesian comonad. In Section 4 we show the main theorem (Theorem 35) and give some applications. In Section 5 we show a technical lemma used in the proof of the main theorem.

2 $W$-Types in Categories

We review the notions of polynomial, algebra and $W$-type. First we recall the notion of algebra for an endofunctor.

Definition 1**.**

Let $P:\mathcal{E}\to\mathcal{E}$ be an endofunctor on a category $\mathcal{E}$. A $P$-algebra consists of an object $X\in\mathcal{E}$ and a morphism $s_{X}:PX\to X$. A morphism of $P$-algebras $(X,s_{X})\to(Y,s_{Y})$ is a morphism $h:X\to Y$ in $\mathcal{E}$ such that $h\circ s_{X}=s_{Y}\circ Ph$. We shall denote by $\mathrm{Alg}(P)$ the category of $P$-algebras and morphisms of $P$-algebras, and by $U_{P}:\mathrm{Alg}(P)\to\mathcal{E}$ the obvious forgetful functor. An initial $P$-algebra is an initial object in the category $\mathrm{Alg}(P)$.

Definition 2**.**

Let $P:\mathcal{E}\to\mathcal{E}$ and $Q:\mathcal{F}\to\mathcal{F}$ be endofunctors. A lax morphism $P\to Q$ is a pair $(H,\sigma)$ consisting of a functor $H:\mathcal{E}\to\mathcal{F}$ and a natural transformation $\sigma:QH\Rightarrow HP$. A strong morphism $P\to Q$ is a lax morphism $(H,\sigma):P\to Q$ such that $\sigma$ is an natural isomorphism.

Proposition 3**.**

Let $P:\mathcal{E}\to\mathcal{E}$ and $Q:\mathcal{F}\to\mathcal{F}$ be endofunctors. A lax morphism $(H,\sigma):P\to Q$ induces a functor $\tilde{H}:\mathrm{Alg}(P)\to\mathrm{Alg}(Q)$ such that $U_{Q}\tilde{H}=HU_{P}$ defined by $\tilde{H}(X,s)=(HX,Hs\circ\sigma(X))$.

The following is analogous to the adjoint lifting theorem for (co)algebras for (co)monads by Johnstone [Joh75] and Keigher [Kei75].

Proposition 4**.**

Let $P:\mathcal{E}\to\mathcal{E}$ and $Q:\mathcal{F}\to\mathcal{F}$ be endofunctors and $(H,\sigma):P\to Q$ a strong morphism. Suppose that $H$ has a right adjoint $R$. Then the induced functor $\tilde{H}:\mathrm{Alg}(P)\to\mathrm{Alg}(Q)$ has a right adjoint $\tilde{R}:\mathrm{Alg}(Q)\to\mathrm{Alg}(P)$ such that $U_{P}\tilde{R}=RU_{Q}$.

Proof.

Let $\eta$ and $\varepsilon$ denote the unit and counit, respectively, of the adjunction $H\dashv R$. The functor $R$ is part of a lax morphism $Q\to P$ with the mate of $\sigma^{-1}$

[TABLE]

Hence we have a functor $\tilde{R}:\mathrm{Alg}(Q)\to\mathrm{Alg}(P)$ such that $U_{P}\tilde{R}=RU_{Q}$. One can show that $\eta$ and $\varepsilon$ defines natural transformations $1\Rightarrow\tilde{R}\tilde{H}$ and $\tilde{H}\tilde{R}\Rightarrow 1$ respectively, so $\tilde{R}$ is the right adjoint to $\tilde{H}$. ∎

$W$-types are defined as the initial algebras for endofunctors represented by polynomials.

Notation 5**.**

Let $\mathcal{E}$ be a locally cartesian closed category. For a morphism $f:I\to J$ in $\mathcal{E}$, we shall denote by $f^{*}$ the pullback functor $\mathcal{E}/J\to\mathcal{E}/I$, by $f_{!}$ or $\Sigma^{\mathcal{E}}_{f}$ its left adjoint, and by $f_{*}$ or $\Pi^{\mathcal{E}}_{f}$ its right adjoint.

[TABLE]

We call $f_{*}$ the pushforward along $f$.

For a functor $H:\mathcal{E}\to\mathcal{F}$ and an object $I\in\mathcal{E}$, we denote by $H/I:\mathcal{E}/I\to\mathcal{F}/HI$ the functor $(f:X\to I)\mapsto(Hf:HX\to HI)$.

Definition 6**.**

Let $\mathcal{E}$ be a locally cartesian closed category. For objects $I,J\in\mathcal{E}$, a polynomial from $I$ to $J$ is a triple $(f,g,h)$ of morphisms of the form

[TABLE]

For a polynomial $(f,g,h)$ from $I$ to $J$, we define a functor $P_{f,g,h}:\mathcal{E}/I\to\mathcal{E}/J$ to be $f_{!}g_{*}h^{*}$. We say a functor $P:\mathcal{E}/I\to\mathcal{E}/J$ is represented by a polynomial $(f,g,h)$ from $I$ to $J$ when $P$ is isomorphic to $P_{f,g,h}$. We shall denote by $\mathbf{Poly}_{\mathcal{E}}(I,J)$ the class of functors $P:\mathcal{E}/I\to\mathcal{E}/J$ that are represented by some polynomial from $I$ to $J$. We often omit the subscript and simply write $\mathbf{Poly}(I,J)$ when the category $\mathcal{E}$ is clear from the context.

Definition 7**.**

Let $\mathcal{E}$ be a locally cartesian closed category. For an object $I\in\mathcal{E}$, an endopolynomial on $I$ is a polynomial of the form

[TABLE]

We say $\mathcal{E}$ has $W$-types or is a locally cartesian closed category with $W$-types if, for any endopolynomial $(f,g,h)$ on any object $I$, there exists an initial $P_{f,g,h}$-algebra.

Remark 8*.*

$W$-types in this paper are what are called dependent $W$-types or indexed $W$-types in the literature. Gambino and Hyland [GH04] showed that a locally cartesian closed category has all non-dependent $W$-types if and only if it has all dependent $W$-types. So our terminology “having $W$-types” coincides with that of Moerdijk and Palmgren [MP00].

Definition 9**.**

Let $\mathcal{E}$ and $\mathcal{F}$ be locally cartesian closed categories and $H:\mathcal{E}\to\mathcal{F}$ a locally cartesian closed functor, namely a functor that preserves finite limits and pushforwards. By definition, for an endopolynomial $(f,g,h)$ on an object $I\in\mathcal{E}$, the functor $H/I:\mathcal{E}/I\to\mathcal{F}/HI$ is part of a strong morphism $P_{f,g,h}\to P_{Hf,Hg,Hh}$. Suppose $\mathcal{E}$ and $\mathcal{F}$ have $W$-types. We say $H$ preserves $W$-types if the induced functor $\mathrm{Alg}(P_{f,g,h})\to\mathrm{Alg}(P_{Hf,Hg,Hh})$ preserves initial objects for any endopolynomial $(f,g,h)$ in $\mathcal{E}$.

By Proposition 4 we have the following.

Proposition 10**.**

Let $\mathcal{E}$ and $\mathcal{F}$ be locally cartesian closed categories with $W$-types and $H:\mathcal{E}\to\mathcal{F}$ a locally cartesian closed functor. If $H$ has a right adjoint, then $H$ preserves $W$-types.

The class of functors represented by polynomials is closed under several constructions.

Proposition 11**.**

Let $\mathcal{E}$ be a locally cartesian closed category.

For any object $I\in\mathcal{E}$, the identity functor $\mathcal{E}/I\to\mathcal{E}/I$ belongs to $\mathbf{Poly}(I,I)$. 2. 2.

For functors $P:\mathcal{E}/I\to\mathcal{E}/J$ and $Q:\mathcal{E}/J\to\mathcal{E}/K$, if $P$ belongs to $\mathbf{Poly}(I,J)$ and $Q$ belongs to $\mathbf{Poly}(J,K)$, then $QP$ belongs to $\mathbf{Poly}(I,K)$.

Proof.

The identity functor $\mathcal{E}/I\to\mathcal{E}/I$ is represented by the polynomial $(1_{I},1_{I},1_{I})$. For the composition, see [GK13]. ∎

Proposition 12**.**

Let $\mathcal{E}$ be a locally cartesian closed category and $P:\mathcal{E}/I\to\mathcal{E}/J$ a functor. If $P$ belongs to $\mathbf{Poly}(I,J)$, then $P/K$ belongs to $\mathbf{Poly}(K,PK)$ for any object $K\in\mathcal{E}/I$.

Proof.

Suppose that $P$ is represented by a polynomial

{I}$${A}$${B}$${J.}$$\scriptstyle{h}$$\scriptstyle{g}$$\scriptstyle{f}

Consider the following diagram,

[TABLE]

where the left and middle squares are pullbacks, $\varepsilon$ is the counit of the adjunction $g^{*}\dashv g_{*}$, and $\eta:g_{*}h^{*}K\to PK$ is an isomorphism. Then the functor $P/K:\mathcal{E}/K\to\mathcal{E}/PK$ is represented by the polynomial $(\eta,g^{\prime},h^{\prime}\varepsilon)$. ∎

We introduce the notion of class of polynomial functors which is a generalization of the family of classes of functors $(\mathbf{Poly}_{\mathcal{E}}(I,J))_{I,J\in\mathcal{E}}$. This generalization is necessary to apply Theorem 35 on the existence of $W$-types for a wide range of categorical constructions (see Section 4.1 and 4.2).

Definition 13**.**

Let $\mathcal{E}$ be a locally cartesian closed category with $W$-types. A class of polynomial functors consists of a class $\mathscr{P}(I,J)$ of functors $\mathcal{E}/I\to\mathcal{E}/J$ for each pair of objects $I,J\in\mathcal{E}$ satisfying the following conditions.

If $P:\mathcal{E}/I\to\mathcal{E}/J$ belongs to $\mathbf{Poly}(I,J)$, then it also belongs to $\mathscr{P}(I,J)$. 2. 2.

If $P:\mathcal{E}/I\to\mathcal{E}/J$ belongs to $\mathscr{P}(I,J)$ and $Q:\mathcal{E}/J\to\mathcal{E}/K$ belongs to $\mathscr{P}(J,K)$, then $QP$ belongs to $\mathscr{P}(I,K)$. 3. 3.

If $P:\mathcal{E}/I\to\mathcal{E}/J$ belongs to $\mathscr{P}(I,J)$ and $P\cong Q$, then $Q$ belongs to $\mathscr{P}(I,J)$. 4. 4.

If $P:\mathcal{E}/I\to\mathcal{E}/J$ belongs to $\mathscr{P}(I,J)$, then $P/K:\mathcal{E}/K\to\mathcal{E}/PK$ belongs to $\mathscr{P}(K,PK)$ for any object $K\in\mathcal{E}/I$. 5. 5.

For any endofunctor $P:\mathcal{E}/I\to\mathcal{E}/I$ that belongs to $\mathscr{P}(I,I)$, there exists an initial $P$-algebra.

Example 14*.*

For a locally cartesian closed category $\mathcal{E}$ with $W$-types, the classes $(\mathbf{Poly}(I,J))_{I,J\in\mathcal{E}}$ form a class of polynomial functors by Proposition 11 and 12.

Example 15*.*

Let $\mathscr{P}$ be a class of polynomial functors on a locally cartesian closed category $\mathcal{E}$ with $W$-types. For an object $K\in\mathcal{E}$ and objects $I,J\in\mathcal{E}/K$, we define a class $\mathscr{P}/K(I,J)$ of functors $(\mathcal{E}/K)/I\to(\mathcal{E}/K)/J$ to be the class of functors that belong to $\mathscr{P}(I,J)$ under the identification $(\mathcal{E}/K)/I\cong\mathcal{E}/I$ and $(\mathcal{E}/K)/J\cong\mathcal{E}/J$. Then $(\mathscr{P}/K(I,J))_{I,J\in\mathcal{E}/K}$ form a class of polynomial functors on $\mathcal{E}/K$.

Remark 16*.*

Clearly $\mathbf{Poly}_{\mathcal{E}/K}\subset\mathbf{Poly}_{\mathcal{E}}/K$ holds, but $\mathbf{Poly}_{\mathcal{E}}/K\subset\mathbf{Poly}_{\mathcal{E}/K}$ need not hold.

2.1 The Characterization Theorem

In some nice category $\mathcal{E}$, $W$-types have a nice characterization due to van den Berg [Ber05]. To achieve this characterization, the category $\mathcal{E}$ should be extensive [CLW93].

Definition 17**.**

An extensive category is a category $\mathcal{E}$ with finite coproduct such that, for any objects $A,B\in\mathcal{E}$, the coproduct functor

[TABLE]

is an equivalence of categories.

When $\mathcal{E}$ is locally cartesian closed, the extensivity of $\mathcal{E}$ is equivalent to much simpler conditions.

Definition 18**.**

Let $\mathcal{E}$ be a category with finite coproducts. We say a binary coproduct $A+B$ in $\mathcal{E}$ is disjoint if the inclusions $A\to A+B$ and $B\to A+B$ are monic and the pullback of these inclusions is the initial object.

Proposition 19**.**

Let $\mathcal{E}$ be a locally cartesian closed category with finite coproducts. The following conditions are equivalent.

$\mathcal{E}$* is extensive.* 2. 2.

Binary coproducts in $\mathcal{E}$ are disjoint. 3. 3.

The binary coproduct $1+1$ is disjoint.

Proof.

It is known that a category with finite coproducts is extensive if and only if binary coproducts are universal and disjoint [CLW93, Proposition 2.14]. Binary coproducts in a locally cartesian closed category $\mathcal{E}$ are always universal because pullback functors have right adjoints. Hence the conditions 1 and 2 are equivalent. Trivially 2 implies 3. Suppose that the coproduct $1+1$ is disjoint. To show that any binary coproduct $A+B$ is disjoint, it suffices to show that the pullback of the inclusions $A\to A+B$ and $B\to A+B$ is the initial object [CLW93, Proposition 2.13] because binary coproducts are universal. Now we have a morphism $A\times_{A+B}B\to 1\times_{1+1}1\cong 0$. Since $\mathcal{E}$ is cartesian closed, the initial object is strict [Joh02, A1.5.12]. Hence $A\times_{A+B}B$ is the initial object. ∎

Definition 20**.**

Let $\mathcal{E}$ be a category. We say an object $A\in\mathcal{E}$ is well-founded if any monomorphism $X\rightarrowtail A$ into $A$ is an isomorphism.

Definition 21**.**

Let $P:\mathcal{E}\to\mathcal{E}$ be an endofunctor on a category. A fixed point of $P$ is a $P$-algebra $(X,s)$ such that $s:PX\to X$ is an isomorphism.

Theorem 22** (Characterization Theorem).**

*Let $\mathcal{E}$ be an extensive locally cartesian closed category with a natural number object and

{I}$${A}$${B}$${I}$$\scriptstyle{h}$$\scriptstyle{g}$$\scriptstyle{f}

an endopolynomial in $\mathcal{E}$. For a $P_{f,g,h}$-algebra $(X,s_{X})$, the following conditions are equivalent.*

$(X,s_{X})$* is an initial $P_{f,g,h}$-algebra.* 2. 2.

$(X,s_{X})$* is a well-founded fixed point of $P_{f,g,h}$, namely a fixed point of $P_{f,g,h}$ that is well-founded in the category $\mathrm{Alg}(P_{f,g,h})$.*

Proof.

The proof is similar to [Ber05, Theorem 26]. ∎

3 Comonads

We review the theory of (cartesian) comonads.

Notation 23**.**

Let $G$ be a comonad on a category $\mathcal{E}$. We will refer to the counit and comultiplication of $G$ as $\varepsilon_{G}:G\Rightarrow 1$ and $\delta_{G}:G\Rightarrow GG$ respectively. We denote by $\mathcal{E}_{G}$ the category of $G$-coalgebras, by $U_{G}:\mathcal{E}_{G}\to\mathcal{E}$ the forgetful functor and by $F_{G}$ the right adjoint to $U_{G}$ such that $U_{G}F_{G}=G$. We will refer to the unit of the adjunction $U_{G}\dashv F_{G}$ as $\eta_{G}:1\Rightarrow F_{G}U_{G}$.

Definition 24**.**

Let $\mathcal{E}$ be a cartesian category. A cartesian comonad on $\mathcal{E}$ is a comonad $G$ on $\mathcal{E}$ whose underlying functor $\mathcal{E}\to\mathcal{E}$ preserves finite limits.

The following Lemma 25 is well-known.

Lemma 25**.**

Let $G$ be a comonad on a category $\mathcal{E}$.

The forgetful functor $U_{G}:\mathcal{E}_{G}\to\mathcal{E}$ creates colimits. 2. 2.

If $G$ is cartesian, then $U_{G}:\mathcal{E}_{G}\to\mathcal{E}$ creates finite limits.

Proposition 26**.**

Let $G$ be a cartesian comonad on a cartesian category $\mathcal{E}$. If $\mathcal{E}$ is locally cartesian closed, then so is $\mathcal{E}_{G}$.

Proposition 26 is a well-known fact [Joh02, A4.2.1]. We concretely describe the construction of pushforward functors.

First we recall the adjoint lifting theorem [Joh75].

Definition 27**.**

Let $\mathcal{E}$ and $\mathcal{F}$ be categories, $G$ a comonad on $\mathcal{E}$ and $H$ a comonad on $\mathcal{F}$. An oplax morphism $G\to H$ consists of a functor $S:\mathcal{E}\to\mathcal{F}$ and a natural transformation $\sigma:SG\Rightarrow HS$ satisfying $\varepsilon_{H}S\circ\sigma=S\varepsilon_{G}$ and $\delta_{H}S\circ\sigma=H\sigma\circ\sigma G\circ S\delta_{G}$.

Proposition 28**.**

Let $\mathcal{E}$ and $\mathcal{F}$ be categories, $G$ a comonad on $\mathcal{E}$, $H$ a comonad on $\mathcal{F}$ and $S:\mathcal{E}\to\mathcal{F}$ a functor. A natural transformation $\sigma:SG\Rightarrow HS$ that makes $S$ an oplax morphism $G\to H$ bijectively corresponds to a functor $T:\mathcal{E}_{G}\to\mathcal{F}_{H}$ such that $U_{H}T=SU_{G}$.

Proposition 29** (Adjoint Lifting Theorem).**

Let $\mathcal{E}$ and $\mathcal{F}$ be cartesian categories, $G$ a cartesian comonad on $\mathcal{E}$, $H$ a cartesian comonad on $\mathcal{F}$ and $(S,\sigma):G\to H$ an oplax morphism. Let $T:\mathcal{E}_{G}\to\mathcal{F}_{H}$ denote the corresponding functor such that $U_{H}T=SU_{G}$. If $S:\mathcal{E}\to\mathcal{F}$ has a right adjoint $R:\mathcal{F}\to\mathcal{E}$ with unit $i$ and counit $e$, then $T$ has a right adjoint defined by the equalizer of the following coreflexive pair:

[TABLE]

$\varphi_{1}$* is the composite*

[TABLE]

where $\tilde{\sigma}:GR\to RH$ is the mate of $\sigma$, namely the composite

[TABLE]

$\varphi_{2}$* is $F_{G}RU_{H}\eta_{H}:F_{G}RU_{H}\to F_{G}RU_{H}F_{H}U_{H}=F_{G}RHU_{H}$.*

A slice of a category of coalgebras is again a category of coalgebras in the following sense. Let $G$ be a cartesian comonad on a cartesian category $\mathcal{E}$. For a $G$-coalgebra $(A,\alpha)$, we define a functor $G_{\alpha}:\mathcal{E}/A\to\mathcal{E}/A$ to be the composite

[TABLE]

One can show that $G_{\alpha}$ is equipped with a comonad structure. By definition $G_{\alpha}$ is cartesian. For a morphism of $G$-coalgebras $f:(A,\alpha)\to(B,\beta)$, the canonical natural transformation $G_{\alpha}f^{*}\Rightarrow f^{*}G_{\beta}$ is an isomorphism. The category $(\mathcal{E}/A)_{G_{\alpha}}$ of $G_{\alpha}$-coalgebras is naturally isomorphic to the slice category $\mathcal{E}_{G}/(A,\alpha)$.

Now we can describe pushforwards in a category of coalgebras. Let $f:(A,\alpha)\to(B,\beta)$ be a morphism of $G$-coalgebras. We identify slice categories $\mathcal{E}_{G}/(A,\alpha)$ with $(\mathcal{E}/A)_{G_{\alpha}}$. By Proposition 29 the pushforward $\Pi^{\mathcal{E}_{G}}_{f}$ is the equalizer of the following coreflexive pair:

[TABLE]

$\varphi_{1}$ is the composite

[TABLE]

where $\sigma:G_{\beta}\Pi^{\mathcal{E}}_{f}\to\Pi^{\mathcal{E}}_{f}G_{\alpha}$ is the mate of the natural isomorphism $f^{*}G_{\beta}\cong G_{\alpha}f^{*}$; $\varphi_{2}$ is $F_{G_{\beta}}\Pi^{\mathcal{E}}_{f}U_{G_{\alpha}}\eta_{G_{\alpha}}:F_{G_{\beta}}\Pi^{\mathcal{E}}_{f}U_{G_{\alpha}}\to F_{G_{\beta}}\Pi^{\mathcal{E}}_{f}U_{G_{\alpha}}F_{G_{\alpha}}U_{G_{\alpha}}=F_{G_{\beta}}\Pi^{\mathcal{E}}_{f}G_{\alpha}U_{G_{\alpha}}$.

The following Proposition 30 describes algebras in the category of coalgebras for a comonad.

Proposition 30**.**

Let $G$ be a comonad on a category $\mathcal{E}$ and $(P,\sigma)$ an oplax morphism $G\to G$. Let $Q:\mathcal{E}_{G}\to\mathcal{E}_{G}$ denote the corresponding functor such that $U_{G}Q=PU_{G}$. The forgetful functor $U_{G}$ induces a functor $\mathrm{Alg}(Q)\to\mathrm{Alg}(P)$. Since $(G,\sigma)$ is a lax morphism $P\to P$, we have a functor $H:\mathrm{Alg}(P)\to\mathrm{Alg}(P)$ defined by $H(X,s)=(GX,Gs\circ\sigma(X))$.

$H$* is part of a comonad on $\mathrm{Alg}(P)$.* 2. 2.

$U_{P}H=GU_{P}$* and $(U_{P},1)$ is an oplax morphism $H\to G$. Now we have a commutative diagram*

[TABLE] 3. 3.

The category $\mathrm{Alg}(Q)$ of $Q$-algebras is isomorphic over $\mathcal{E}_{G}\times_{\mathcal{E}}\mathrm{Alg}(P)$ to the category $\mathrm{Alg}(P)_{H}$ of $H$-coalgebras. 4. 4.

For any initial $P$-algebra $(W,s)$, there exists a unique initial $Q$-algebra $(W^{\prime},s^{\prime})$ such that $U_{G}W^{\prime}=W$ and $U_{G}s^{\prime}=s$.

Proof.

1 and 2 are straightforward. To see 3, observe that both a $Q$-algebra and a $H$-coalgebra consist of the following data:

• •

an object $A\in\mathcal{E}$;

• •

a morphism $\alpha:A\to GA$;

• •

a morphism $s:PA\to A$

such that $\alpha$ is a $G$-coalgebra and the following diagram commutes.

[TABLE]

4 follows from 3 and Lemma 25. ∎

Corollary 31**.**

Let $G$ be a cartesian comonad on a cartesian category $\mathcal{E}$ with finite coproducts. Then the forgetful functor $U_{G}:\mathcal{E}_{G}\to\mathcal{E}$ creates natural number objects.

Proof.

By Lemma 25, the diagram

[TABLE]

commutes. Then use Proposition 30. ∎

4 $W$-Types in Categories of Coalgebras

We show the main theorem: the existence of $W$-types in the category of coalgebras for a cartesian comonad. We also give some applications of this theorem.

Lemma 32**.**

Let $\mathcal{E}$ be an extensive locally cartesian closed category. If $\mathcal{E}$ has $W$-types, then it has a natural number object.

Proof.

Because the natural number object is the initial algebra for the associated functor of the polynomial

[TABLE]

∎

Lemma 33**.**

Let $G$ be a cartesian comonad on a locally cartesian closed category $\mathcal{E}$. If $\mathcal{E}$ is an extensive category, then so is $\mathcal{E}_{G}$.

Proof.

By Lemma 25, the binary coproduct $1+1$ in $\mathcal{E}_{G}$ is disjoint. Then use Proposition 19. ∎

Lemma 34**.**

Let $\mathcal{E}$ be a locally cartesian closed category, $P_{0},P_{1}:\mathcal{E}\to\mathcal{E}$ endofunctors and $\varphi,\psi:P_{0}\Rightarrow P_{1}$ and $\varepsilon:P_{1}\Rightarrow P_{0}$ natural transformations such that $\varepsilon\varphi=\varepsilon\psi=1$. Let $\iota:P\Rightarrow P_{0}$ denote the equalizer of $\varphi$ and $\psi$. Suppose that $P_{0}$ preserves pullbacks and $P_{1}$ preserves monomorphisms. If $P_{0}$ and $P_{1}$ have initial algebras, then $P$ has a well-founded fixed point.

We will prove Lemma 34 in Section 5.

Theorem 35**.**

Let $\mathcal{E}$ be an extensive locally cartesian closed category with $W$-types, $\mathscr{P}$ a class of polynomial functors on $\mathcal{E}$ and $G$ a cartesian comonad on $\mathcal{E}$. Suppose that the underlying functor $\mathcal{E}\to\mathcal{E}$ of $G$ belongs to $\mathscr{P}(1,1)$. Then the category $\mathcal{E}_{G}$ of $G$-coalgebras has $W$-types.

Proof.

Let

[TABLE]

be an endopolynomial in $\mathcal{E}_{G}$. Since $f_{!}$ preserves equalizers, the endofunctor $P_{f,g,h}:\mathcal{E}_{G}/(I,\iota)\to\mathcal{E}_{G}/(I,\iota)$ is an equalizer of the form

[TABLE]

where $P_{0}=f_{!}F_{G_{\beta}}\Pi^{\mathcal{E}}_{f}U_{G_{\alpha}}h^{*}$ and $P_{1}=f_{!}F_{G_{\beta}}\Pi^{\mathcal{E}}_{f}G_{\alpha}U_{G_{\alpha}}h^{*}$, and both $\varphi$ and $\psi$ are sections of a natural transformation $P_{1}\Rightarrow P_{0}$ (see Section 3). Since the forgetful functor $U_{G}:\mathcal{E}_{G}\to\mathcal{E}$ creates finite limits, we have $P_{0}=f_{!}F_{G_{\beta}}\Pi^{\mathcal{E}}_{f}h^{*}U_{G_{\iota}}$ and $P_{1}=f_{!}F_{G_{\beta}}\Pi^{\mathcal{E}}_{f}G_{\alpha}h^{*}U_{G_{\iota}}$. We define $Q_{0}:\mathcal{E}/I\to\mathcal{E}/I$ to be $f_{!}G_{\beta}\Pi^{\mathcal{E}}_{f}h^{*}$ and $Q_{1}:\mathcal{E}/I\to\mathcal{E}/I$ to be $f_{!}G_{\beta}\Pi^{\mathcal{E}}_{f}G_{\alpha}h^{*}$. Then we have $U_{G_{\iota}}P_{0}=U_{G_{\iota}}f_{!}F_{G_{\beta}}\Pi^{\mathcal{E}}_{f}h^{*}U_{G_{\iota}}=f_{!}U_{\beta}F_{G_{\beta}}\Pi^{\mathcal{E}}_{f}h^{*}U_{G_{\iota}}=f_{!}G_{\beta}\Pi^{\mathcal{E}}_{f}h^{*}U_{G_{\iota}}=Q_{0}U_{G_{\iota}}$ and similarly $U_{G_{\iota}}P_{1}=Q_{1}U_{G_{\iota}}$. Since $Q_{0}$ and $Q_{1}$ belong to $\mathscr{P}(I,I)$ by construction, they have initial algebras, and so do $P_{0}$ and $P_{1}$ by Proposition 30. By construction $P_{0}$ and $P_{1}$ preserve pullbacks, and thus there exists a well-founded fixed point $(W,s)$ of $P_{f,g,h}$ by Lemma 34. By Theorem 22 $(W,s)$ is an initial $P_{f,g,h}$-algebra, because $\mathcal{E}_{G}$ has a natural number object by Lemma 32 and Corollary 31 and is extensive by Lemma 33. ∎

4.1 Application: Internal Diagrams

Let $C$ be an internal category in a locally cartesian closed category $\mathcal{E}$. We denote by $\partial_{0}$ and $\partial_{1}$ the domain and codomain morphisms

{C_{1}}$${C_{0}}

respectively. The category $\mathcal{E}^{C}$ of internal diagrams on $C$ is isomorphic to the category of coalgebras for the cartesian comonad

[TABLE]

on $\mathcal{E}/C_{0}$. It is known that the diagonal functor $\Delta:\mathcal{E}\to\mathcal{E}^{C}$ is a locally cartesian closed functor.

Corollary 36**.**

Let $\mathcal{E}$ be an extensive locally cartesian closed category and $C$ an internal category in $\mathcal{E}$. If $\mathcal{E}$ has $W$-types, then so does the category $\mathcal{E}^{C}$ of internal diagrams on $C$. Moreover, the diagonal functor $\Delta:\mathcal{E}\to\mathcal{E}^{C}$ preserves $W$-types.

Proof.

Apply Theorem 35 with $\mathscr{P}=\mathbf{Poly}_{\mathcal{E}}/C_{0}$. The preservation of $W$-types follows from Proposition 10 because $\Delta$ has a right adjoint. ∎

4.2 Application: Gluing

Let $H:\mathcal{E}_{1}\to\mathcal{E}_{2}$ be a cartesian functor between locally cartesian closed categories. Since the comma category $(\mathcal{E}_{2}\downarrow H)$ is isomorphic to the category of coalgebras for the cartesian comonad $(X_{1},X_{2})\mapsto(X_{1},HX_{1}\times X_{2})$ on $\mathcal{E}_{1}\times\mathcal{E}_{2}$, it is locally cartesian closed. From the construction of pushforwards described in Section 3 we know that the projection $\pi_{1}:(\mathcal{E}_{2}\downarrow H)\to\mathcal{E}_{1}$ is a locally cartesian closed functor.

Corollary 37**.**

Let $H:\mathcal{E}_{1}\to\mathcal{E}_{2}$ be a cartesian functor between extensive locally cartesian closed categories. If $\mathcal{E}_{1}$ and $\mathcal{E}_{2}$ have $W$-types, then so does $(\mathcal{E}_{2}\downarrow H)$. Moreover, the projection $\pi_{1}:(\mathcal{E}_{2}\downarrow H)\to\mathcal{E}_{1}$ preserves $W$-types.

To show Corollary 37, we define an appropriate class of polynomial functors on $\mathcal{E}_{1}\times\mathcal{E}_{2}$.

Definition 38**.**

Let $\mathcal{E}_{1}$ and $\mathcal{E}_{2}$ be locally cartesian closed categories with $W$-types and $\mathscr{P}_{1}$ and $\mathscr{P}_{2}$ classes of polynomial functors on $\mathcal{E}_{1}$ and $\mathcal{E}_{2}$ respectively. For objects $(I_{1},I_{2}),(J_{1},J_{2})\in\mathcal{E}_{1}\times\mathcal{E}_{2}$, we define a class $\mathscr{P}_{1}\rtimes\mathscr{P}_{2}((I_{1},I_{2}),(J_{1},J_{2}))$ of functors $(\mathcal{E}_{1}\times\mathcal{E}_{2})/(I_{1},I_{2})\cong\mathcal{E}_{1}/I_{1}\times\mathcal{E}_{2}/I_{2}\to\mathcal{E}_{1}/J_{1}\times\mathcal{E}_{2}/J_{2}\cong(\mathcal{E}_{1}\times\mathcal{E}_{2})/(J_{1},J_{2})$ to be the class of functors of the form $(F_{1}\circ\pi_{1},F_{2})$ with $F_{1}:\mathcal{E}_{1}/I_{1}\to\mathcal{E}_{1}/J_{1}$ and $F_{2}:\mathcal{E}_{1}/I_{1}\times\mathcal{E}_{2}/I_{2}\to\mathcal{E}_{2}/J_{2}$ such that $F_{1}$ belongs to $\mathscr{P}_{1}(I_{1},J_{1})$ and $F_{2}(K,-)$ belongs to $\mathscr{P}_{2}(I_{2},J_{2})$ for every $K\in\mathcal{E}_{1}/I_{1}$.

Proposition 39**.**

For classes $\mathscr{P}_{1}$ and $\mathscr{P}_{2}$ of polynomial functors on locally cartesian closed categories with $W$-types $\mathcal{E}_{1}$ and $\mathcal{E}_{2}$ respectively, $\mathscr{P}_{1}\rtimes\mathscr{P}_{2}$ is a class of polynomial functors on $\mathcal{E}_{1}\times\mathcal{E}_{2}$.

Proof.

A functor of the form $F_{1}\times F_{2}$ with $F_{1}\in\mathscr{P}_{1}(I_{1},J_{1})$ and $F_{2}\in\mathscr{P}_{2}(I_{2},J_{2})$ belongs to $\mathscr{P}_{1}\rtimes\mathscr{P}_{2}((I_{1},I_{2}),(J_{1},J_{2}))$, and thus $\mathbf{Poly}_{\mathcal{E}_{1}\times\mathcal{E}_{2}}((I_{1},I_{2}),(J_{1},J_{2}))\subset\mathscr{P}_{1}\rtimes\mathscr{P}_{2}$. It is also clear that $\mathscr{P}_{1}\rtimes\mathscr{P}_{2}$ is closed under isomorphism. To see that it is closed under composition, let $F_{1}:\mathcal{E}_{1}/I_{1}\to\mathcal{E}_{1}/J_{1}$, $F_{2}:\mathcal{E}_{1}/I_{1}\times\mathcal{E}_{2}/I_{2}\to\mathcal{E}_{2}/J_{2}$, $G_{1}:\mathcal{E}_{1}/J_{1}\to\mathcal{E}_{1}/K_{1}$ and $G_{2}:\mathcal{E}_{1}/J_{1}\times\mathcal{E}_{2}/J_{2}\to\mathcal{E}_{2}/K_{2}$ be functors such that $F_{1}\in\mathscr{P}_{1}(I_{1},J_{1}))$, $G_{1}\in\mathscr{P}_{1}(J_{1},K_{1})$, $F_{2}(X_{1},-)\in\mathscr{P}_{2}(I_{2},J_{2})$ and $G_{2}(Y_{1},-)\in\mathscr{P}_{2}(J_{2},K_{2})$ for any $X_{1}\in\mathcal{E}_{1}/I_{1}$ and $Y_{1}\in\mathcal{E}_{1}/J_{1}$. Then we have $(G_{1}\pi_{1},G_{2})\circ(F_{1}\pi_{1},F_{2})=(G_{1}F_{1}\pi_{1},G_{2}(F_{1}\pi_{1},F_{2}))$ and $G_{1}F_{1}\in\mathscr{P}_{1}(I_{1},K_{1})$ and $G_{2}(F_{1}\pi_{1},F_{2})(X_{1},-)=G_{2}(F_{1}(X_{1}),-)\circ F_{2}(X_{1},-)\in\mathscr{P}_{2}(I_{2},K_{2})$ for any $X_{1}\in\mathcal{E}_{1}/I_{1}$.

To show that $\mathscr{P}_{1}\rtimes\mathscr{P}_{2}$ is closed under slice, let $F_{1}:\mathcal{E}_{1}/I_{1}\to\mathcal{E}_{1}/J_{1}$ and $F_{2}:\mathcal{E}_{1}/I_{1}\times\mathcal{E}_{2}/I_{2}\to\mathcal{E}_{2}/J_{2}$ be functors and $(K_{1},K_{2})\in\mathcal{E}_{1}/I_{1}\times\mathcal{E}_{2}/I_{2}$ objects such that $F_{1}\in\mathscr{P}_{1}(I_{1},J_{1})$ and $F_{2}(X_{1},-)\in\mathscr{P}_{2}(I_{2},J_{2})$ for any $X_{1}\in\mathcal{E}_{1}/I_{1}$. Then we have $(F_{1}\pi_{1},F_{2})/(K_{1},K_{2})=((F_{1}/K_{1})\pi_{1},F_{2}/(K_{1},K_{2}))$ and $F_{1}/K_{1}\in\mathscr{P}_{1}(K_{1},FK_{1})$. We also have $(F_{2}/(K_{1},K_{2}))(X_{1},-)\in\mathscr{P}_{2}(K_{2},F_{2}(K_{1},K_{2}))$ for any $X_{1}\in\mathcal{E}_{1}/K_{1}$ because it is the composite

[TABLE]

Finally we show the existence of initial algebras. Let $F_{1}:\mathcal{E}_{1}/I_{1}\to\mathcal{E}_{1}/I_{1}$ and $F_{2}:\mathcal{E}_{1}/I_{1}\times\mathcal{E}_{2}/I_{2}\to\mathcal{E}_{2}/I_{2}$ be functors such that $F_{1}\in\mathscr{P}_{1}(I_{1},I_{1})$ and $F_{2}(X_{1},-)\in\mathscr{P}_{2}(I_{2},I_{2})$ for any $X_{1}\in\mathcal{E}_{1}/I_{1}$. Let $(W_{1},s_{1})$ be the initial $F_{1}$-algebra and $(W_{2},s_{2})$ the initial $F_{2}(W_{1},-)$-algebra. Then the object $(W_{1},W_{2})\in\mathcal{E}_{1}/I_{1}\times\mathcal{E}_{2}/I_{2}$ and the morphism $(s_{1},s_{2}):(F_{1}W_{1},F_{2}(W_{1},W_{2}))\to(W_{1},W_{2})$ form a $(F_{1}\pi_{1},F_{2})$-algebra. Let $(t_{1},t_{2}):(F_{1}X_{1},F_{2}(X_{1},X_{2}))\to(X_{1},X_{2})$ be another $(F_{1}\pi_{1},F_{2})$-algebra. A morphism $((W_{1},W_{2}),(s_{1},s_{2}))\to((X_{1},X_{2}),(t_{1},t_{2}))$ of $(F_{1}\pi_{1},F_{2})$-algebras consists of a morphism $h_{1}:W_{1}\to X_{1}$ and $h_{2}:W_{2}\to X_{2}$ such that $h_{1}\circ s_{1}=t_{1}\circ F_{1}h_{1}$ and $h_{2}\circ s_{2}=t_{2}\circ F_{2}(h_{1},h_{2})$. The second condition is equivalent to that $h_{2}$ is a morphism of $F_{2}(W_{1},-)$-algebras $(W_{2},s_{2})\to(X_{2},t_{2}\circ F_{2}(h_{1},X_{2}))$. Hence, there exists a unique pair of morphisms $(h_{1},h_{2})$ satisfying these conditions by the initiality of $(W_{1},s_{1})$ and $(W_{2},s_{2})$. ∎

Proof of Corollary 37.

Apply Theorem 35 with $\mathscr{P}=\mathbf{Poly}_{\mathcal{E}_{1}}\rtimes\mathbf{Poly}_{\mathcal{E}_{2}}$. The preservation of $W$-types follows from Proposition 10 because $\pi_{1}$ has a right adjoint. ∎

5 Algebras for the Equalizer of a Coreflexive Pair

In this section we prove Lemma 34: the existence of a well-founded fixed point for an endofunctor defined as the equalizer of a coreflexive pair.

Lemma 40**.**

Suppose that we are given the following commutative diagram in a cartesian category

[TABLE]

where $A$ is the equalizer of $f$ and $g$, $X$ is the equalizer of $u$ and $v$, and $q$ is a monomorphism. Then the induced morphism $X\to A$ is the pullback of $p$ along $A\to B$.

Proof.

For a morphism $h:W\to Y$, the following conditions are equivalent.

• •

$h$ factors through $X$

• •

$uh=vh$

• •

$quh=qvh$

• •

$fph=gph$

• •

$ph$ factors through $A$

∎

Proof of Lemma 34.

Let $s_{0}:P_{0}W_{0}\to W_{0}$ and $s_{1}:P_{1}W_{1}\to W_{1}$ be initial $P_{0}$- and $P_{1}$-algebras respectively. By the initiality of $W_{0}$ and $W_{1}$, we have morphisms $u,v:W_{0}\to W_{1}$ and $e:W_{1}\to W_{0}$ such that $u\circ s_{0}=s_{1}\circ\varphi\circ P_{0}u$, $v\circ s_{0}=s_{1}\circ\psi\circ P_{0}v$, $e\circ s_{1}=s_{0}\circ\varepsilon\circ P_{1}e$ and $eu=ev=1$. Let $i:W\to W_{0}$ be the equalizer of $u$ and $v$. Consider the diagram

[TABLE]

where all rows are equalizers. Since $P_{1}$ preserves monomorphisms, $PW$ is the pullback of $PW_{0}$ along $P_{0}i:P_{0}W\to P_{0}W_{0}$ by Lemma 40 . $P_{0}$ also preserves monomorphisms because it preserves pullbacks. Therefore $PW$ is the intersection of $PW_{0}$ and $P_{0}W$ in the poset of subobjects of $P_{0}W_{0}$. For a morphism $f:Z\to P_{0}W_{0}$, the following conditions are equivalent.

$f$ factors through $PW$. 2. 2.

$\varphi(W_{0})\circ f=\psi(W_{0})\circ f$ and $P_{0}u\circ f=P_{0}v\circ f$. 3. 3.

$P_{1}u\circ\varphi(W_{0})\circ f=P_{1}v\circ\psi(W_{0})\circ f$. 4. 4.

$\varphi(W_{1})\circ P_{0}u\circ f=\psi(W_{1})\circ P_{0}v\circ f$.

The conditions 1 and 2 are equivalent by definition. The conditions 3 and 4 are equivalent by the naturality of $\varphi$ and $\psi$. From 2, we have 3 as $P_{1}u\circ\varphi(W_{0})\circ f=P_{1}u\circ\psi(W_{0})\circ f=\psi(W_{1})\circ P_{0}u\circ f=\psi(W_{1})\circ P_{0}v\circ f=P_{1}v\circ\psi(W_{0})\circ f$. 3 and 4 imply 2 because $eu=ev=1$ and $\varepsilon\varphi=\varepsilon\psi=1$. Hence, $PW$ is also an equalizer of $\varphi(W_{1})\circ P_{0}u$ and $\psi(W_{1})\circ P_{0}v$. In the following diagram,

[TABLE]

all rows are equalizers and $s_{0}$ and $s_{1}$ are isomorphisms, and thus the morphism $PW\to W_{0}$ factors as $i\circ s$ with an isomorphism $s:PW\to W$.

We show that $(W,s)$ is a well-founded $P$-algebra. Let $(X,t:PX\to X)$ be a $P$-algebra and $j:X\rightarrowtail W$ a monomorphism that is a morphism of $P$-algebras. Let $X_{0}$ denote the pushforward $i_{*}X$. Since $i$ is a monomorphism, we have a pullback

[TABLE]

Hence, it suffices to show that the monomorphism $X_{0}\to W_{0}$ is an isomorphism. To prove this, it is enough to see that $X_{0}$ carries a $P_{0}$-algebra structure over $s_{0}:P_{0}W_{0}\to W_{0}$, that is, the composite

{P_{0}X_{0}}$${P_{0}W_{0}}$${W_{0}}$$\scriptstyle{s_{0}}

factors through $X_{0}\rightarrowtail W_{0}$.

[TABLE]

Since $X_{0}=i_{*}X$ and $i^{*}P_{0}W_{0}\cong PW$, it is equivalent to that the composite

{i^{*}P_{0}X_{0}}$${i^{*}P_{0}W_{0}\cong PW}$${W}$$\scriptstyle{s}

factors through $X\rightarrowtail W$. Since $X$ has a $P$-algebra structure over $s:PW\to W$, it suffices to show that $i^{*}P_{0}X_{0}\to PW$ factors through $PX\rightarrowtail PW$. Now $P$ is the equalizer of $\varphi,\psi:P_{0}\Rightarrow P_{1}$ and $P_{1}X\to P_{1}W$ is a monomorphism, and thus the square

[TABLE]

is a pullback by Lemma 40. Hence, to show that $i^{*}P_{0}X_{0}\to PW$ factors through $PX$, it suffices to show that the composite

{i^{*}P_{0}X_{0}}$${PW}$${P_{0}W}$$\scriptstyle{\iota(W)}

factors through $P_{0}X$. Since $P_{0}$ preserves pullbacks, we have a pullback

[TABLE]

and thus it is enough to show that the composite

{i^{*}P_{0}X_{0}}$${PW}$${P_{0}W}$${P_{0}W_{0}}$$\scriptstyle{\iota(W)}$$\scriptstyle{P_{0}i}

factors through $P_{0}X_{0}\to P_{0}W_{0}$. But this is true because $i^{*}P_{0}X_{0}$ is the pullback

[TABLE]

and $\iota(W_{0})\circ Pi=P_{0}i\circ\iota(W)$ by the naturality of $\iota$. ∎