W-Types with Reductions and the Small Object Argument

TL;DR

This paper introduces a new class of higher inductive types called W-types with reductions, generalizing dependent W-types, and explores their existence in various toposes and their applications in algebraic weak factorisation systems.

Contribution

It defines W-types with reductions as initial algebras of pointed polynomial endofunctors and demonstrates their existence under certain set-theoretic conditions, extending the theory of W-types.

Findings

W-types with reductions exist in all $ ext{ extbf{Π}W}$-pretoposes satisfying WISC.

A large class of these types can be constructed in internal presheaf categories without WISC.

They can be used to construct algebraic weak factorisation systems, including cofibrantly generated ones.

Abstract

We define a simple kind of higher inductive type generalising dependent $W$-types, which we refer to as $W$-types with reductions. Just as dependent $W$-types can be characterised as initial algebras of certain endofunctors (referred to as polynomial endofunctors), we will define our generalisation as initial algebras of certain pointed endofunctors, which we will refer to as pointed polynomial endofunctors. We will show that $W$-types with reductions exist in all $\Pi W$-pretoposes that satisfy a weak choice axiom, known as weakly initial set of covers (WISC). This includes all Grothendieck toposes and realizability toposes as long as WISC holds in the background universe. We will show that a large class of $W$-types with reductions in internal presheaf categories can be constructed without using WISC. We will show that $W$-types with reductions suffice to construct some interesting examples of algebraic weak factorisation systems (awfs's). Specifically, we will see how to construct awfs's that are cofibrantly generated with respect to a codomain fibration, as defined in a previous paper by the author.

Equations

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.77083pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&&\crcr}}}\ignorespaces{\hbox{\kern-3.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 30.77083pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 52.48955pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 69.84026pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 9.30583pt\raise-12.9861pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.43056pt\hbox{$\scriptstyle{h}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 6.77084pt\raise-30.32036pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 69.84026pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 95.62476pt\raise-13.22916pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{g}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 107.86803pt\raise-30.24101pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-6.77083pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z}$}}}}}}}{\hbox{\kern 35.30554pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 73.85414pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 107.86803pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.83507pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&&\crcr}}}\ignorespaces{\hbox{\kern-6.83507pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{R\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 14.25261pt\raise 5.43056pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.43056pt\hbox{$\scriptstyle{k}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 30.83507pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 30.83507pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 52.55379pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 69.9045pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 9.34775pt\raise-12.9861pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.43056pt\hbox{$\scriptstyle{h}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 6.77084pt\raise-30.33357pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 69.9045pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 95.689pt\raise-13.22916pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{g}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 107.93227pt\raise-30.24101pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-6.77083pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z}$}}}}}}}{\hbox{\kern 35.36978pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 73.91838pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 107.93227pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$${\Sigma }_h{\Sigma }_k{k}^{\ast }{f}^{\ast }{\Pi }_f{h}^{\ast }⟶{\Sigma }_h{\Sigma }_k{k}^{\ast }{h}^{\ast }⟶{\Sigma }_h{h}^{\ast }⟶{\mathrm{Id}}_{\mathbb{C}/Z}$$

$${\Sigma }_g{\Sigma }_f{\Sigma }_k{k}^{\ast }{f}^{\ast }{\Pi }_f{h}^{\ast }⟶{\Sigma }_g{\Sigma }_f{f}^{\ast }{\Pi }_f{h}^{\ast }⟶{\Sigma }_g{\Pi }_f{h}^{\ast }$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 31.63087pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\crcr}}}\ignorespaces{\hbox{\kern-31.63087pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Sigma_{h}\Sigma_{k}k^{\ast}f^{\ast}\Pi_{f}h^{\ast}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 58.01877pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 0.0pt\raise-30.26666pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 58.01877pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\operatorname{Id}_{\mathbb{C}/Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 70.98044pt\raise-31.68057pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-17.7501pt\raise-41.51389pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Sigma_{g}\Pi_{f}h^{\ast}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 55.63087pt\raise-41.51389pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 55.63087pt\raise-41.51389pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{P_{f,g,h,k}\ignorespaces}$}}}}}}}\ignorespaces{\hbox{\kern 60.79813pt\raise-41.51389pt\hbox{\ignorespaces\ignorespaces\hbox{\kern 0.0pt\raise 10.18231pt\hbox{\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 65.41881pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\crcr}}}\ignorespaces{\hbox{\kern-65.41881pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Sigma_{z:Z}\Sigma_{y:Y(z)}\Sigma_{r:R(y)}\Pi_{x:X(y)}W(h(x))\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 105.65727pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 0.0pt\raise-30.5pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 105.65727pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{W\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 114.07394pt\raise-30.5pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-53.89023pt\raise-41.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Sigma_{z:Z}\Sigma_{y:Y(z)}\Pi_{x:X(y)}W(h(x))\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 89.41881pt\raise-41.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 89.41881pt\raise-41.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{P_{f,g,h,k}(W)\ignorespaces}$}}}}}}}\ignorespaces{\hbox{\kern 103.89163pt\raise-41.0pt\hbox{\ignorespaces\ignorespaces\hbox{\kern 0.0pt\raise 10.18231pt\hbox{\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 65.41881pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&\crcr}}}\ignorespaces{\hbox{\kern-65.41881pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Sigma_{z:Z}\Sigma_{y:Y(z)}\Sigma_{r:R(y)}\Pi_{x:X(y)}W(h(x))\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 48.12451pt\raise-14.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\lambda z,y,r,\alpha.\alpha(x)}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 119.41881pt\raise-38.31226pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 0.0pt\raise-30.5pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 89.41881pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 124.83548pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern-53.89023pt\raise-41.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Sigma_{z:Z}\Sigma_{y:Y(z)}\Pi_{x:X(y)}W(h(x))\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 59.4031pt\raise-45.50694pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.50694pt\hbox{$\scriptstyle{c}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 119.41881pt\raise-41.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 89.41881pt\raise-41.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 119.41881pt\raise-41.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{W}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.83507pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&\crcr}}}\ignorespaces{\hbox{\kern-6.83507pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{R\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 32.60677pt\raise 5.43056pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.43056pt\hbox{$\scriptstyle{k}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 67.54338pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern 30.83507pt\raise-30.54742pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern-2.13171pt\lower-2.11089pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 34.18922pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 67.54338pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X}$}}}}}}}{\hbox{\kern-3.0pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 30.83507pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{S\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 43.54338pt\raise-30.65912pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 56.01315pt\raise-23.8472pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.43056pt\hbox{$\scriptstyle{l}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 71.99313pt\raise-3.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 72.0781pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 31.63087pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&\crcr}}}\ignorespaces{\hbox{\kern-31.63087pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Sigma_{h}\Sigma_{k}k^{\ast}f^{\ast}\Pi_{f}h^{\ast}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 55.63087pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern-3.0pt\lower 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern 67.68623pt\raise-32.89885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 55.63087pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Sigma_{h}\Sigma_{l}l^{\ast}f^{\ast}\Pi_{f}h^{\ast}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 85.43634pt\raise-30.26666pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 140.97443pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 140.97443pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\operatorname{Id}_{\mathbb{C}/Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 153.9361pt\raise-31.68057pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-3.0pt\raise-41.51389pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 67.68623pt\raise-41.51389pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Sigma_{g}\Pi_{f}h^{\ast}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 139.2418pt\raise-41.51389pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 139.2418pt\raise-41.51389pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{P_{f,g,h,l}\ignorespaces}$}}}}}}}\ignorespaces{\hbox{\kern 143.75378pt\raise-41.51389pt\hbox{\ignorespaces\ignorespaces\hbox{\kern 0.0pt\raise 10.18231pt\hbox{\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 8.23508pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&&\crcr}}}\ignorespaces{\hbox{\kern-8.23508pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{R_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 14.6526pt\raise 6.075pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.78612pt\hbox{$\scriptstyle{k_{1}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 32.23508pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 32.23508pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 55.7538pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f_{1}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 74.10449pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 9.04535pt\raise-12.79277pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.78612pt\hbox{$\scriptstyle{h_{1}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 6.77084pt\raise-31.52673pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 74.10449pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Y_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 101.8957pt\raise-13.68027pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{g_{1}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 114.93228pt\raise-31.22258pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-6.77083pt\raise-37.73553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z}$}}}}}}}{\hbox{\kern 38.16978pt\raise-37.73553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 79.51839pt\raise-37.73553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 114.93228pt\raise-37.73553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 8.23508pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&&\crcr}}}\ignorespaces{\hbox{\kern-8.23508pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{R_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 14.6526pt\raise 6.075pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.78612pt\hbox{$\scriptstyle{k_{2}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 32.23508pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 32.23508pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 55.7538pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f_{2}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 74.10449pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 9.04535pt\raise-12.79277pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.78612pt\hbox{$\scriptstyle{h_{2}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 6.77084pt\raise-31.52673pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 74.10449pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Y_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 101.8957pt\raise-13.68027pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{g_{2}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 114.93228pt\raise-31.22258pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-6.77083pt\raise-37.73553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z}$}}}}}}}{\hbox{\kern 38.16978pt\raise-37.73553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 79.51839pt\raise-37.73553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 114.93228pt\raise-37.73553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$$R_1+R_2\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$Q_1+Q_2\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 8.35277pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\crcr}}}\ignorespaces{\hbox{\kern-8.35277pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Q_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 32.35277pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 0.0pt\raise-29.70778pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 32.35277pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\operatorname{Id}_{\mathbb{C}/Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 45.31444pt\raise-29.70778pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-8.30452pt\raise-39.54109pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{P_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 37.56029pt\raise-39.54109pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 37.56029pt\raise-39.54109pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{S_{1}\ignorespaces}$}}}}}}}\ignorespaces{\hbox{\kern 35.13213pt\raise-39.54109pt\hbox{\ignorespaces\ignorespaces\hbox{\kern 0.0pt\raise 10.18231pt\hbox{\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}\quad\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 8.35277pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\crcr}}}\ignorespaces{\hbox{\kern-8.35277pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Q_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 32.35277pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 0.0pt\raise-29.70778pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 32.35277pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\operatorname{Id}_{\mathbb{C}/Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 45.31444pt\raise-29.70778pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-8.30452pt\raise-39.54109pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{P_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 37.56029pt\raise-39.54109pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 37.56029pt\raise-39.54109pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{S_{2}\ignorespaces}$}}}}}}}\ignorespaces{\hbox{\kern 35.13213pt\raise-39.54109pt\hbox{\ignorespaces\ignorespaces\hbox{\kern 0.0pt\raise 10.18231pt\hbox{\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}\quad\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 12.96167pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\crcr}}}\ignorespaces{\hbox{\kern-12.96167pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\operatorname{Id}_{\mathbb{C}/Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 36.96167pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 0.0pt\raise-29.70778pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 36.96167pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{S_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 44.71582pt\raise-29.70778pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-7.75415pt\raise-39.54109pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{S_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 38.36166pt\raise-39.54109pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 38.36166pt\raise-39.54109pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{S\ignorespaces}$}}}}}}}\ignorespaces{\hbox{\kern 34.53351pt\raise-39.54109pt\hbox{\ignorespaces\ignorespaces\hbox{\kern 0.0pt\raise 10.18231pt\hbox{\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 9.58992pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\crcr}}}\ignorespaces{\hbox{\kern-7.27847pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{D\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 14.47292pt\raise 5.1875pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{q}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.27847pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern-9.58992pt\raise-18.41666pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{g}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-27.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 31.27847pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 38.32187pt\raise-18.41666pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 38.32187pt\raise-27.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-6.93124pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 14.4pt\raise-42.0208pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{p}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.57187pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 31.57187pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$$W\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 9.00795pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\crcr}}}\ignorespaces{\hbox{\kern-7.71465pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{A_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 0.0pt\raise-29.50667pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\lower-3.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern 39.95238pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 39.95238pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{W\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 48.36905pt\raise-28.83998pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\lower-3.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-9.00795pt\raise-39.33998pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X_{y}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 18.94557pt\raise-43.84692pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.50694pt\hbox{$\scriptstyle{\alpha}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 33.00795pt\raise-39.33998pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 33.00795pt\raise-39.33998pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{W/{\sim}}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$$A_i\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 9.58992pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\crcr}}}\ignorespaces{\hbox{\kern-6.75pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 14.45433pt\raise 5.1875pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{q}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 30.75pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern-9.58992pt\raise-18.41666pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{g}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-27.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 30.75pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 38.28471pt\raise-18.41666pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 38.28471pt\raise-27.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-6.25346pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{J\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 14.38141pt\raise-42.0208pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{p}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.27083pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 31.27083pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Y}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 10.03311pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\crcr}}}\ignorespaces{\hbox{\kern-7.0434pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 20.5579pt\raise 5.15279pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.15279pt\hbox{$\scriptstyle{t}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.60416pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern-10.03311pt\raise-19.37332pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.43056pt\hbox{$\scriptstyle{h}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-28.91333pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 31.60416pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{A\times_{X}A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 49.6436pt\raise-19.37332pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.5pt\hbox{$\scriptstyle{\langle g,g\rangle}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 49.6436pt\raise-28.91333pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-7.60416pt\raise-38.74664pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{K\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 20.18117pt\raise-43.25359pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.50694pt\hbox{$\scriptstyle{s}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 32.8889pt\raise-38.74664pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 32.8889pt\raise-38.74664pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{J\times_{Y}J}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$$X\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$f^{\ast }(\mathbf{y}(c))\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 8.4139pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&&\crcr}}}\ignorespaces{\hbox{\kern-8.4139pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Y_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 20.64247pt\raise 5.15138pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8625pt\hbox{$\scriptstyle{\iota_{2}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 32.4139pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 32.4139pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X_{1}+Y_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 69.8826pt\raise 6.62944pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.23167pt\hbox{$\scriptstyle{f_{1}+1_{Y_{2}}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 95.11107pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 17.20026pt\raise-13.43721pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.43056pt\hbox{$\scriptstyle{h}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 6.77084pt\raise-32.79626pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 95.11107pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Y_{1}+Y_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 137.58624pt\raise-13.68027pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{g}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 156.76662pt\raise-32.5913pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-6.77083pt\raise-37.73553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z}$}}}}}}}{\hbox{\kern 48.76248pt\raise-37.73553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 110.93884pt\raise-37.73553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 156.76662pt\raise-37.73553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$$N(\tau )(N(\sigma )(\sup (y,\alpha )))$$

$$=N_0(\tau )(\alpha (\sigma ,x))$$

$$=\alpha (\tau \circ \sigma ,X(\tau )(x))$$

$$=N(\tau \circ \sigma )(\sup (y,\alpha ))$$

$${\Sigma }_g{\Pi }_f{h}^{\ast }(N)(c)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\alpha }^{\prime }(x):=\{\begin{array}{ll}{a}_1& x=x_1\\ a_2& x=x_2\\ \alpha (x)& \text{otherwise}\end{array}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 7.02777pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&\\&&\crcr}}}\ignorespaces{\hbox{\kern-6.95901pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{U\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 0.0pt\raise-30.16669pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 31.09653pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\sigma^{\ast}(U)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 6.95901pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 85.37524pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 46.2015pt\raise-29.5pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 36.0192pt\raise 0.0pt\hbox{\ignorespaces\ignorespaces\hbox{\kern 0.0pt\raise-10.18231pt\hbox{\hbox{\kern 0.0pt\lower 0.0pt\hbox{\lower-5.0pt\hbox{\line@@}}}\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{}}}}}}{\hbox{\kern 85.37524pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 92.90996pt\raise-30.16669pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-7.02777pt\raise-40.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{V\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 0.0pt\raise-68.58334pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 31.02777pt\raise-40.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\sigma^{\ast}(V)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 7.02779pt\raise-40.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 85.89607pt\raise-40.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 46.2015pt\raise-68.58334pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 36.0192pt\raise-40.0pt\hbox{\ignorespaces\ignorespaces\hbox{\kern 0.0pt\raise-10.18231pt\hbox{\hbox{\kern 0.0pt\lower 0.0pt\hbox{\lower-5.0pt\hbox{\line@@}}}\hbox{\kern 0.0pt\lower 0.0pt\hbox{\hbox{\line@@}}}\hbox{}}}}}}{\hbox{\kern 85.89607pt\raise-40.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 92.90996pt\raise-68.58334pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-5.59027pt\raise-78.41666pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{I}$}}}}}}}{\hbox{\kern 38.59735pt\raise-78.41666pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{K\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 18.10081pt\raise-73.90971pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.50694pt\hbox{$\scriptstyle{\sigma}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 5.59027pt\raise-78.41666pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 86.6565pt\raise-78.41666pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 86.6565pt\raise-78.41666pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{J}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$${\Sigma }_{i:I}{\Sigma }_{j:J}{\Sigma }_{\beta :V(i)\to Y(j)}{\Pi }_{v:V(i)}(U(i,v)\to X(j,\beta (v)))$$

$${\sigma }^{\ast }(U)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\sigma }^{\ast }(U)$$

Full text

We will show that $W$-types with reductions exist in all $\Pi W$-pretoposes that satisfy a weak choice axiom, known as weakly initial set of covers ($\mathbf{WISC}$). This includes all Grothendieck toposes and realizability toposes as long as $\mathbf{WISC}$ holds in the background universe.

We will show that a large class of $W$-types with reductions in internal presheaf categories can be constructed without using $\mathbf{WISC}$.

We will show that $W$-types with reductions suffice to construct some interesting examples of algebraic weak factorisation systems (awfs’s). Specifically, we will see how to construct awfs’s that are cofibrantly generated with respect to a codomain fibration, as defined in a previous paper by the author.

1 Introduction

A key idea in type theory is that of inductively generated types. The essential idea is that one specifies a way to construct new elements of a type from old, and an inductively generated type is the “least” type matching this specification. The simplest example is the natural numbers, $\mathbb{N}$. It is the type inductively generated by the requirements that [math] is an element of $\mathbb{N}$ and $S(n)$ is an element of $\mathbb{N}$ whenever $n$ is. Since $\mathbb{N}$ is the least such type, we can prove a formula $\varphi$ holds for all natural numbers $n$, by first proving $\varphi$ for [math], then showing $\varphi$ holds for $S(n)$ whenever it holds for $n$.

An important class of inductive types is that of $W$-types. These have elegant categorical semantics due to Moerdijk and Palmgren [17], and later developed further to dependent $W$-types by Gambino and Hyland [9]. In these semantics, $W$-types are implemented as initial algebras of a certain class of endofunctors, known as polynomial endofunctors. Type theoretically the idea (for the simpler non dependent case) is that we are given a type $Y$ that we refer to as constructors and a family of types $X_{y}$ indexed by the elements of $y$, which we refer to as arities. We then construct a type $W$, which contains an element of the form $\sup(y,\alpha)$ whenever $y\in Y$ and $\alpha\colon X_{y}\rightarrow W$.

Higher inductive types are one of the main ideas in homotopy type theory [29], in which one defines a new type by specifying not only how to construct elements of a type, but also how to construct proofs of equality between elements (and also proofs of equality between proofs of equality, etc). A lot of the time the aim here is to construct types with nontrivial higher type structure that represent interesting topological spaces (such as $n$ dimensional spheres) type theoretically. However, there are examples of higher inductive types that are non trivial even when working in an extensional setting, where UIP holds (any two proofs of equality are equal). Many years before the term “higher inductive type” was even coined, it was known that free algebras can be constructed for (infinitary) varieties, and as observed by Blass, this can even be carried out internally in a topos with a natural numbers object satisfying the internal axiom of choice [5, Section 8]. As observed by Lumsdaine and Shulman in the introduction to [15], this can now be viewed as a kind of higher inductive type. More recently, in [1] Altenkirch, Capriotti, Dijkstra and Forsberg developed a class of higher inductive types, which they call quotient inductive-inductive types which also have interesting structure even within extensional type theory. See also the earlier work on quotient inductive types by Altenkirch and Kaposi in [2].

We will develop an idea for a simple kind of higher inductive type that we will call $W$-type with reductions. Essentially, we identify $\sup(y,\alpha)$ with some of the elements $\alpha(x)$ used to construct it.

Although $W$-types with reductions are relatively simple, we will see that they have an interesting application in homotopical algebra and the semantics of homotopy type theory. A well known construction in homotopical algebra is Garner’s small object argument [11], in which a cofibrantly generated algebraic weak factorisation system (awfs) is constructed, making essential use of transfinite colimits. In an earlier paper [28] the author defined a new generalised definition of cofibrantly generated within a Grothendieck fibration, and showed that to construct a cofibrantly generated awfs in this new sense, it suffices to show that certain pointed endofunctors have initial algebras. We will show that when working over the codomain fibration for a locally cartesian closed category, these initial algebras can be seen as $W$-types with reductions. This will then be used to construct some interesting, previously unknown examples of awfs’s.

$W$-types with reductions may turn out to be special cases of free algebras for varieties and/or QIITs, and just like with those they are non trivial even when working in extensional type theory. Indeed throughout this paper we will be working with locally cartesian closed categories which we think of as models for extensional type theory. However, the relative simplicity of $W$-types with reductions will have some important advantages. We will show how the semantics for dependent $W$-types can be generalised to also give us semantics for $W$-types with reductions. We will then show that $W$-types with reductions can be implemented in any $\Pi W$-pretopos satisfying a weak choice axiom known as $\mathbf{WISC}$ (such categories are sometimes referred to as predicative toposes [30]). An interesting aspect of this is that currently approaches to the semantics of higher inductive types such as the work of Lumsdaine and Shulman in [15] use transfinite colimits for the construction of the underlying objects. On the other hand, there are interesting examples of predicative toposes based on realizability that do not have infinite colimits, that we will see in section 8. The key is that we will construct the types within the internal logic of the predicative topos using $W$-types.

The main focus of this paper is on semantics, in the same spirit as Gambino and Hyland in [9]. We will, however give an intuitive explanation of what $W$-types with reductions look like in the internal logic of a $\Pi W$-pretopos, which will suggest what a syntax for $W$-types with reductions might look like.

1.1 On Internal Languages for Locally Cartesian Closed

Categories

Throughout this paper we will use type theoretic notation for objects in a locally cartesian closed category, and type theory style arguments for some of the proofs. Often, given a map $f\colon X\rightarrow Y$ we will think of it as a family of types indexed by $Y$, written as $X_{y}$ or $X(y)$. This is justified by the well known paper by Seely [26], although strictly speaking, in order to really interpret extensional type theory one needs the later work by Hofmann in [12].

One can also add disjoint coproducts, propositional truncation and effective quotients to the type theory, as long as the locally cartesian closed category possesses the appropriate structure. See e.g. the work of Maietti in [16].

Furthermore, as shown by Moerdijk and Palmgren $W$-types in type theory correspond closely to the categorical definition that we will use here. See [17] for more details.

In [17, Remark 5.9] Moerdijk and Palmgren point out a subtle issue to bear in mind when working with $W$-types. If we are constructing a map from a $W$-type, $W$ to an object $A$, then it is very straightforward to convert an argument by recursion in type theory into a direct argument using the initial algebra property of $W$. However, sometimes in proofs we want to construct a predicate on $W$ by induction. In this case there is not a straightforward way to interpret such arguments in an arbitrary locally cartesian closed category. However, as Moerdijk and Palmgren show in [18], such arguments can be interpreted in the richer structure of a stratified pseudotopos, and that many natural examples of $\Pi W$-pretoposes possess this additional structure. In this paper we will sometimes see such arguments, since they are often the most natural and easy to understand proofs. However, our results do apply to arbitrary locally cartesian categories and we will also include brief explanations of how the proofs can be adapted to work in general.

2 $W$-Types with Reductions

2.1 Definition

We recall from [9] that Gambino and Hyland defined the following notions of polynomial, dependent polynomial endofunctor and dependent $W$-type, which we will generalise. Throughout we assume that we are given a locally cartesian closed and finitely cocomplete category $\mathbb{C}$.

Definition 2.1** (Gambino and Hyland).**

A polynomial is a diagram of the following form.

[TABLE]

A dependent polynomial endofunctor is an endofunctor $\mathbb{C}/Z\rightarrow\mathbb{C}/Z$ of the form $\Sigma_{g}\Pi_{f}h^{\ast}$, where $g$, $f$ and $h$ are as above. We denote this endofunctor as $P_{f,g,h}$.

A dependent $W$-type is an initial object in the category of $P_{f,g,h}$-algebras for some dependent polynomial endofunctor $P_{f,g,h}$.

We now give the new more general definition of polynomial with reductions and pointed polynomial endofunctor with reductions.

Definition 2.2**.**

Suppose we are given maps $f,g,h$ and $r$ as in the following diagram.

[TABLE]

We say the diagram is coherent, or satisfies the coherence condition if $g\circ f\circ k=h\circ k$.

We say that a diagram as in (1) satisfying the coherence condition is a polynomial with reductions.

We refer to the subdiagram consisting of $f$, $g$ and $h$ as the underlying polynomial, and to $R$ and $k$ as the reductions.

Proposition 2.3**.**

Polynomials in the sense of definition 2.1 correspond precisely to polynomials with reductions where $R$ is the initial object in $\mathbb{C}$.

Proof.

We draw attention to the fact that the coherence condition is vacuous when $R$ is initial. Aside from this it is obvious. ∎

Definition 2.4**.**

Suppose we are given a polynomial with reductions as in definition 2.2.

We construct a pointed endofunctor $P_{f,g,h,k}$ as follows.

Note that the coherence conditions gives us the isomorphism (equality, in fact) $\Sigma_{g}\Sigma_{f}\Sigma_{k}\cong\Sigma_{h}\Sigma_{k}$. We construct a map $\Sigma_{h}\Sigma_{k}k^{\ast}f^{\ast}\Pi_{f}h^{\ast}\rightarrow\operatorname{Id}_{\mathbb{C}/Z}$ as follows. Note that we have an evaluation map $f^{\ast}\Pi_{f}\rightarrow\operatorname{Id}_{\mathbb{C}/Z}$ in $\mathbb{C}/X$ (which is just the counit of the adjunction $f^{\ast}\dashv\Pi_{f}$). We also have a map $\Sigma_{k}k^{\ast}\rightarrow\operatorname{Id}_{\mathbb{C}/Z}$ over $X$ given by the counit of the adjunction $\Sigma_{k}\dashv k^{\ast}$ (which recall is just one of the projection maps in the pullback). We have a similar such map for $h$. We put these together in the following composition:

[TABLE]

Again using the counits of $\Sigma$ and pullback adjunctions we get a composition

[TABLE]

Finally, we combine these together to get two maps out of $\Sigma_{h}\Sigma_{k}k^{\ast}f^{\ast}\Pi_{f}h^{\ast}$ in $\mathbb{C}/Z$ and then take the pushout.

[TABLE]

This defines a pointed endofunctor on $\mathbb{C}/Z$ with the point given by the right hand inclusion of the pushout.

We will refer to pointed endofunctors defined in this way as pointed polynomial endofunctors.

We first note that we get in this way a generalisation of Gambino and Hyland’s notion of dependent polynomial endofunctor in the following proposition.

Proposition 2.5**.**

If $R$ is an initial object, then $P_{f,g,h,k}$ is just $P_{f,g,h}+1$, which is a pointed endofunctor with a category of algebras isomorphic to the algebras of the dependent polynomial endofunctor on the underlying polynomial.

Definition 2.6**.**

Let $f,g,h,k$ be a polynomial with reductions. We refer to the initial object of the category of $P_{f,g,h,k}$-algebras (if it exists) as the $W$-type with reductions on $f,g,h,k$.

Proposition 2.7**.**

If $R$ is initial, then the $W$-type with reductions is just the dependent $W$-type on the underlying polynomial.

2.2 A Formulation in the Internal Language of a Category

We will often work in the internal logic of $\mathbb{C}$. In this case it is useful to reformulate the definition in a more intuitive way as follows. We will view $g\colon Y\rightarrow Z$ as a family of types $Y_{z}$ indexed by $z\in Z$, and $f\colon X\rightarrow Y$ as a family of types $X_{z,y}$ indexed by $z\in Z$ and $y\in Y_{z}$. We view $k$ as a family of types $R_{z,y,x}$ for $x\in X_{z,y}$.

We refer to $Y_{z}$ as the constructors over $z\in Z$. For $y\in Y_{z}$, we refer to $X_{z,y}$ as the arity of the constructor $y$. We will refer to the map $h\colon X\rightarrow Z$ as the reindexing map.

Suppose we are given a family $(W_{z})_{z\in Z}$ over $Z$. Now we can reformulate the pointed polynomial endofunctor with reductions at $W$ as the following pushout using type theoretic notation as below.

[TABLE]

Then note that by the universal property of the pushout, $P_{f,g,h,k}$-algebra structures on $W$ correspond precisely to commutative triangles of the form below.

[TABLE]

We can rephrase this as the following.

For each $z\in Z$, each constructor $y\in Y(z)$, and each element $\alpha$ of type $\Pi_{x:X(y)}W(h(x))$, we are given a choice of element $c(y,\alpha)$ of type $W(z)$. 2. 2.

For each $y\in Y_{z}$ and each $x\in X(y)$, if there exists $r\in R(x)$ then the equation $c(y,\alpha)=\alpha(x)$ is true. We refer to such equations as reduction equations or just reductions.

Remark 2.8**.**

Note that the coherence condition ensures that whenever $y\in Y(z)$, $x\in X(y)$ and there exists $r\in R(x)$, we have $h(x)=g(f(x))$ and so $\alpha(x)$ lies in the fibre $W(z)$, the same as $c(y,\alpha)$.

The first part is then the same as an algebra structure over the underlying polynomial endofunctor, and the second part is what we gain by adding reductions.

The $W$-type with reductions is then the object inductively generated by the first condition subject to the equations in the second condition. The way we combine an inductively defined type with equations in this way is an example of a higher inductive type. These play an important role in homotopy type theory (see [29]).

In the above we only talked about $R(x)$ being inhabited, and didn’t need to depend on any particular choice of element from $R(x)$. We justify this with the following proposition.

Proposition 2.9**.**

Every pointed polynomial endofunctor with reductions is isomorphic to one derived from a polynomial with reductions where where $k$ is monic. Moreover, given any polynomial with reductions, we obtain an isomorphic pointed endofunctor by replacing $k$ with the inclusion with its image in $X$.

Proof.

Recall that the image factorisation of $k$ is defined as the (unique up to isomorphism) factorisation of $k$ as a regular epimorphism followed by a monomorphism, as in the diagram below.

[TABLE]

Note that this factorisation always exists since $\mathbb{C}$ is locally cartesian closed and finitely cocomplete and therefore regular.

The epimorphism $R\twoheadrightarrow R^{\prime}$ then gives us an epimorphism $k^{\ast}f^{\ast}\Pi_{f}h^{\ast}\twoheadrightarrow l^{\ast}f^{\ast}\Pi_{f}h^{\ast}$, and so an epimorphism in the top left map below.

[TABLE]

However, now by diagram chasing the outer rectangle is also a pushout, and so $P_{f,g,h,k}\cong P_{f,g,h,l}$. ∎

2.3 Coproducts of Pointed Polynomial Endofunctors with

Reductions

In [9, Section 5], Gambino and Hyland observe that under suitable conditions, the class of dependent polynomial endofunctors over a fixed object $Z$ is closed under coproduct. We will now show the analogous result when reductions are added. Note that since we are now working with pointed endofunctors, the appropriate notion of coproduct is the coproduct in the category of pointed endofunctors, which appears in the category of endofunctors as pushout along the units of the pointed endofunctors.

Proposition 2.10**.**

Suppose that $\mathbb{C}$ is a finitely cocomplete locally cartesian closed category with disjoint coproducts.111It’s useful to note that every such category is extensive, as a corollary of [6, Proposition 2.14]. Then the class of pointed polynomial endofunctors over a fixed object $Z$ is closed under coproduct.

Proof.

Suppose we are given two diagrams as below.

[TABLE]

Similarly to the case for dependent polynomial endofunctors, we combine the two diagrams using coproduct as below.

[TABLE]

Again, by the same argument as for dependent polynomial endofunctors, note that $\Sigma_{[g_{1},g_{2}]}\Pi_{f_{1}+f_{2}}[h_{1},h_{2}]^{\ast}\cong\Sigma_{g_{1}}\Pi_{f_{1}}h_{1}^{\ast}+\Sigma_{g_{2}}\Pi_{f_{2}}h_{2}^{\ast}$ and $\Sigma_{[h_{1},h_{2}]}\Sigma_{k_{1}+k_{2}}(k_{1}+k_{2})^{\ast}(f_{1}+f_{2})^{\ast}\Pi_{f_{1}+f_{2}}[h_{1},h_{2}]^{\ast}\cong\Sigma_{h_{1}}\Sigma_{k_{1}}k_{1}^{\ast}f_{1}^{\ast}\Pi_{f_{1}}h_{1}^{\ast}+\Sigma_{h_{2}}\Sigma_{k_{2}}k_{2}^{\ast}f_{2}^{\ast}\Pi_{f_{2}}h_{2}^{\ast}$. Writing $P_{i}$ for $\Sigma_{g_{i}}\Pi_{f_{i}}h_{i}^{\ast}$ and $Q_{i}$ for $\Sigma_{h_{i}}\Sigma_{k_{i}}k_{i}^{\ast}f_{i}^{\ast}\Pi_{f_{i}}h_{i}^{\ast}$ for $i=1,2$, we deduce that the pointed polynomial endofunctor generated by (3) is $\operatorname{Id}_{\mathbb{C}/Z}\rightarrow S$ in the following pushout.

[TABLE]

However, a quick diagram chase verifies that $\operatorname{Id}_{\mathbb{C}/Z}\rightarrow S$ is the map produced by the following three pushouts.

[TABLE]

We deduce that the dependent pointed polynomial endofunctor produced by (3) (given by $\operatorname{Id}_{\mathbb{C}/Z}\rightarrow S$) is the coproduct of the two diagrams given, as required. ∎

3 Constructing $W$-Types with Reductions in $\Pi W$-Pretoposes

3.1 Review of Small Cover Bases and $\mathbf{WISC}$

The axiom $\mathbf{WISC}$ was independently noticed and studied by various authors.

For example, it was considered by Van den Berg in [30] under the name $\mathbf{AMC}$, as a weakening of the axiom $\mathbf{AMC}$ considered by Moerdijk and Palmgren in [18]. We recall the definition below and make some basic observations that will be used later.

Definition 3.1**.**

Let $\mathbb{C}$ be a category. A map $f\colon B\rightarrow A$ is a cover if the only subobject of $A$ that it factors through is $A$ itself.

Proposition 3.2**.**

If $\mathbb{C}$ is a regular category then a map $f$ is a cover if and only if it is a regular epimorphism.

Definition 3.3**.**

Suppose we are given a square of the form below.

[TABLE]

We say the square is covering if both $p$ and the canonical map $D\rightarrow B\times_{A}C$ are covers.

In the internal logic of the category we can think of a covering square as follows. We think of the map $f\colon B\rightarrow A$ as a family of types indexed by $A$, which we write $(B_{a})_{a\in A}$. We think of the map $p\colon C\rightarrow A$ as a family of types indexed by $A$, $(C_{a})_{a\in A}$, where the requirement that $p$ is a cover says that each $C_{a}$ is inhabited. We then think of the map $g\colon D\rightarrow C$ as a family of types $(D_{a,c})_{a\in A,c\in C_{a}}$. Finally, the requirement that the canonical map $D\rightarrow B\times_{A}C$ is a cover says that for every $a\in A$ and $c\in C_{a}$ we have a surjection $q_{a,c}\colon D_{a,c}\twoheadrightarrow B_{a}$. Hence such a square is sometimes referred to as a set of covers.

Definition 3.4**.**

We say that a square as in (4) is collection if the following holds in the internal logic222Since the statement involves quantifying over a class of objects we need to use stack semantics to phrase it in the internal language. See e.g. the description by Roberts in [23, Section 2] for details.. For all $a\in A$ and for each cover $e\colon E\twoheadrightarrow B_{a}$ there is $c\in C_{a}$ and a map $t\colon D_{c}\rightarrow E$ such that $q_{a,c}=e\circ t$.

Squares that are both covering and collection are sometimes referred to as weakly initial sets of covers or cover bases.

Definition 3.5**.**

Let $\mathbb{C}$ be a regular category. We say that a map $f\colon B\rightarrow A$ admits a cover base if $f$ fits into the right hand side of a square as in (4) that is both covering and collection.

The axiom weakly initial set of covers ($\mathbf{WISC}$) states that any map admits a cover base.

Lemma 3.6**.**

Suppose that we are given a covering collection square as in (4). Then the following holds in the internal language.

For all $a\in A$, we have the following. Suppose we are given a family of types $(X_{b})_{b\in B_{a}}$ such that $X_{b}$ is inhabited for all $b\in B_{a}$. Then there exists $c\in C_{a}$ and an element of the product type $\Pi_{d\in D_{a,c}}X_{q_{a,c}(d)}$.

Proof.

We apply collection to the cover $\Sigma_{b\in B_{a}}X_{b}\twoheadrightarrow B_{a}$ given by projection (which is a cover since each $X_{b}$ is inhabited). ∎

The following lemmas, which will be used later are easy to check, so we omit proofs here.

Lemma 3.7**.**

Suppose that a map $f\colon B\rightarrow A$ admits a weak cover base. Then the same is true for the pullback of $f$ along any map $h\colon A^{\prime}\rightarrow A$.

Moreover, the pullback of the covering and collection square along $h$ is also covering and collection.

Lemma 3.8**.**

Suppose that $\mathbb{C}$ has disjoint coproducts. Suppose that $f_{1}\colon B_{1}\rightarrow A_{1}$ and $f_{2}\colon B_{2}\rightarrow A_{2}$ both admit weak cover bases. Then the same is true for $f_{1}+f_{2}\colon B_{1}+B_{2}\rightarrow A_{1}+A_{2}$.

Moreover, the coproduct of the two covering and collection squares is itself covering and collection.

3.2 Construction of the Initial Algebras

In this section we work towards the construction of initial algebras for dependent pointed polynomial endofunctors with reductions over $\Pi W$-pretoposes. Although there are a number of possible approaches to doing this that already appear in the literature, none seems to be quite adequate for our purposes (this will be discussed further in section 9.2). The main obstacle is that we wish for the construction to hold in categories that do not have infinite colimits, such as realizability toposes. We therefore give a direct construction for $\Pi W$-pretoposes rather than applying an existing result.

3.2.1 Outline of the Construction

We start with a rough illustration of the overall idea, with the motivation for each part of the proof.

For the proof to apply for realizability toposes, the proof should be carried out in the internal logic of the $\Pi W$-pretopos. We can see that some kind of transfinite construction is likely to be necessary, and the only such construction available to us internally is to use $W$-types (and in section 7 we will see that $W$-types really are necessary for the theorem to hold). By the results of Gambino and Hyland in [9] we may use dependent $W$-types. Some form of the axiom of choice may be necessary. $\mathbf{WISC}$ is acceptable, since it holds in many examples of $\Pi W$-pretoposes including realizability toposes, but we will try to avoid anything stronger.

The most naïve approach using $W$-types is as follows. We know from the description of $P_{f,g,h,k}$ algebras before that an algebra structure on $W$ consists of the structure of an algebra over the polynomial endofunctor $P_{f,g,h}$ whose operators satisfy the reduction equations. We might therefore take $W$ to be an initial algebra for $P_{f,g,h}$ and then simply quotient out by the equivalence relation generated by the reduction equations. Note however, that this won’t work. We need in particular an algebra structure on $W/{\sim}$. For the time being we will consider the non dependent case for simplicity. Suppose that we want to define $\sup(\alpha)$ for $\alpha\colon X_{y}\rightarrow W/{\sim}$ (the solid horizontal line below). We want to use the algebra structure on $W$ to define $\sup(\alpha)$, but to do this, we need a map $X_{y}\rightarrow W$ (the dotted line below).

[TABLE]

In order for any such map to exist, we need the axiom of choice, and then once we’ve found such a map we need to ensure that the particular choice of map doesn’t matter in order to produce a well defined algebra structure.

Note however, that if $(A_{i},q_{i})_{i\in I}$ is a cover base for $(X_{y})_{y\in Y_{z},z\in Z}$, then there does exist a dotted line in the diagram below for some $i\in I$.

[TABLE]

We therefore modify the naïve argument as follows. We first form a dependent $W$ type, using as arities, not $(X_{y})_{y\in Y_{z}}$ directly, but instead $(A_{i})_{i\in I}$ where $(A_{i},q_{i})_{i\in I}$ is a cover base for $(X_{y})_{y\in Y_{z}}$.

We then define an equivalence relation $\sim$ on $W$ as (the image of) another dependent $W$-type. We need to ensure of all of the following:

The reduction equations are satisfied. 2. 2.

If $\alpha(q_{i}(a))\sim\alpha^{\prime}(q_{i^{\prime}}(a^{\prime}))$ whenever $q_{i}(a)=q_{i^{\prime}}(a^{\prime})$ then also $\sup(\alpha)\sim\sup(\alpha^{\prime})$ (function extensionality). 3. 3.

$\sim$ is an equivalence relation, in particular symmetric and transitive.

Using a cover base like this has solved one problem but introduced another. In order to show that the algebra structure is initial, we will need that any $\alpha\colon A_{i}\rightarrow W/{\sim}$ extends to $X_{y}$ as below, but this is not always the case.

[TABLE]

In fact the dotted line exists if and only if $\alpha(q_{i}(a))\sim\alpha(q_{i^{\prime}}(a^{\prime}))$ whenever $q_{i}(a)=q_{i^{\prime}}(a^{\prime})$. To deal with this point we define $\sim$ not to be an equivalence relation, but instead a partial equivalence relation. We then ensure that whenever $\sup(\alpha)\sim\sup(\alpha)$ the condition above is satisfied (we will refer to such elements as well defined). Then we can restrict to $w\in W$ such that $w\sim w$ in our construction.

A final point is that we know the dotted map in (5) exists, but now we also have to show it is well defined. We will define $\sim$ as the image of a certain $W$-type, and well definedness will amount to the existence of a function which provides for each $a\in A_{i}$ and $a^{\prime}\in A_{i^{\prime}}$ such that $q_{i}(a)=q_{i^{\prime}}(a^{\prime})$, a witness of $\alpha(a)\sim\alpha(a^{\prime})$. We have effective quotients and ensured that $\sim$ is an equivalence relation, but this only tells us that such a witness exists for each $a$, not how to find one. To deal with this, we use another cover base, this time for $A_{i}\times_{X_{y}}A_{i^{\prime}}$ over all $y\in Y_{z}$. We then can use the same trick again of using the cover base in our dependent $W$-type instead of $A_{i}\times_{X_{y}}A_{i^{\prime}}$ itself.

We now provide a more careful, detailed version of the above argument.

3.2.2 $2$-Cover Bases

At the end of the outline we indicated that we would need two levels of cover base. We formalise this using the following notion.

Definition 3.9**.**

Let $u\colon U\rightarrow I$ be a morphism in $\mathbb{C}$. A $2$-cover base for $u$ consists of two squares of the following form that are both covering and collection.

[TABLE]

[TABLE]

Note in particular that if $\mathbf{WISC}$ holds in the pretopos, then any map has a 2-cover base by applying $\mathbf{WISC}$ twice. Also if $X$ is the surjective image of a projective object then $g\circ f$ has a 2-cover base, which in particular includes all finite colimits of representables in presheaf categories.

We also prove below that maps that admit $2$-cover bases are closed under pullback and coproduct.

Lemma 3.10**.**

Suppose that a map $f\colon X\rightarrow Y$ admits a $2$-cover base. Then the same is true for the pullback of $f$ along any map $Y^{\prime}\rightarrow Y$.

Proof.

By applying lemma 3.7 twice. ∎

Lemma 3.11**.**

Suppose that $\mathbb{C}$ has disjoint coproducts. Suppose further that $f_{1}\colon X_{1}\rightarrow Y_{1}$ and $f_{2}\colon X_{2}\rightarrow Y_{2}$ admit $2$-cover bases. Then the same is true for $f_{1}+f_{2}\colon X_{1}+X_{2}\rightarrow Y_{1}+Y_{2}$.

Proof.

By applying lemma 3.8 twice. ∎

3.2.3 The Underlying Object of the Initial Algebra

We assume we are given a polynomial with reductions as in (1), which as in section 2.2, we view as families of types $Y_{z}$, $X_{z,y}$ and $R_{z,y,x}$ (which we’ll sometimes abbreviate to $X_{y}$ and $R_{x}$).

We will assume that $f$ has a 2-cover base and view it as families of types as follows. We assume we have a type $I_{z,y}$ for each $z\in Z$ and $y\in Y_{z}$ together with a type $A_{z,y,i}$ (which we will usually write just as $A_{i}$) and surjections $q_{i}\colon A_{i}\twoheadrightarrow X_{y}$ such that $(A_{i},q_{i})_{i\in I}$ form a cover base for $X_{y}$.

For the second part of the 2-cover base, we say that for each $y$ and $z$ we have a type $J_{i,i^{\prime}}$ for each $i,i^{\prime}\in I_{z,y}$ and a family of types and surjections $t_{j}\colon B_{j}\twoheadrightarrow A_{i}\times A_{i^{\prime}}$ for $j\in J_{i,i^{\prime}}$, forming a cover base for $A_{i}\times_{X_{y}}A_{i^{\prime}}$.

We will now construct the initial algebra.

We first define a family of types $W_{z}$ for $z\in Z$ as the dependent $W$-type generated by the following rule:

If $y\in Y_{z}$, $i\in I_{z,y}$ and $\alpha\in\Pi_{a\in A_{i}}W_{h(q_{i}(a))}$ then $\mathtt{cons}(y,i,\alpha)$ is a new element of $W_{z}$.

We now form a second dependent $W$-type, $Q$, which will be indexed over $W\times_{Z}W$. First note that by the definition of $W$ and the basic properties of dependent $W$-types, for every $w\in W_{z}$ there is unique $y\in Y_{z}$, $i\in I_{z,y}$ and $\alpha\in\Pi_{a\in A_{i}}W_{h(q_{i}(a))}$ such that $w=\mathtt{cons}(y,i,\alpha)$. We will sometimes write $Q_{w_{0},w_{1}}$ as $Q(w_{0},w_{1})$ to ease readability.

If $w^{\prime}\in W_{z}$, $q_{1}\in Q_{w_{0},w^{\prime}}$ and $q_{2}\in Q_{w^{\prime},w_{1}}$, then $Q_{w_{0},w_{1}}$ has an element of the form $\mathtt{trans}(q_{1},q_{2})$. 2. 2.

If $y$, $i$ and $\alpha$ are such that $w_{0}=\mathtt{cons}(y,i,\alpha)$ and we are given $x\in X_{z,y}$ such that $\alpha(x)=w_{1}$, $r\in R_{z,y,x}$, $j\in J_{i,i}$, and $\gamma\colon\Pi_{b\in B_{j}}Q(\alpha(\pi_{0}(t_{j}(b))),\alpha(\pi_{1}(t_{j}(b))))$, then $Q_{w_{0},w_{1}}$ has an element of the form $\mathtt{reduceleft}(r,j,\alpha,\gamma)$. 3. 3.

If $y$, $i$ and $\alpha$ are such that $w_{1}=\mathtt{cons}(y,i,\alpha)$ and we are given $x\in X_{z,y}$ such that $\alpha(x)=w_{0}$, $r\in R_{z,y,x}$, $j\in J_{i,i}$, and $\gamma\colon\Pi_{b\in B_{j}}Q(\alpha(\pi_{0}(t_{j}(b))),\alpha(\pi_{1}(t_{j}(b))))$, then $Q_{w_{0},w_{1}}$ has an element of the form $\mathtt{reduceright}(r,j,\alpha,\gamma)$. 4. 4.

If we are given $y\in Y_{z}$, $i_{0},i_{1}\in I_{y}$, $j\in J_{i_{0},i_{1}}$, $\alpha_{0}\in\Pi_{a\in A_{i_{0}}}W_{h(q_{i_{0}}(a))}$, $\alpha_{1}\in\Pi_{a\in A_{i_{1}}}W_{h(q_{i_{1}}(a))}$ are such that $w_{0}=\mathtt{cons}(y,i_{0},\alpha_{0})$ and $w_{1}=\mathtt{cons}(y,i_{1},\alpha_{1})$ and $\gamma\in\Pi_{b\in B_{j}}Q(\alpha_{0}(\pi_{0}(t_{j}(b))),\alpha_{1}(\pi_{1}(t_{j}(b))))$, then $Q_{w_{0},w_{1}}$ has an element of the form $\mathtt{extn}(\alpha_{0},\alpha_{1},\gamma)$.

We now define $Q_{z}:=\Sigma_{w_{0}\in W_{z}}\Sigma_{w_{1}\in W_{z}}Q_{w_{0},w_{1}}$ and define $l,r\colon Q_{z}\rightarrow W_{z}$ to be the two projections.

Note that we have defined $Q_{z}$ so that its image in $W_{z}\times W_{z}$, which we write as $\sim$, is a partial equivalence relation. For transitivity we use $\mathtt{trans}$. We prove symmetry in the following lemma.

Lemma 3.12**.**

The relation $\sim$ on $W_{z}$ is symmetric.

Proof.

We show by induction on the construction of $Q$ that given any element $q$ of $Q_{w_{0},w_{1}}$ we can prove there exists an element of $Q_{w_{1},w_{0}}$. Formally, we need to be a little careful to make this argument work in general $\Pi W$-pretoposes. Write $\tau\colon W\times_{Z}W\rightarrow W\times_{Z}W$ for the map swapping the two components. Then we need to define a map from $Q$ to $\tau^{\ast}(\sim)$, regarded as objects in $\mathbb{C}/(W\times_{Z}W)$. We do this by defining an algebra structure on $\tau^{\ast}(\sim)$ and then using the initial map. The proof below is presented as an argument by induction on the structure of $Q_{w_{0},w_{1}}$ because it’s more intuitive, but it’s easy to adapt to the form above.

Note that the definitions of $\mathtt{reduceleft}$ and $\mathtt{reduceright}$ were chosen so that they can just be swapped round, and $\mathtt{trans}$ is easy to deal with by induction.

This only leaves us with the case of $\mathtt{extn}$, which is a little non trivial. Suppose we are given an element of $Q_{w_{0},w_{1}}$ of the form $\mathtt{extn}(\alpha_{0},\alpha_{1},\gamma)$. Suppose further that we are given some $(a^{\prime},a)\in A_{i^{\prime}}\times_{X_{y}}A_{i}$. Then note that we also have $(a,a^{\prime})\in A_{i}\times_{X_{y}}A_{i^{\prime}}$.

Since $t_{j}\colon B_{j}\twoheadrightarrow A_{i}\times_{X_{z}}A_{i^{\prime}}$ is a surjection, there exists some $b\in B_{j}$ such that $t_{j}(b)=(a,a^{\prime})$ and we have that $\gamma(b)\in\Pi_{b\in B_{j}}Q(\alpha_{0}(\pi_{0}(t_{j}(b))),\alpha_{1}(\pi_{1}(t_{j}(b))))$. By induction, we may assume therefore that $Q(\alpha_{1}(\pi_{1}(t_{j}(b))),\alpha_{0}(\pi_{0}(t_{j}(b))))$ contains some element $q^{\prime}$. Then using the fact that $(B_{i^{\prime},i,j})_{j\in J_{i^{\prime},i}}$ is a cover base, we deduce that there exists $j\in J_{i^{\prime},i}$ together with $\gamma^{\prime}\colon B_{i^{\prime},i^{\prime},j}\rightarrow Q^{\prime}$ choosing witnesses of this. We then form the element of $Q_{w_{1},w_{0}}$, $\mathtt{extn}(\alpha_{1},\alpha_{0},\gamma^{\prime})$ and note that it is as required. ∎

We say that $w\in W$ is well defined if $w\sim w$. We write $W^{\prime}$ for the set of well defined elements of $Z$. Note that $\sim$ restricts to an equivalence relation on $W^{\prime}$ (as is always the case for partial equivalence relations). Note that we can use $\mathtt{extn}$ to produce well defined elements as follows.

Lemma 3.13**.**

Suppose that $w,w^{\prime}\in W$ are of the form $\mathtt{cons}(y,i,\alpha)$ and $\mathtt{cons}(y,i^{\prime},\alpha^{\prime})$ respectively. Suppose further that for every $(a,a^{\prime})\in A_{i}\times_{X_{y}}A_{i^{\prime}}$ we have that $\alpha(a)\sim\alpha^{\prime}(a^{\prime})$. Then $w\sim w^{\prime}$.

Proof.

Suppose that for every $(a,a^{\prime})\in A_{i}\times_{X_{y}}A_{i^{\prime}}$ we have that $\alpha(a)\sim\alpha^{\prime}(a^{\prime})$. Then using the fact that $(B_{i,i^{\prime},j})_{j\in J_{i,i^{\prime}}}$ is a cover base for $A_{i}\times_{X_{y}}A_{i^{\prime}}$, there exists $j\in J_{i,i^{\prime}}$ and a choice function $\gamma\in\Pi_{b\in B_{j}}Q(\alpha(\pi_{0}(t_{j}(b))),\alpha^{\prime}(\pi_{1}(t_{j}(b))))$. We then have $\mathtt{extn}(\alpha,\alpha^{\prime},\gamma)\in Q(\mathtt{cons}(y,i,\alpha),\mathtt{cons}(y,i^{\prime},\alpha^{\prime})$ and so $w\sim w^{\prime}$. ∎

Lemma 3.14**.**

Suppose $w\in W$ is of the form $\mathtt{cons}(y,i,\alpha)$ and for every $(a,a^{\prime})\in A_{i}\times_{X_{y}}A_{i}$ we have that $\alpha(a)\sim\alpha(a^{\prime})$. Then $w\sim w$.

Proof.

This is a special case of the previous lemma where $\alpha=\alpha^{\prime}$ and $i=i^{\prime}$. ∎

3.2.4 The Algebra Structure of the Initial Algebra

We now give $W^{\prime}/{\sim}$ an algebra structure over the pointed endofunctor. We first show the following lemma.

Lemma 3.15**.**

Suppose that we are given a map $\alpha_{0}\in\Pi_{x\in X_{y}}W_{h(x)}^{\prime}/{\sim}$. Then there exists $i\in I$ and $\alpha\in\Pi_{a\in A_{i}}W^{\prime}$ such that for all $a\in A_{i}$ we have $[\alpha(a)]=\alpha_{0}(q_{i}(a))$.

Furthermore, if $(i,\alpha)$ and $(i^{\prime},\alpha^{\prime})$ are two such pairs then $\mathtt{cons}(i,\alpha)\sim\mathtt{cons}(i^{\prime},\alpha^{\prime})$ (and in particular these are well defined).

Proof.

First we construct $\alpha$ by applying lemma 3.6.

Now suppose that $(i,\alpha)$ and $(i^{\prime},\alpha^{\prime})$ are two such pairs. By lemma 3.13 it suffices to show that $\alpha(a)\sim\alpha^{\prime}(a^{\prime})$ for every $(a,a^{\prime})\in A_{i}\times_{X_{y}}A_{i^{\prime}}$. However, we know that $[\alpha(a)]=\alpha_{0}(q_{i}(a))$ and $[\alpha^{\prime}(a^{\prime})]=\alpha_{0}(q_{i^{\prime}}(a^{\prime}))$. Since $(a,a^{\prime})$ belongs to the pullback over $X_{y}$, we have $q_{i}(a)=q_{i^{\prime}}(a^{\prime})$, and so $[\alpha(a)]=[\alpha^{\prime}(a^{\prime})]$. Finally, since quotients are effective, we deduce $\alpha(a)\sim\alpha^{\prime}(a^{\prime})$. ∎

Lemma 3.16**.**

We exhibit an algebra structure on $W^{\prime}/{\sim}$ over the pointed endofunctor.

Proof.

By the characterisation of algebra structures in section 2.2, it suffices to construct $\sup(\alpha_{0})$ for every $\alpha_{0}\in\Pi_{x\in X_{y}}W_{h(x)}^{\prime}/{\sim}$ and show that it respects the reduction equations.

Given $\alpha_{0}\in\Pi_{x\in X_{y}}W_{h(x)}^{\prime}/{\sim}$, we define $\sup(\alpha_{0})$ to be $[\mathtt{cons}(i,\alpha)]$ where $(i,\alpha)$ is such that $[\alpha(a)]=\alpha_{0}(q_{i}(a))$ for every $a\in A_{i}$. This determines a unique element of $W_{z}/{\sim}$ by lemma 3.13.

We now need to show that, for all $x\in X$, if $R_{z,y,x}$ is inhabited, then $\sup(\alpha_{0})=\alpha_{0}(x)$. To do this, we will show there exists an appropriate element of $Q$ using $\mathtt{reduceleft}$. Firstly, let $i$ and $\alpha$ be as above. Let $a\in A_{i}$ be such that $q_{i}(a)=x$. Next, note that following the proof of lemma 3.13 we can show there exists $j\in J_{i,i}$ and $\gamma\colon B_{j}\rightarrow Q^{\prime}$ such that for all $b\in B_{j}$, $\gamma(b)\in Q(\alpha(\pi_{0}(t_{j}(b))),\alpha(\pi_{1}(t_{j}(b))))$. Then, $\mathtt{reduceleft}(a,j,\alpha,\gamma)$ witnesses $\mathtt{cons}(i,\alpha)\sim\alpha(a)$ and so $\sup(\alpha_{0})=[\mathtt{cons}(i,\alpha)]=[\alpha(a)]=\alpha_{0}(x)$ as required. ∎

3.2.5 Proof of Initiality

We now show that the algebra structure we defined is initial. Suppose that we are given an object $T$ together with an algebra structure on $T$. We will use the presentation from section 2.2, where we view an algebra structure as an algebra structure for the underlying polynomial, $c\colon\Sigma_{g}\Pi_{f}h^{\ast}(T)\rightarrow T$ such that $c$ respects the reduction equations.

We first need to construct algebra map from $W^{\prime}/{\sim}$ to $T$, and then show that it is unique.

For this, we will follow the basic outline below.

Define a relation $S\rightarrowtail W\times_{Z}T$ by induction on the construction of $W$. 2. 2.

Show by induction on the construction of $Q$ that for every $q\in Q_{w_{0},w_{1}}$ there exists a unique $t\in T$ such that $\langle w_{0},t\rangle\in S$ and the same $t$ is unique such that $\langle w_{1},t\rangle\in S$ (which in particular tells us that when $w\sim w$ there exists a unique $t\in T$ such that $\langle w_{0},t\rangle\in S$). 3. 3.

Deduce (using effectiveness of quotients) that the corresponding relation on $W^{\prime}/{\sim}\times_{Z}T$ is functional, and so gives a morphism $W^{\prime}/{\sim}\rightarrow T$ over $Z$.

We define $S\rightarrowtail W\times_{Z}T$ inductively as follows.

We add $\langle\mathtt{cons}(i,\alpha),x\rangle$ to $S$ when $\alpha^{\prime}\in\Pi_{x\in X_{z}}T_{h(x)}$ is such that for every $a\in A_{i}$, $\alpha^{\prime}(q(a))$ is the unique $t$ such that $\langle\alpha(a),t\rangle\in S$ and $x$ is the result of applying the algebra structure of $T$ to $\alpha^{\prime}$.

Formally, we can construct $S$ in an arbitrary $\Pi W$-pretopos as a dependent $W$-type as follows. We work over the context $W\times_{Z}T$.

Let $\langle w,t\rangle\in W\times_{Z}T$. We construct $S(w,t)$ as follows. Suppose we are given all of the following.

A triple $y,i,\alpha$ such that $w=\sup(y,i,\alpha)$ 2. 2.

A dependent function $\alpha^{\prime}\colon\Pi_{x:X(z)}T(h(x))$ such that $t=c(\alpha^{\prime})$ (recall that $c$ is the algebra structure for $T$). 3. 3.

A dependent function $\beta\colon\Pi_{a:A_{i}}S(\alpha(a),\alpha^{\prime}(q(a)))$

Then we construct a new element of $S$ of the form $\sup(\alpha^{\prime},\beta)$.

One can check that the composition $S\rightarrow W\times_{Z}T\rightarrow W$ is monic, it follows that this definition of $S$ matches the other definition.

We can now state and prove the main lemma.

Lemma 3.17**.**

Let $T$ and $S$ be as above. Then for any $e\in Q_{w_{0},w_{1}}$, there exists a unique $t$ such that $\langle w_{0},t\rangle\in S$ and the same $t$ is unique such that $\langle w_{1},t\rangle\in S$.

Proof.

We prove this by induction on the construction of $e\in Q_{w_{0},w_{1}}$.

The case $\mathtt{trans}$ is easy to deal with by induction.

We next consider $\mathtt{extn}$. Suppose that $w_{0}=\mathtt{cons}(y,i_{0},\alpha_{0})$, $w_{1}=\mathtt{cons}(y,i_{1},\alpha_{1})$ and $e$ is of the form $\mathtt{extn}(\alpha_{0},\alpha_{1},\gamma)$. Note that we may assume by induction that for every $b\in B_{j}$, $\gamma(b)$ satisfies the statement of the lemma. We define an element $\tilde{\alpha}$ of $\Pi_{x\in X_{z}}T_{h(x)}$ as follows. Given $x\in X_{z}$, let $a$ be such that $q_{i_{0}}(a)=x$ (which exists since $q_{i_{0}}$ is surjective). Furthermore, let $a^{\prime}$ be such that $q_{i_{1}}(a^{\prime})=x$. Then clearly $(a,a^{\prime})\in A_{i_{0}}\times_{X}A_{i_{1}}$. Let $b$ be such that $t_{j}(b)=(a,a^{\prime})$. Then $\gamma(b)\in Q(\alpha_{0}(\pi_{0}(a)),\alpha_{1}(\pi_{1}(a^{\prime})))$, so in particular there is a unique $t\in T_{h(x)}$ such that $\langle\alpha(a),t\rangle\in S$. We will take $\tilde{\alpha}(x)$ to be such a $t$, but we still need to complete the proof that $t$ is uniquely determined by $x$. It only remains to check that $t$ is independent of the choice of $a\in q_{i}^{-1}(x)$. So let $a^{\prime\prime}\in q_{i}^{-1}(x)$ and let $t^{\prime\prime}$ be unique such that $\langle\alpha(a^{\prime\prime}),t^{\prime\prime}\rangle\in S$. We need to check that $t=t^{\prime\prime}$. Suppose that $a^{\prime}\in q_{i^{\prime}}^{-1}(x)$, as before, and note that we have $b,b^{\prime}\in B_{j}$ such that $\gamma(b)\in Q(\alpha(a),\alpha^{\prime}(a^{\prime}))$ and $\gamma(b^{\prime})\in Q(\alpha(a^{\prime\prime}),\alpha^{\prime}(a^{\prime}))$. Using the inductive hypothesis, we have then a unique $t^{\prime}$ such that $\langle\alpha^{\prime}(a^{\prime}),t^{\prime}\rangle\in S$ and $t=t^{\prime}$ and $t^{\prime\prime}=t^{\prime}$, which implies $t=t^{\prime\prime}$, as required. Finally, note that the $\tilde{\alpha}$ we have now defined is unique such that for all $a\in A_{i}$, $\langle\alpha(a),\tilde{\alpha}(q_{i}(a))\rangle\in S$. By the same argument as above, $\tilde{\alpha}$ is also unique such that for all $a\in A_{i^{\prime}}$, $\langle\alpha^{\prime}(a),\tilde{\alpha}(q_{i^{\prime}}(a))\rangle\in S$. Therefore, applying the algebra structure of $T$ to $\tilde{\alpha}$ gives us a unique $t$ such that $\langle w_{0},t\rangle\in S$ and the same $t$ is unique such that $\langle w_{1},t\rangle\in S$ as required.

The last two cases to consider are $\mathtt{reduceleft}$ and $\mathtt{reduceright}$. We will just consider when $e$ is of the form $\mathtt{reduceleft}(a_{0},j,\alpha,\gamma)$, the other case being similar.

First note that by induction we may assume that for every $b\in B_{j}$, $\gamma(b)$ satisfies the statement of the lemma. Hence, we may apply the same argument as before to construct a unique $\alpha_{0}\in\Pi_{x\in X}T_{h(x)}$ such that for all $a\in A_{i}$, $\langle\alpha(a),\alpha_{0}(q_{i}(a))\rangle\in S$.333In fact, this is the sole reason for including $\gamma$ in the definition of $\mathtt{reduceleft}$. We now have, as before that applying the algebra structure of $T$ to $\alpha_{0}$ gives us a unique $t$ such that $\langle\mathtt{cons}(i,\alpha),t\rangle\in S$.

Also, note that there exists $b\in B_{j}$ such that $q_{j}(b)=(a_{0},a_{0})$, and so again by induction, there is a unique $t^{\prime}$ such that $\langle\alpha(a_{0}),t^{\prime}\rangle\in S$.

Finally, since the algebra structure on $T$ has to respect the reduction equations, we have $t=t^{\prime}$, as required. ∎

Finally, since $W^{\prime}$ includes only the well defined elements of $W$, we deduce that for every $w\in W^{\prime}$, there is a unique $t\in T$ such that $\langle w,t\rangle\in S$, and if $w\sim w^{\prime}$ and $t^{\prime}$ is unique such that $\langle w^{\prime},t^{\prime}\rangle\in S$ then $t=t^{\prime}$. We deduce that this gives us a well defined function $W^{\prime}/{\sim}\rightarrow T$. Finally note that by the definition of $S$ and the algebra structure on $W^{\prime}/{\sim}$, we can easily see that the function is the unique algebra structure preserving map, which gives us the lemma below.

Lemma 3.18**.**

$W^{\prime}/{\sim}$* with the algebra structure given in lemma 3.16 is initial.*

We can now deduce the main theorem of this section.

Theorem 3.19**.**

Let $\mathbb{C}$ be a $\Pi W$-pretopos.

Suppose we are given a polynomial with reductions in $\mathbb{C}$ together with a $2$-covering for it. Then we can construct an initial algebra for the corresponding pointed polynomial endofunctor. 2. 2.

Suppose that $\mathbf{WISC}$ holds in $\mathbb{C}$, making it a predicative topos. Then every pointed polynomial endofunctor admits an initial algebra. In other words, $\mathbb{C}$ has all $W$-types with reductions.

4 A Simplification in Categories of Presheaves

In section 3 we gave a very general construction that works for any polynomial with reductions in any predicative topos. However, the result is in some ways unsatisfactory. Since we relied on effective quotients, the result does not apply to presheaf assemblies, which are one of the main intended applications of this work. The reliance on cover bases and $\mathbf{WISC}$ may turn out to be less serious in practice, but is still not ideal. It could, for example lead to subtle coherence issues when applying the results to the semantics of type theory.

In this section we therefore give another version of the main result, which will appear as theorem 4.16. We no longer assume effective quotients or $\mathbf{WISC}$, so the result is applicable to a wider range of categories, and we obtain more concrete descriptions of the initial algebras. The class of polynomials with reductions that we consider is, however, much more restricted, but will still include many interesting examples.

Recall, e.g. from [13, Chapter 7] that in any finitely complete category we can define the notion of internal category, and thereby a notion of category of internal diagrams (which we will refer to here as internal presheaves).

Let $\mathbb{C}$ be a finitely cocomplete locally cartesian closed category with disjoint coproducts and $W$-types (e.g. a category of assemblies). Note that for any internal category $\mathcal{C}$ in $\mathbb{C}$, the category of internal assemblies is also finitely cocomplete locally cartesian closed, and has disjoint coproducts. We will construct initial algebras for a certain class of polynomials with reductions in such internal presheaf categories.

4.1 Dependent $W$-Types in Internal Presheaves

We first give an explicit description of dependent $W$-types in presheaves. We will consider polynomial endofunctors over the following polynomial in internal presheaves. Note that by forgetting the action, we can also view this as a polynomial in $\mathbb{C}/\mathcal{C}_{0}$

[TABLE]

Suppose we are given a morphism of presheaves $A\rightarrow Z$. Then, using (the internal version of) Yoneda and the adjunctions $f^{\ast}\dashv\Pi_{f}$ and $\Sigma_{h}\dashv h^{\ast}$ we can show that for $c\in\mathcal{C}_{0}$ elements of $\Pi_{f}h^{\ast}(A)(c)$ consist of $y\in Y(c)$ (which we view as a map $\ulcorner y\urcorner\colon\mathbf{y}(c)\rightarrow Y$) together with with a map $f^{\ast}(\mathbf{y}(c))\rightarrow A$ making the following square commute.

[TABLE]

Expanding the definition of $\mathbf{y}(c)$, we see that this consists of a (dependent) function assigning, for each $d\in\mathcal{C}_{0}$, each $\sigma\colon c\rightarrow d$ in $\mathcal{C}_{1}$, and each $x\in f_{d}^{-1}(Y(\sigma)(y))$, an element, $\alpha(\sigma,x)$ of $A(d,h_{d}(Y(\sigma)(y)))$, satisfying the naturality condition that for all $\tau\colon d\rightarrow d^{\prime}$ we have $\alpha(\tau\circ\sigma,X(\tau)(x))=A(\tau)(\alpha(\sigma,x))$. Note that if we drop the naturality condition, then we get a dependent polynomial functor in $\mathbb{C}$. We denote the corresponding dependent $W$-type as $W_{0}$. We define the action of morphisms making $W_{0}$ into a presheaf over $Z$ as follows. For $c\in\mathcal{C}_{0}$ and $z\in Z(c)$, everything in $W_{0}(c,z)$ is of the form $\sup(y,\alpha)$ where $y$ and $\alpha$ are as above. Given $\tau\colon c\rightarrow c^{\prime}$, we define $W_{0}(\tau)(\sup(y,\alpha))$ to be $\sup(Y(\tau)(y),\alpha^{\prime})$ where $\alpha^{\prime}(\sigma,x)$ is defined to be $\alpha(\sigma\circ\tau,x)$. Following Moerdijk and Palmgren in [17, Paragraph 5.4] we note that if we can form the subobject of $W_{0}$ consisting of the corresponding dependent $W$-type consisting of hereditarily natural444In [17] Moerdijk and Palmgren refer to another condition in addition to naturality that they call composability. We have already dealt with this by using exploiting the fact that we are using dependent $W$-types rather than ordinary $W$-types. elements, then this gives the $W$-type in presheaves. We can construct this subobject in an arbitrary locally cartesian closed category with $W$-types by a similar technique to the construction of dependent $W$-types from ordinary $W$-types, which we do in the following lemma.

Lemma 4.1**.**

$W_{0}$* has a subobject $W$ such that an element $\sup(y,\alpha)$ of $W_{0}$ belongs to $W$ if and only if $\alpha$ is natural, and for every $\sigma\colon c\rightarrow d$ and $x\in Y(\sigma)(y)$, we have $\alpha(\sigma,x)\in W$.*

Proof.

We first modify the definition of $W_{0}$ to get a dependent $W$-type, $V$ defined as follows. We take the context and the constructors to be the same as for $W_{0}$. For $W_{0}$, the arity at $Y\in Y(c,z)$ consisted of pairs $(\sigma,x)$ where $\sigma\colon c\rightarrow d$ and $x\in X(d,Y(\sigma)(y))$. For $V$, we instead define an element of the arity over $y$ to consist of two morphisms $\sigma\colon c\rightarrow d$ and $\tau\colon d\rightarrow e$ in $\mathcal{C}$, together with $x\in X(d,Y(\sigma)(y))$. We define the reindexing map at $(\sigma,\tau,x)$ to be $Z(\tau\circ\sigma)(z)$. In other words we add an element to $V(c,z)$ of the form $\sup(y,\alpha)$ whenever $y\in Y(c,z)$, and $\alpha$ is a dependent function such that for $\sigma\colon c\rightarrow d$, $\tau\colon d\rightarrow e$ and $x\in X(d,Y(\sigma)(y))$, $\alpha(\sigma,\tau,x)$ is an element of $V(e,Z(\tau\circ\sigma)(z))$.

Note that we have two maps $r,s\colon W_{0}\rightarrow V$ over $Z$ defined recursively as follows. Suppose we are given an element of $W_{0}$ of the form $\sup(y,\alpha)$. We define $r(\sup(y,\alpha))$ to be $\sup(y,\alpha^{\prime})$ and $s(\sup(y,\alpha))$ to be $\sup(y,\alpha^{\prime\prime})$, where $\alpha^{\prime}$ and $\alpha^{\prime\prime}$ are defined as follows. Let $\sigma\colon c\rightarrow d$, $\tau\colon d\rightarrow e$ and $x\in X(d,Y(\sigma)(y))$. We define $\alpha^{\prime}(\sigma,\tau,x)$ to be $r(\alpha(\tau\circ\sigma,X(\tau)(x)))$. We define $\alpha^{\prime\prime}(\sigma,\tau,x)$ to be $s(W_{0}(\tau)(\alpha(\sigma,x)))$.

We define $W$ to be the equaliser of $r$ and $s$.

Note that $r$ and $s$ have a common retract $t\colon V\rightarrow W_{0}$ defined recursively as follows. Given an element of $V$ of the form $\sup(y,\alpha)$, we define $t(\sup(y,\alpha))$ to be $\sup(y,\alpha^{\prime})$ where $\alpha^{\prime}$ is defined as follows. Given $\sigma\colon c\rightarrow d$ and $x\in X(d,Y(\sigma)(y))$, we define $\alpha^{\prime}(\sigma,x):=t(\alpha(\sigma,1_{d},x))$.

We now need to check that $W$ does in fact satisfy the lemma.

Every element of $W_{0}$ is of the form $\sup(y,\alpha)$. First suppose that $\sup(y,\alpha)\in W$. Then $\alpha^{\prime}=\alpha^{\prime\prime}$, where $\alpha^{\prime}$ and $\alpha^{\prime\prime}$ are as above. Hence for all $\sigma\colon c\rightarrow d$, $\tau\colon d\rightarrow e$ and $x\in X(d,Y(\sigma)(y))$ we have $r(\alpha(\tau\circ\sigma,X(\tau)(x)))=s(W_{0}(\tau)(\alpha(\sigma,x)))$. Applying the common retract $t$ of $r$ and $s$ to this equation allows us to deduce $\alpha(\tau\circ\sigma,X(\tau)(x))=W_{0}(\tau)(\alpha(\sigma,x))$ for all $\sigma,\tau,x$, and so that $\alpha$ is natural. Applying the equation to the special case $\tau=1_{d}$, allows to deduce $r(\alpha(\sigma,x))=s(\alpha(\sigma,x))$ and so $\alpha(\sigma,x)\in W$ for all $\sigma$ and $x$.

Conversely, suppose that $\alpha$ is natural and $\alpha(\sigma,x)\in W$ for all $\sigma$ and $x$. We need to show that $\alpha^{\prime}=\alpha^{\prime\prime}$ where $\alpha^{\prime}$ and $\alpha^{\prime\prime}$ are as above. Naturality tells us that for all $\sigma\colon c\rightarrow d$, $\tau\colon d\rightarrow e$ and $x\in X(d,Y(\sigma)(y))$ we have $\alpha(\tau\circ\sigma,X(\tau)(x))=W_{0}(\tau)(\alpha(\sigma,x))$, and so applying $s$ we have $s(\alpha(\tau\circ\sigma,X(\tau)(x)))=s(W_{0}(\tau)(\alpha(\sigma,x)))$. However, we also have $\alpha(\tau\circ\sigma,X(\tau)(x))\in W$ and so $s(\alpha(\tau\circ\sigma,X(\tau)(x)))=r(\alpha(\tau\circ\sigma,X(\tau)(x)))$. Putting these together we have $r(\alpha(\tau\circ\sigma,X(\tau)(x)))=s(W_{0}(\tau)(\alpha(\sigma,x)))$ and so $\alpha^{\prime}=\alpha^{\prime\prime}$, and so $\sup(y,\alpha)\in W$, as required. ∎

Remark 4.2**.**

Lemma 4.1 can also be proved using the notion of paths, as used by Van den Berg and De Marchi for $M$-types in [32, Proposition 5.7].

Now note that the action of morphisms restricts to the subobject $W$, making $W$ into a presheaf (and in fact a subpresheaf of $W_{0}$). We can then assign $W$ an algebra structure making into the initial algebra for the polynomial endofunctor.

4.2 Decidable and Locally Decidable Polynomials with

Reductions

We now define the class of polynomials with reductions that we will work over. The basic idea is that a polynomial is decidable when for each constructor there is either no reduction at all, or there is exactly one reduction. $W$-types with reductions over decidable polynomials can be viewed directly as dependent $W$-types. This makes them simple to construct but not so useful in practice when we already have $W$-types.

Therefore, instead of decidable polynomials with reductions, we look at locally decidable polynomials with reductions. In this case we work in an internal presheaf category, and then the polynomial does not have to be decidable in the internal logic of the presheaf category. It turns out to be sufficient that it is decidable in the external category, in order to construct the initial algebras.

Proposition 4.3**.**

The following are equivalent.

The polynomial with reductions (1) is isomorphic to one of the following form.

[TABLE] 2. 2.

$f\circ k$* is isomorphic to one of the inclusion maps of a coproduct.* 3. 3.

$f\circ k$* is a monomorphism with decidable image.* 4. 4.

In the internal logic, the following holds. For each constructor $y\in Y_{z}$, either there are no $x\in X_{y}$ such that $R_{z,y,x}$ is inhabited, or there exists exactly one $x\in X_{z,y}$ such that $R_{z,y,x}$ is inhabited, and in this case $R_{z,y,x}$ also has exactly one element.

Definition 4.4**.**

We say a polynomial with reductions is decidable if it satisfies one of the equivalent conditions in proposition 4.3.

Definition 4.5**.**

When we are working in the internal logic of the locally cartesian closed category, and $y\in Y_{z}$, we will say $y$ does not reduce if $R_{z,y,x}$ is empty for all $x$, and we will say $y$ reduces at $x$ if $x$ is unique such that $R_{z,y,x}$ is inhabited.

Definition 4.6**.**

We say a polynomial with reductions in presheaves is locally decidable if its image in $\mathbb{C}/\mathcal{C}_{0}$ after forgetting the action is decidable.

Proposition 4.7**.**

Suppose that $\mathbb{C}$ is a boolean topos with natural number object. Then a pointed polynomial endofunctor is decidable if and only if $f\circ k$ is monic. Similarly if $\mathbb{C}$ is a category internal presheaves over a boolean topos with natural number object, then a pointed polynomial endofunctor is locally decidable if and only if $f\circ k$ is monic.

Given a polynomial with reductions in a category of presheaves, it makes sense to talk about it being locally decidable and it also makes sense to talk about the polynomial with reductions being decidable internally in the category of presheaves. It’s important to note the distinction between the two notions.

Every decidable polynomial with reductions is also locally decidable, but the converse does not hold in general. Given a morphism $\sigma\colon c\rightarrow d$ in the internal category $\mathcal{C}$, locally decidability says that any $y\in Y(c)$ either lies in the image of $f_{c}\circ k_{c}$ or does not, and the same for $y\in Y(d)$. In any case we know that if $y\in Y(c)$ belongs to the image of $f_{c}\circ k_{c}$ then also $Y(\sigma)(y)$ belongs to the image of $f_{d}\circ k_{d}$. Decidability states that the converse also holds, so if $Y(\sigma)(y)$ lies in the image of $f_{d}\circ k_{d}$, then $y$ lies in the image of $f_{c}\circ k_{c}$. In order to get a result applicable to the CCHM model of type theory, we need it to apply to locally decidable pointed polynomial endofunctors that aren’t decidable. Explicitly, we need to allow for the case of $y\in Y(c)$ that does not belong to the image of $f_{c}\circ k_{c}$ but where $Y(\sigma)(y)$ does belong to the image of $f_{d}\circ k_{d}$, or informally “$\sup(y,\alpha)$ does not yet reduce at $c$, but will reduce at $d$.”

4.3 Construction of the Initial Algebras

Assume we are given a polynomial with reductions of the form (1) that is locally decidable. We will construct an initial algebra for the corresponding pointed endofunctor, showing that $W$-types with reductions exist for all locally decidable polynomials with reductions (theorem 4.16).

4.3.1 Normal Forms

We first form a variant of the dependent $W$-type $W_{0}$ that we used in the construction of dependent $W$-types in presheaves. We call this $N_{0}$, and define it as follows. For $c\in\mathcal{C}_{0}$ and $z\in Z(c)$, we add an element $\sup(y,\alpha)$ to $N(c,z)$ whenever $y\in Y(c,z)$ with $y\notin\operatorname{im}(f\circ k)$ and $\alpha\in\Pi_{d\in\mathcal{C}_{0}}\Pi_{\sigma\colon c\rightarrow d}\Pi_{x\in X(c,z,y)}N_{0}(d,h_{d}(Y(\sigma)(y)))$. For the moment we don’t add any naturality condition. Note that if $W_{0}$ is the corresponding $W$-type over all elements of $Y$ (again, with the naturality condition dropped), then we have a canonical monomorphism $i\colon N_{0}\rightarrow W_{0}$ over $Z$. We refer to elements of $N_{0}$ as normal forms. In other words we only consider those terms that do not reduce because they have constructor $y\in Y$ whose fibre over $f\circ k$ is empty. Like with $W_{0}$, we can define for each $\tau\colon c\rightarrow c^{\prime}$ and each $z\in Z(c)$, a map $N_{0}(\tau)\colon N_{0}(c,z)\rightarrow N_{0}(c^{\prime},Z(\tau)(z))$. Any element of $N_{0}(c,z)$ is of the form $\sup(y,\alpha)$. Define $\alpha^{\prime}$ the same as for $W_{0}$. Note that $\sup(Y(\tau)(y),\alpha^{\prime})$ is not necessarily an element of $N_{0}(c^{\prime},Z(\tau)(z))$, since $Y(\tau)(y)$ might reduce. However, by local decidability we can split into two cases: either $Y(\tau)(y)$ reduces or it does not. If it does not, we define $N_{0}(\tau)(\sup(y,\alpha))$ to be $\sup(Y(\tau)(y),\alpha^{\prime})$, the same as for $W_{0}$. If $Y(\tau)(y)$ reduces, at $x$, say, define $N_{0}(\tau)(\sup(y,\alpha))$ to be $\alpha(\tau,x)$. Unlike with $W_{0}$, this does not make $N_{0}$ into a presheaf over $Z$. We will see why in the proof of lemma 4.8.

4.3.2 The Presheaf of Natural Normal Forms

By analogy with $W$ in section 4.1, we define a subobject $N$ of $N_{0}$. Given $\sup(y,\alpha)\in N_{0}(c,z)$, we say it is natural if for all $\sigma\colon c\rightarrow d$ and $\tau\colon d\rightarrow e$ in $\mathcal{C}$ and all $x\in X_{Y(\sigma)(y)}$, we have $N_{0}(\tau)(\alpha(\sigma,x))=\alpha(\tau\circ\sigma,X(\tau)(x))$. We define the subobject $N$ of $N_{0}$ of hereditarily natural elements to be those of the form $\sup(y,\alpha)$ which are natural and such that for all $\sigma\colon c\rightarrow d$ and all $x\in X_{Y(\sigma)(y)}$, $\alpha(\sigma,x)$ is hereditarily natural. Formally, we can define this object using the same technique as for lemma 4.1.

Note that for each $\tau\colon c\rightarrow c^{\prime}$, $N_{0}(\tau)$ restricts to a map $N(c,z)\rightarrow N(c^{\prime},Z(\tau)(z))$. We now verify that this does give an internal presheaf.

Lemma 4.8**.**

$N$* with the action of morphisms defined above is a presheaf.*

Proof.

It is straightforward to check that the action preserves identities.

Now suppose we are given $\sigma\colon c\rightarrow d$ and $\tau\colon d\rightarrow e$. We need to verify that for all $v\in N(c,z)$, $N(\tau\circ\sigma)(v)=N(\tau)(N(\sigma)(v))$. We know that $v$ must be of the form $\sup(y,\alpha)$. The equation is straightforward to check when $Y(\sigma)(y)$ does not reduce. Hence we just show the case when $Y(\sigma)(y)$ reduces at $x\in X_{y}$, for which we will need naturality. Note that $Y(\tau\circ\sigma)(y)$ reduces at $X(\tau)(x)$.

[TABLE]

∎

4.3.3 The Algebra Structure

It only remains to check that $N$ really is an initial algebra. In this section we define the algebra structure $s$. We will use the presentation we saw in section 2.2 where an algebra structure is an algebra structure for the underlying dependent polynomial endofunctor that satisfies the reduction equations. We need to define $s_{z,c}(y,\alpha)$ whenever $\alpha\colon f^{\ast}(\mathbf{y}(c))\rightarrow h^{\ast}(N)$. As explained in section 4.1, this is just an element of $\Pi_{\Sigma_{\sigma\colon c\rightarrow d}X(Y(\sigma)(y))}N(d,Z(\sigma)(z))$ that satisfies the naturality condition. We split into cases depending on whether $y$ reduces. If it does, then we define $s(y,\alpha)$ to be $\alpha(x)$ where $y$ reduces at $x$. Otherwise, we take $s(y,\alpha)$ to be the element $\sup(y,\alpha)$ in $N_{0}$, which in fact lies in $N$ since it is clearly hereditarily natural by the fact that $\alpha$ maps into $N$ and is natural. We also need to show that $s$ is natural, which we do in the lemma below.

Lemma 4.9**.**

The operation $s_{z,c}$ defined above is natural in the following sense. For any $\tau\colon c\rightarrow c^{\prime}$ in $\mathcal{C}$ and $z\in Z(c)$, we have the following commutative diagram (where the dependent product is the one internal in the category of presheaves).

[TABLE]

Proof.

Let $(y,\alpha)\in\Sigma_{g}\Pi_{f}h^{\ast}(N)(c)$.

There are three cases to consider. Either neither $y$ nor $Y(\tau)(y)$ reduces, or $Y(\tau)(y)$ reduces but not $y$, or $y$ reduces. The first case is essentially the same as for ordinary $W$-types in presheaves, and the other two cases are straightforward to check. ∎

Finally, we also need to check the reduction equations. However, note that they hold internally if and only if they hold pointwise, and it is clear that they do by the definition of $N$ and $s$.

We can now deduce the following lemma.

Lemma 4.10**.**

The operation $s_{c}$ defined above gives $N$ the structure of an algebra over the given pointed polynomial endofunctor.

4.3.4 Proof of Initiality

We now show that the algebra structure we have defined really is initial. Suppose we are given an internal presheaf $A$ with the structure of an algebra over the pointed polynomial endofunctor. As before we use the presentation in section 2.2, where we view an algebra over the pointed endofunctor as an algebra structure over the dependent polynomial endofunctor $\Sigma_{g}\Pi_{f}h^{\ast}$, which we’ll write as $r\colon\Sigma_{g}\Pi_{f}h^{\ast}(A)\rightarrow A$, such that this algebra structure satisfies the reduction equations. We need to define a structure preserving map $t\colon N\rightarrow A$, and show that it is the unique such map.

The basic idea for the definition of $t$ is fairly simple. Given $\sup(y,\alpha)$ in $N(c,z)$, we want to define $t(\sup(y,\alpha))$ to be $r(y,t\circ\alpha)$. This is however quite tricky to formalise, since $r(y,t\circ\alpha)$ is only well defined when we know that $t\circ\alpha$ is natural, but this only makes sense when we have already defined at least some of $t$. This issue already occurs for ordinary $W$-types in presheaves, but is especially relevant here, where the proof of naturality is more difficult. What we need to do is to simultaneously show that $t$ is natural while we are defining it, since then we can deduce that $t\circ\alpha$ is also natural, and so $r(y,t\circ\alpha)$ is well defined.

To help us with this, we define another presheaf $T$, again using dependent $W$-types in $\mathbb{C}$ over $Z$, where we modify the definition of $N$ by adding in also elements of $A$. We will in fact construct $T$ in several stages, first using a dependent $W$-type, $T_{0}$, then taking a succession of inductively defined subobjects $T_{1}$, $T_{2}$ and finally $T$. In each case, we’ll just give the inductive definition, but in fact they can all be constructed in arbitrary locally cartesian closed categories with $W$-types using similar techniques to those in the proof of lemma 4.1.

We first define the dependent $W$-type, $T_{0}$ by the following inductive definition.

Let $c\in\mathcal{C}$ and $z\in Z(c)$. Suppose that we are given $y\in Y(c,z)$ such that $y$ does not reduce, $a\in A(c,z)$ and $\alpha$ in $\Pi_{\Sigma_{\sigma\colon c\rightarrow d}X(Y(\sigma)(y))}T_{0}(d,Z(\sigma)(z))$. Then $T_{0}(c,z)$ contains an element of the form $\sup(y,a,\alpha)$.

Note that we have a projection $\pi_{0}\colon T_{0}\rightarrow N_{0}$ over $Z$ by simply “forgetting” the $a$’s. We also have a projection $\pi_{1}\colon T_{0}\rightarrow A$ given by $\pi_{1}(\sup(y,a,\alpha)):=a$.

We define $T_{0}(\tau)\colon T_{0}(c,z)\rightarrow T_{0}(c^{\prime},Z(\tau)(z))$ the same as for $N_{0}(\tau)$. We now define $T_{1}$ to be the subobject of $T_{0}$ of hereditarily natural elements, which is defined exactly the same as in $N$. It follows that $\pi_{0}$ restricts to a function $T_{1}\rightarrow N$. We also have naturality in the following lemma.

Lemma 4.11**.**

Let $\tau\colon c\rightarrow c^{\prime}$. Then $T_{0}(\tau)$ restricts to a morphism $T_{1}(\tau)\colon T_{1}(c,z)\rightarrow T_{1}(c^{\prime},Z(\tau)(z))$. This makes $T_{1}$ into a presheaf, and the restriction of $\pi_{0}$ into a natural transformation.

Proof.

Since we mimicked the construction of $N$ from $N_{0}$, it’s clear that we can use the same proof as in lemma 4.8 to show $T_{1}$ is a presheaf and that $\pi_{0}$ is natural. ∎

We now define a subobject $T_{2}$ of $T_{1}$ by the following inductive definition. Given, $\sup(y,a,\alpha)\in T_{1}$, we say $\sup(y,a,\alpha)$ belongs to $T_{2}$ if the following hold.

If $\sigma\colon c\rightarrow d$ is such that $Y(\sigma)(y)$ reduces at $x$, then $A(\sigma)(a)=\pi_{1}(\alpha(\sigma,x))$. 2. 2.

For all $\sigma\colon c\rightarrow d$ and $x\in X(d,Y(\tau)(y))$, $\alpha(\sigma,x)\in T_{2}$.

We can now show the following lemma.

Lemma 4.12**.**

The restriction of $\pi_{1}$ to $T_{2}$ is natural.

Proof.

Suppose we are given $\sup(y,a,\alpha)\in T_{2}(c,z)$. We need to show that $\pi_{1}(T_{2}(\tau)(\sup(y,a,\alpha)))=A(\tau)(\pi_{1}(\sup(y,a,\alpha)))$. This is clear when $Y(\tau)(y)$ does not reduce. When $Y(\tau)(y)$ does reduce it’s still clear, but we need to use the clause added to the definition of $T_{2}$ (it does not hold for $T_{1}$). ∎

The key point is that naturality in the definition of $T_{1}$ ensures that we also have naturality for the composition of $\alpha$ with projection to $A$, in the following sense.

Lemma 4.13**.**

For each $\sup(y,a,\alpha)$ in $T_{2}(c,z)$, $\pi_{1}\circ\alpha$ is natural.

Proof.

This is straightforward from the definition of $T_{1}$ (together with the observation that the same then applies when restricting to the subobject $T_{2}$) and lemma 4.12. ∎

We now know that the expression $r(y,\pi_{1}\circ\alpha)$ is well defined, which finally allows us to define $T$ as the subobject of $T_{2}$ defined inductively as follows. An element $\sup(y,a,\alpha)$ of $T_{2}$ belongs to $T$ if both of the conditions below hold.

$a=r(y,\pi_{1}\circ\alpha)$ 2. 2.

For all $\sigma\colon c\rightarrow d$ and $x\in X(d,Y(\tau)(y))$, $\alpha(\sigma,x)\in T$.

We can now show the main lemma.

Lemma 4.14**.**

Let $T$ be as above. Then $\pi_{0}\colon T\rightarrow N$ is an isomorphism.

Proof.

We show by induction on the construction of $N$ that for all $v\in N$, the fibre $\pi_{0}^{-1}(\{v\})$ in $T$ contains exactly one element.

Suppose we are given an element of $N(c,z)$ of the form $\sup(y,\alpha)$. Clearly any element of $\pi_{0}^{-1}(\sup(y,\alpha))$ must be of the form $\sup(y,r(y,\pi_{1}\circ\pi_{0}^{-1}\circ\alpha),\pi_{0}^{-1}\circ\alpha)$. We just need to check that this really is a well defined expression and that it belongs to $T$ (as opposed to just $T_{0}$, say).

In the above, we were just using $\pi_{0}^{-1}$ as a convenient notation for a partial function, rather than a total inverse. Note however, that the induction hypothesis tells us that $\pi_{0}^{-1}\circ\alpha$ is a well defined function and the usual proof that the levelwise inverse of a natural transformation is natural still applies and, together with lemma 4.11 and the naturality of $\alpha$, allows us to show that $\pi_{0}^{-1}\circ\alpha$ is natural.

It follows from the above together with lemma 4.12 that $\pi_{1}\circ\pi_{0}^{-1}\circ\alpha$ is natural and so $r(y,\pi_{1}\circ\pi_{0}^{-1}\circ\alpha)$ is a well defined expression. Hence $\sup(y,r(y,\pi_{1}\circ\pi_{0}^{-1}\circ\alpha),\pi_{0}^{-1}\circ\alpha)$ is a valid expression for an element of $T_{0}$. We just need to show that it belongs to the subobject $T$.

From the naturality of $\pi_{0}^{-1}\circ\alpha$ that we’ve already seen, it’s clear that $\sup(y,r(y,\pi_{1}\circ\pi_{0}^{-1}\circ\alpha),\pi_{0}^{-1}\circ\alpha)$ belongs to $T_{1}$.

To show it belongs to $T_{2}$, we need to show that when $\tau\colon c\rightarrow d$ is such that $Y(\tau)(y)$ reduces at $x$, we have $A(\tau)(r(y,\pi_{1}\circ\pi_{0}^{-1}\circ\alpha))=\pi_{1}(\pi_{0}^{-1}(\alpha(\tau,x)))$. However, this follows directly from the naturality of $r$ together with the fact that $r$ was required to respect the reduction equations.

It’s now clear that $\sup(y,r(y,\pi_{1}\circ\pi_{0}^{-1}\circ\alpha),\pi_{0}^{-1}\circ\alpha)$ belongs to $\pi_{0}^{-1}(\{\sup(y,\alpha)\})$ in $T$ and that in fact it’s the unique such object. ∎

We can now define $t\colon N\rightarrow A$ to be $\pi_{1}\circ\pi_{0}^{-1}$. We now just need to check that it is a structure preserving map, and unique with this property.

Lemma 4.15**.**

The map $t\colon N\rightarrow A$ defined by $\pi_{1}\circ\pi_{0}^{-1}$ is a natural transformation that is structure preserving and is the unique such map.

Proof.

Naturality follows from lemmas 4.11 and 4.12.

To show that $t$ is structure preserving, we again need to split into two cases depending on whether there is a reduction. However, both cases are straightforward to show from the definition.

It’s also clear from the definition that $t$ is the unique structure preserving map, and in fact for uniqueness it’s sufficient just to look at the case where there is no reduction. ∎

We can now deduce the main theorem of this section.

Theorem 4.16**.**

In any category of internal presheaves in a locally cartesian closed category with disjoint coproducts, every locally decidable pointed polynomial endofunctor has an initial algebra.

5 $W$-Types with Reductions in Classical Logic

We will see in this section how to construct all $W$-types with reductions in boolean toposes with natural number object. We have already seen the main idea in the previous section. Every topos is a category of internal presheaves over itself via the trivial category, and in this case locally decidable is the same as decidable. For a boolean topos, a polynomial with reductions is decidable just when the map $f\circ k$ is monic. This only leaves the case where $f\circ k$ is not monic. What this says is that the same constructor can reduce in more than one place. The key point is that when we know that this happens, things become trivial, in the following sense.

Lemma 5.1**.**

Suppose we are given a polynomial with reductions of the form (1). Let $(A_{z})_{z\in Z}$ be a family of types over $Z$ with algebra structure given by $c$ (which we will view as an algebra on the underlying polynomial that satisfies the reduction equations). Suppose that for some $z\in Z$ there is a constructor $y\in Y_{z}$ that reduces in two distinct places $x_{1}\neq x_{2}\in X_{y}$ and there exists a dependent function $\alpha:\Pi_{x\in X_{y}}A_{h(z)}$. Then $A_{z}$ contains exactly one element.

Proof.

First of all, note that $A_{z}$ contains at least one element using the algebra structure, which is $c(y,\alpha)$.

Next, suppose that $a_{1}$ and $a_{2}$ are both elements of $A_{z}$. Then we define a new dependent function $\alpha^{\prime}$ as follows.

[TABLE]

Note that the coherence condition ensures that this is still a dependent function of type $\Pi_{x:X_{y}}A_{h(x)}$. Also note that we needed classical logic to show this is a well defined function.

Then the reduction equation at $x_{1}$ tell us $c(y,\alpha^{\prime})=a_{1}$, and the reduction equation at $x_{2}$ tells us $c(y,\alpha^{\prime})=a_{2}$. Hence $a_{1}=a_{2}$. Therefore, $A_{z}$ contains exactly one element. ∎

We will now use this idea to construct any $W$-type with reductions. We aim towards the following theorem.

Theorem 5.2**.**

Let $\mathbb{C}$ be a boolean topos with natural number object. Then $\mathbb{C}$ has all $W$-types with reductions.

We first define a useful construction. Suppose we are given a subobject $C\subseteq Z$. Then we construct a new polynomial as follows. We work over the same context $Z$. For $z\in C$, we define the set of constructors $Y^{\prime}_{z}$ to consist of exactly one element $\ast$, with empty arity $X^{\prime}_{\ast}:=\emptyset$.

Otherwise, for $z\notin C$, we define $Y^{\prime}_{z}$ to be the subobject of $Y_{z}$ consisting of those $y$ with no reductions. That is, those where $R_{y,x}=\emptyset$ for all $x\in X_{y}$. We define the arity $X^{\prime}_{y}$ to be $X_{y}$.

Write $W^{C}$ for the resulting $W$-type on the polynomial. Observe that for $z\in C$, $W^{C}_{z}$ has exactly one element, of the form $\sup(\ast,\emptyset)$, where $\ast$ is the only constructor over $z$.

Remark 5.3**.**

For the special case $C=\emptyset$, this gives us the definition of normal forms like in section 4.3.1. For the special case $C=Z$, the resulting $W$-type contains exactly one element in every fibre of $z\in Z$.

We say that $C$ is closed if whenever $z\in Z$ is such that there exists a constructor $y\in Y_{z}$ that reduces in two distinct places $x_{1}\neq x_{2}$ and there exists some dependent function $\alpha:\Pi_{x:X_{y}}W^{C}_{h(x)}$, then we have $z\in C$.

We then define $C_{0}$ to be the intersection of all closed sets $C$.

Lemma 5.4**.**

$C_{0}$* is itself closed.*

Proof.

Let $z\in Z$ be such that there exists a constructor $y\in Y_{z}$ that reduces in two distinct places $x_{1}\neq x_{2}$ and let $\alpha:\Pi_{x:X_{y}}W^{C_{0}}_{h(x)}$. We need to show that for any closed set $C$, $z\in C$, so let $C$ be an arbitrary closed set.

We first construct a map $i\colon W^{C_{0}}\rightarrow W^{C}$ over $Z$ recursively as follows. Suppose that $z^{\prime}\in Z$, and we are given an element of $W^{C_{0}}_{z^{\prime}}$ of the form $\sup(y,\alpha)$.

First suppose that $z^{\prime}\in C$. In this case we take $i(\sup(y,\alpha))$ to be the unique element of $W^{C}_{z^{\prime}}$.

Otherwise we know that $z^{\prime}\notin C$. In that case, we define $i(\sup(y,\alpha))$ to be $\sup(y,i\circ\alpha)$, which is a valid element of $W^{C}_{z^{\prime}}$ since $z^{\prime}\notin C$, and also $z^{\prime}\notin C_{0}$ (since $C_{0}\subseteq C$).

We then use $i$ to construct an element of $\Pi_{x\in X_{y}}W^{C}_{h(x)}$ defined by $i\circ\alpha$. But we can now deduce that $z\in C$.

Since we showed $z\in C$ for any closed set, we have $z\in C_{0}$, and so $C_{0}$ is closed, as required. ∎

Lemma 5.5**.**

For any closed set $C$, we give $W^{C}$ an algebra structure $d$ for our given polynomial with reductions.

Proof.

Suppose we are given $y\in Y_{z}$ for some $z\in Z$, and a dependent function $\alpha:\Pi_{x\in X_{y}}W^{C}_{h(x)}$. To define $d(y,\alpha)$ we split into cases. Firstly, if $z\in C$, we take $d(y,\alpha)$ to be the unique element of $W^{C}_{z}$. Now consider just the case when $z\notin C$. If $y$ reduces in two different places, then we could show $z\in C$, since $C$ is closed, deriving a contradiction. Hence we may assume that $y$ either reduces exactly once, or not at all. We now proceed the same as in section 4.3.3. If $y$ reduces at $x$, we define $d(y,\alpha)$ to be $\alpha(x)$. Otherwise $y$ does not reduce at all, and so we can use the $W$-type structure and take $d(y,\alpha)$ to be $\sup(y,\alpha)$.

This algebra structure clearly satisfies the reduction equations. ∎

Lemma 5.6**.**

$W^{C_{0}}$* with the algebra structure given in lemma 5.5 is initial.*

Proof.

Suppose we are given a family of types $(A_{z})_{z\in Z}$ with algebra structure $c$. We need to show that there is a unique structure preserving map $i\colon W^{C_{0}}\rightarrow A$ over $Z$.

We define $C$ to consist of those $z\in Z$ such that $A_{z}$ contains exactly one element. We now recursively define a map $j\colon W^{C}\rightarrow A$. Suppose we are given $z\in Z$, and $\sup(y,\alpha)\in W^{C}_{z}$. If $y=\ast$, then we must have $z\in C$. But then we can take $j(\sup(\ast,\alpha))$ to be the unique element of $A_{z}$. Otherwise, $y$ must be one of the original constructors in $Y_{z}$, and $\alpha:\Pi_{x:X_{y}}W^{C}_{h(x)}$. We define $j(\sup(y,\alpha))$ to be $c(y,j\circ\alpha)$.

We can now deduce that $C$ is closed, since if we are given a constructor $y\in Y_{z}$ that reduces in two distinct places and a dependent function $\alpha:\Pi_{x:X_{y}}W^{C}_{h(x)}$, then by considering $j\circ\alpha$, we show by lemma 5.1 that $A_{z}$ has exactly one element, and so $z\in C$. But this implies that $C_{0}\subseteq C$, and so we get a canonical map $W^{C_{0}}\rightarrow W^{C}$, as in the proof of lemma 5.4. Composing with $j$ gives us the map $W^{C_{0}}\rightarrow A$ over $Z$.

However, it is now straightforward to check that this is the unique structure preserving map. ∎

We can now use the above lemma to deduce the main theorem 5.2.

6 Cofibrantly Generated Awfs’s in Codomain Fibrations

6.1 Review of Lifting Problems over Codomain Fibrations

We recall some definitions from [28, Section 7.5]. Since we focus only on the special case of codomain fibrations, we can simplify some of the definitions a little.

Definition 6.1**.**

Let $f$ be a map in $\mathbb{C}/I$ and let $g$ be a map in $\mathbb{C}/J$. A family of lifting problems from $f$ to $g$ over $K\in\mathbb{C}$ is diagram of the following form, where the squares on the left are both pullbacks.

[TABLE]

A solution to the family of lifting problems is a map $\sigma^{\ast}(V)\rightarrow X$ making the upper right square into two commutative triangles.

Definition 6.2**.**

Let $f$ be a map in $\mathbb{C}/I$ and let $g$ be a map in $\mathbb{C}/J$. The universal family of lifting problems from $f$ to $g$, is the family of lifting problems, where we define $K$ to be type below,

[TABLE]

and the right maps in the family of lifting problems are given by evaluation.

Definition 6.3**.**

Fix a map $Y\rightarrow J$. Step 1 of the small object argument at $Y$ is the pointed endofunctor $R_{1}\colon\mathbb{C}/Y\rightarrow\mathbb{C}/Y$ defined as follows. Suppose that we are given $f\colon X\rightarrow Y$ in $\mathbb{C}/Y$. We first form the universal lifting problem from $m$ to $f$ as in definition 6.2. We then define $R_{1}f$ to be the unique map out of the pushout, with unit given by the pushout inclusion $\lambda_{f}$, as below.

[TABLE]

We recall the following from [28, Theorem 7.5.2] (see also [28, Remark 7.5.6], and [28, Section 4.4] for the more general and precise definitions of fibred and strongly fibred).

Proposition 6.4**.**

The pointed endofunctors are preserved by pullback along all maps $J^{\prime}\rightarrow J$. We say $R_{1}$ is a fibred lawfs.

Definition 6.5**.**

We say $R_{1}$ is strongly fibred if it is preserved by pullback along all maps $Y^{\prime}\rightarrow Y$.

Given any $f\colon X\rightarrow Y$ in $\mathbb{C}/Y$, we have a pointed endofunctor, which we will denote $I_{X}$, defined by coproduct, sending $X^{\prime}$ to $X^{\prime}+X$, with unit given by coproduct inclusion. We clearly have the following proposition (by taking reductions and arities both to be initial).

Proposition 6.6**.**

For any $X$, $I_{X}$ is pointed polynomial.

Theorem 6.7**.**

Suppose that for each map $Y\rightarrow J$ and every $f\colon X\rightarrow Y$ in $\mathbb{C}/Y$ we are given a choice of initial algebra for the pointed endofunctor $I_{X}+R_{1}$. Then the awfs cofibrantly generated by $m$ exists, and is fibred.

Proof.

See [28, Corollary 5.4.7].

∎

Theorem 6.8**.**

If $R_{1}$ is strongly fibred then so is the resulting cofibrantly generated rawfs, if it exists.

Proof.

See [28, Theorem 5.5.2]. ∎

6.2 Step 1 as a Pointed Polynomial Endofunctor

Theorem 6.9**.**

$R_{1}$* is pointed polynomial.*

Proof.

Unfolding the type theoretic definition of universal lifting problem, we get the following descriptions of $\sigma^{\ast}(U)$ and $\sigma^{\ast}(V)$.

[TABLE]

However, like this it is clear that the definition matches the definition of pointed polynomial endofunctor. ∎

It is easiest to understand the definition of the polynomial with reductions for $R_{1}$ when we phrase it in terms of constructors, arities, reindexing and reductions. We read these off from the description above.

The overall context we are working in is the object $Y$, which in type theoretic notation is $\Sigma_{j:J}Y(j)$ (since we are thinking of $Y$ as a family of types indexed by $J$).

A constructor over $(j,y)$ for $j:J$ and $y:Y(j)$ consists of $i:I$, $v_{0}:V(i)$ and a map $\beta\colon V(i)\rightarrow Y(j)$ such that $\beta(v_{0})=y$.

The arity of the constructor $(i,v_{0},\beta)$ is $\Sigma_{v:V(i)}U(i,v)$.

The reindexing map sends $(i,v_{0},\beta,(v,u))$ to $\beta(v)$.

Finally, the reduction equations say that given $\alpha:\Pi_{\Sigma_{v:V(i)}U(i,v)}X(j,\beta(j,p_{0}(z)))$ and $u:U(v_{0})$, $\sup(i,v_{0},\beta,\alpha)$ reduces to $\alpha(v_{0},u_{0})$ (where $\sup(i,v_{0},\beta,\alpha)$ is given by some $R_{1}$-algebra structure).

We can think of the corresponding $W$-type with reductions directly in terms of lifting problems as follows. Suppose we are given a constructor $(i,v_{0},\beta)$ and a map $\alpha:\Pi_{\Sigma_{v:V(i)}U(i,v)}X(j,\beta(j,p_{0}(z)))$. Then, firstly $\beta$ and $\alpha$ together form a lifting problem of $m_{i}$ against $f_{j}$. We think of $\sup(i,v_{0},\beta,\alpha)$ as a diagonal filler of the lifting problem, evaluated at $v_{0}$. The reduction equations then ensure that the upper triangle of the diagonal filler commutes. Therefore, we think of an initial algebra of $R_{1}$ as the result of freely adding a filler for every lifting problem, subject to ensuring that the upper triangles do always commute.

An initial algebra for $R_{1}+I_{X}$ is similar. Once again, we are freely adding a filler for every lifting problem. However in this case we start off with a copy of $X$ before adding all the fillers.

Finally, we will later need the lemma below.

Lemma 6.10**.**

For each $Y\rightarrow J$, $R_{1}$ at $Y$ is generated by the polynomial with reductions of the form below, where the map $A\rightarrow C$ is a pullback of the map $U\rightarrow I$.

[TABLE]

Proof.

We can read off an description of the map $A\rightarrow C$ from the arguments above.555The same is true for the other maps, but we don’t need them here, and it is somewhat messy.

In type theoretic notation, $A$ and $C$ are defined as below, with the map $A\rightarrow C$ given by projection.

[TABLE]

However, in this form it is clear that the map $A\rightarrow C$ is just the pullback of the map $U\rightarrow I$ along the projection $C\rightarrow I$. ∎

We can now deduce the following.

Theorem 6.11**.**

Suppose we are given a family of maps of the following form over the codomain functor on a $\Pi W$-pretopos

[TABLE]

Furthermore suppose we are given a 2-cover base of the map $U\rightarrow I$. Then $m$ cofibrantly generates an awfs.

Proof.

We have shown in theorem 6.9 that $R_{1}$ is pointed polynomial. Hence for each $f\colon X\rightarrow Y$, the pointed endofunctor $R_{1}+I_{X}$ from theorem 6.7 is also pointed polynomial.

$I_{X}$ trivially has a $2$-cover base. $R_{1}$ has a $2$-cover base since by lemma 6.10 it is a pullback of the map $U\rightarrow I$ for which we are given a $2$-cover base and so we can apply lemma 3.10.

Hence we can construct a $2$-cover base for each $R_{1}+I_{X}$ by lemma 3.11.

But then by theorem 3.19 we can find initial algebras, so we can deduce by theorem 6.7 that the cofibrantly generated awfs on $m$ exists. ∎

Corollary 6.12**.**

Suppose we are given a family of maps of the following form over the codomain functor on a $\Pi W$-pretopos satisfying $\mathbf{WISC}$

[TABLE]

Then the awfs cofibrantly generated by the family of maps exists.

Proof.

By $\mathbf{WISC}$, the map $U\rightarrow I$ has a 2-cover base. Hence we can apply theorem 6.11. ∎

Remark 6.13**.**

One might expect that corollary 6.12 can be proved directly without going via theorem 6.11, by using $\mathbf{WISC}$ directly to find each $2$-cover base. However, this doesn’t work because we need to have a choice of $2$-cover bases for every vertical map $X\rightarrow Y\rightarrow J$, and $\mathbf{WISC}$ only tells us at least one such $2$-cover base exists. When we use theorem 6.11 this does not matter because we only have to apply $\mathbf{WISC}$ once (or rather, twice), to get a $2$-cover base for the map $U\rightarrow I$, and from that we can define all the other $2$-cover bases that we need.

We can also apply the simplified construction from section 4 to get the following theorem.

Theorem 6.14**.**

Let $\mathbb{C}$ be a finitely cocomplete locally cartesian closed category with disjoint coproducts. Let $\mathcal{A}$ be an internal category in $\mathbb{C}$, and $\mathbb{C}^{\mathcal{A}}$ the category of diagrams of shape $\mathcal{A}$. Suppose we are given a family of maps of the following form over the codomain functor on $\mathbb{C}^{\mathcal{A}}$.

[TABLE]

Suppose further that the map $U\rightarrow V$ is locally decidable.

Then the awfs cofibrantly generated by the diagram exists.

Proof.

Note that locally decidable maps are closed under pullback and coproduct. Hence, by a similar argument to the one in the proof of theorem 6.11, we see that $R_{1}+I_{X}$ is a locally decidable point polynomial endofunctor. We can then deduce the result by theorems 6.7 and 4.16. ∎

6.3 Lifting Problems for Squares

Recall that in [28, Section 8] the author showed that Sattler’s notion of lifting problem for squares (from [25]) can be generalised to work over a fibration. We apply this to the codomain fibration on $\mathbb{C}$ to get the following.

Suppose that we are given a diagram of the following from.

[TABLE]

Definition 6.15**.**

Let $f\colon X\rightarrow Y$ be a morphism in $\mathbb{C}/J$ for some $J\in\mathbb{C}$. We say a family of lifting problems from (9) to $f$ is a family of lifting problems (in the sense of definition 6.1) from $m_{1}$ to $f$.

Note that pasting the family of lifting problems to the pullback of (9) gives a commutative diagram of the following form.

[TABLE]

Definition 6.16**.**

A solution to the family of lifting problems is a map $\sigma^{\ast}(V_{0})\rightarrow X$ making the upper rectangle in (10) into two commutative triangles.

Definition 6.17**.**

The universal family of lifting problems from (9) to $f\colon X\rightarrow Y$ is the universal family of lifting problems from $m_{1}$ to $f$.

Recall from section 6.1 that the universal lifting problem is defined type theoretically by taking $K$ to be the following type, with the right maps given by evaluation.

[TABLE]

We use this to construct a pointed endofunctor over $\operatorname{cod}$.

Definition 6.18**.**

Fix a square over an object $I$ as in (9). We define a pointed endofunctor $R_{1}$ over $\operatorname{cod}$ called step one of the small object argument as follows. Given $f\colon X\rightarrow Y$ we define $R_{1}f$ to be the map below given by the universal property of the pushout, where we take $\sigma\colon K\rightarrow I$ to be as in the universal lifting problem from the square to $f$. The unit at $f$, is given by the inclusion $\lambda_{f}$ into the pushout.

[TABLE]

Lemma 6.19**.**

For any family of squares as in (9), step one of the small object argument is a pointed polynomial endofunctor.

Proof.

By unfolding the type theoretic definition, similarly to as in theorem 6.9. ∎

Theorem 6.20**.**

Suppose that $\mathbb{C}$ is a locally cartesian closed category and we are given a family of squares as in (9). Suppose further that one of the following two conditions holds.

$\mathbb{C}$* is a $\Pi W$-pretopos that satisfies $\mathbf{WISC}$.* 2. 2.

$\mathbb{C}$* is a category of internal presheaves over a finitely cocomplete locally cartesian closed category with disjoint coproducts, and the map $U_{0}\rightarrow V_{0}$ is a locally decidable monomorphism.*

Then the rawfs cofibrantly generated by (9) exists.

Furthermore, if the map $V_{1}\rightarrow I$ is an isomorphism then the resulting rawfs is strongly fibred.

Proof.

Similar to corollary 6.12 and theorem 6.14, this time using lemma 6.19 and [28, Theorem 5.3.6].

For showing the rawfs is strongly fibred, we use [28, Theorem 5.3.8 and Lemma 8.2.1]. ∎

7 Recovering $W$-Types from Cofibrantly Generated Awfs’s

In section 6 we saw that cofibrantly generated awfs’s could be constructed using $W$-types and $\mathbf{WISC}$. We will know show that the assumption of the existence of $W$-types is strictly necessary. We will show that in fact $W$-types can be recovered from the existence of cofibrantly generated awfs’s. This shows that the results in section 6 don’t hold for the category of sets in $\mathbf{CZF}$, even if we add $\mathbf{PAx}$, a choice axiom which implies $\mathbf{WISC}$.

Theorem 7.1**.**

Let $\mathbb{C}$ be a locally cartesian closed category with disjoint coproducts. Suppose that every monic decidable family of maps cofibrantly generates an awfs. Then $\mathbb{C}$ has all $W$-types.

Proof.

Let $f\colon A\rightarrow B$ be a morphism in $\mathbb{C}$. We then consider the following family of morphisms.

[TABLE]

Let $X$ be an object of $\mathbb{C}$. Writing the local exponential as a dependent product, the universal lifting problem of $\iota_{0}$ against the unique map $X\rightarrow 1$ is of the following form, where the top map is given by evaluation.

[TABLE]

Since $\mathbb{C}$ is locally cartesian closed, pullback preserves coproduct, and so we have $\Pi_{f}(A^{\ast}(X))\times_{B}(A+B)\cong(\Pi_{f}(A^{\ast}(X))\times_{B}A)+(\Pi_{f}(A^{\ast}(X))\times_{B}B)$. The second component is just the pullback of an identity map, so we deduce that the universal lifting problem is actually of the form below.

[TABLE]

We deduce that solutions to the universal lifting problem correspond precisely to algebra structures on $X$ for the polynomial endofunctor $\Sigma_{B}\circ\Pi_{f}\circ A^{\ast}$. Therefore an initial algebra for the polynomial endofunctor is exactly the factorisation of $0\rightarrow 1$ in the cofibrantly generated awfs. ∎

Corollary 7.2**.**

In $\mathbf{CZF}+\mathbf{PAx}$ one cannot prove that cofibrantly generated awfs’s exist for every monic decidable family of maps for the codomain fibration over the category of sets.

Proof.

By theorem 7.1 the existence of cofibrantly generated awfs’s implies that the category of sets has $W$-types. However, $\mathbf{CZF}+\mathbf{PAx}$ has the same consistency strength as $\mathbf{CZF}$ itself, but the addition of $W$-types leads to a strictly higher consistency strength (see [21]). ∎

8 Examples of Previously Unknown Awfs’s

We now give some new examples of awfs’s, all based on realizability. We assume that the reader is already familiar with well known definitions in realizability such as pca’s, assemblies and realizability and relative realizability toposes. See the reference [33] by Van Oosten for a comprehensive introduction to all of these notions. We will use the same terminology and notation as Van Oosten.

None of these categories admit colimits over arbitrary infinite sequences (even countably infinite sequences).

8.1 Kan Fibrations in the Effective Topos

In [31], Van den Berg and Frumin considered two classes of maps in the effective topos, $\mathcal{E}ff$ referred to as trivial fibrations and fibrations. In [28, Section 7.5.2], the author showed that these classes are both cofibrantly generated with respect to the codomain fibration, by the following two families of maps.

[TABLE]

In loc. cit., Van den Berg and Frumin showed that if one restricts to the full subcategory of $\mathcal{E}ff$ of fibrant objects (i.e. objects $X$ where the unique map $X\rightarrow 1$ is a fibration) then fibrations are the right classes of a wfs, and moreover this forms part of a model structure on the subcategory. However, their proof relies on restricting to fibrant objects, and doesn’t apply to the entire category $\mathcal{E}ff$.

We can now confirm that in fact, we do get awfs’s on all of $\mathcal{E}ff$, without restricting to fibrant objects.

Theorem 8.1**.**

There are awfs’s $(C,F^{t})$ and $(C^{t},F)$ on $\mathcal{E}ff$ such that

A map admits an $F^{t}$-algebra structure if and only if it is a trivial fibration. 2. 2.

A map admits an $F$-algebra structure if and only if it is a fibration. 3. 3.

The awfs $(C,F^{t})$ is strongly fibred (i.e. stable under pullback).

Proof.

In [30], Van den Berg showed that $\mathcal{E}ff$ is a $\Pi W$-pretopos and satisfies $\mathbf{WISC}$ (there referred to as AMC). We can therefore construct $(C,F^{t})$ and $(C^{t},F)$ using corollary 6.12. We see that $(C,F^{t})$ is strongly fibred by [28, Corollary 7.5.5]. ∎

Remark 8.2**.**

In fact we can define $(C,F^{t})$ in two different ways. We can either take the underlying lawfs to be $(C_{1},F^{t}_{1})$ together with a multiplication that we can add using the fact that cofibrations can be composed. Alternatively, we can take $(C,F^{t})$ to be the awfs algebraically free on $(C_{1},F^{t}_{1})$. As Gambino and Sattler point out in [10, Remark 9.5] these two definitions are not the same. However, both are strongly fibred and we end up with the same wfs in either case.

8.2 Computable Hurewicz Fibrations in the Kleene-Vesley Topos

Recall that the function realizability topos, $\mathbf{RT}(\mathcal{K}_{2})$ is the realizability topos on $\mathcal{K}_{2}$. Then $\mathbf{RT}(\mathcal{K}_{2})$ has as a subcategory, the Kleene-Vesley topos, $\mathcal{KV}$, which is defined as the relative realizability topos $\mathbf{RT}(\mathcal{K}_{2}^{\mathrm{rec}},\mathcal{K}_{2})$. See [33, Section 4.5] for more details.

We can embed subspaces of $\mathbb{R}^{n}$ into $\mathbf{RT}(\mathcal{K}_{2})$. A subspace of $\mathbb{R}^{n}$ is in particular a countably based $T_{0}$-space, which Bauer showed in [3] embed into $\mathbf{PER}(\mathcal{K}_{2})$, which in turn embeds into $\mathbf{RT}(\mathcal{K}_{2})$. Note however, that for the special case of subspaces of $\mathbb{R}^{n}$, we can more explicitly describe the embedding into $\mathbf{Asm}(\mathcal{K}_{2})$. Given a subspace $X$ of $\mathbb{R}^{n}$, we take the underlying set of the assembly to be $X$ itself, and we define the existence predicate, $E$, by taking $E(x)$ to be the set of (functions encoding) Cauchy sequences of rationals that converge to $x$, for each $x\in X$.

Hence the endpoint inclusion into the topological interval $\delta_{0}\colon 1\rightarrow[0,1]$, can be viewed as a map in $\mathbf{RT}(\mathcal{K}_{2})$. Moreover, since the map is evidently computable, it in fact lies in the subcategory $\mathcal{KV}$.

Definition 8.3**.**

We say a map in $\mathcal{KV}$ is a computable Hurewicz fibration if it has the fibred right lifting property against the following (trivial) family of maps.

[TABLE]

Note that since this is the fibred right lifting property, it is equivalent to having the right lifting property against the map $\delta_{0}\times X\colon X\rightarrow X\times[0,1]$, for every object $X$ of $\mathcal{KV}$. This justifies the name computable Hurewicz fibration, by analogy with Hurewicz fibrations in topology.

Theorem 8.4**.**

There is an awfs on $\mathcal{KV}$ where the maps that admit the structure of a right map are precisely the computable Hurewicz fibrations.

Proof.

It suffices to show that $\mathcal{KV}$ is a $\Pi W$-pretopos and satisfies $\mathbf{WISC}$. Van den Berg showed in [30] that this is the case for internal realizability toposes, as long as it holds in the background. However, Birkendal and Van Oosten showed in [4] that relative realizability toposes can be viewed as internal realizability toposes in $\mathbf{Set}^{\mathbf{2}}$, so $\mathcal{KV}$ is indeed a $\Pi W$-pretopos satisfying $\mathbf{WISC}$. We can now apply corollary 6.12. ∎

8.3 Cubical Assemblies

We will construct a category of internal presheaves in $\mathbf{Asm}(\mathcal{K}_{1})$ which we will call the category of cubical assemblies, which will be a realizability variant of the category of cubical sets defined by Cohen, Coquand, Huber and Mörtberg in [7]. The definitions of Kan trivial fibration and fibration are based on the presentation in [28, Section 7.5.4].

First, note that we can view the free de Morgan algebra on a countable set $\mathbb{A}$ as follows. We write $\mathbf{dM}_{0}(\mathbb{A})$ for the set of strings in the language of de Morgan algebras with constants from $\mathbb{A}$. Then $\mathbf{dM}(\mathbb{A})$ is the quotient of $\mathbf{dM}_{0}(\mathbb{A})$ by the appropriate equalities corresponding the de Morgan algebra axioms. We write $\phi\equiv\psi$ if $\phi$ and $\psi$ are words that are identified in $\mathbf{dM}(\mathbb{A})$. Clearly there is a Gödelnumbering of $\mathbf{dM}_{0}(\mathbb{A})$. Given $\phi\in\mathbf{dM}_{0}(A)$, we write the corresponding Gödelnumber as $\ulcorner\phi\urcorner$.

We define an internal category in assemblies as follows. We take the underlying small category to be the same as for CCHM cubical sets. That is, the full subcategory of the Kleisli category on $\mathbf{dM}$ with objects the finite subsets of $\mathbb{A}$. We then need to define existence predicates $E_{0}$ and $E_{1}$ for the objects and morphisms. Given a finite subset $A$ of $\mathbb{A}$, we define $E_{0}(A)$ to consist of lists $\langle a_{1},\ldots,a_{n}\rangle$ such that $A=\{a_{1},\ldots,a_{n}\}$. Given a morphism $\theta\colon A\rightarrow B$, we define $E_{1}(\theta)$ to consist of triples $\langle d,c,e\rangle$, where $d$ and $c$ are codes for the domain and codomain, and $e$ tracks the function $A\rightarrow\mathbf{dM}(B)$ underlying $\theta$. That is, given $a\in A$, $\theta\ulcorner a\urcorner$ is defined and equal to $\ulcorner\phi\urcorner$ for some $\phi$ such that $\phi\equiv\theta(a)$. We call this internal category the cube category.

We now define the category of cubical assemblies to be the category of diagrams for the cube category. Note that the forgetful functor $\Gamma\colon\mathbf{Asm}(\mathcal{K}_{1})\rightarrow\mathbf{Set}$ extends to a functor from cubical assemblies to cubical sets.

We define an interval object $\mathbb{I}$ as the following cubical assembly. The underlying cubical set is the same as the interval in CCHM cubical sets. Namely, we take $\mathbb{I}(A)$ to be $\mathbf{dM}(A)$. We define the existence predicate on $\mathbb{I}(A)$ by taking $E([\phi])$ to be the set consisting of $\ulcorner\psi\urcorner$ for $\psi$ such that $\psi\equiv\phi$.

We define the face lattice, $F$, to be the quotient of $\mathbb{I}$ by the following equivalence relation. We define $[\phi]\sim[\psi]$ when $\phi\equiv 1\Leftrightarrow\psi\equiv 1$ holds in cubical assemblies. In $\mathbf{Asm}(\mathcal{K}_{1})$, this says that for $[\phi],[\psi]\in F(A)$, $[\phi]\sim[\psi]$ when for every $\theta\colon A\rightarrow B$ in the cube category, $F(\theta)(\phi)\equiv 1\Leftrightarrow F(\theta)(\psi)\equiv 1$.

As Coquand et al remark in [7, Section 3], free de Morgan algebras have decidable equality. In fact the equality in $\mathbf{dM}(A)$ is uniformly computably decidable over all finite subsets $A$ of $\mathbb{A}$, and so $\mathbb{I}$ has decidable equality in $\mathbf{Asm}(\mathcal{K}_{1})$.

We will check that the map $\top\colon 1\rightarrow F$ has decidable image. Note that since $\mathbf{Asm}(\mathcal{K}_{1})$ does not have effective quotients in general we need to be a little careful.

Suppose we are given an element of $F(A)$ of the form $[\phi]$. By decidability of $\equiv$ we know that $\phi\equiv 1$ or $\phi\not\equiv 1$. In the former case we clearly have $\phi\sim 1$ and so $[\phi]=1$. We now show that in the latter case $[\phi]\neq 1$. Just using the fact that the quotient is a coequalizer and again that $\mathbb{I}$ has decidable equality we can define a map $f\colon F(A)\rightarrow 2$ such that $f([\psi])=1$ when $\psi\equiv 1$ and $f([\psi])=0$ when $\psi\not\equiv 1$. But then $f([\phi])=0$ and $f(1)=1$, so we can deduce $[\phi]\neq 1$.

In fact one can deduce that this particular quotient is effective, but we don’t need that here.

Therefore, by theorem 6.14 there exists a (strongly fibred) awfs cofibrantly generated by the following family of maps, which we refer to as the awfs of Kan cofibrations and trivial fibrations.

[TABLE]

Finally note that the Leibniz product $\delta_{0}\hat{\times}\top$, is the subobject of $F\times\mathbb{I}$, which at $A$ consists of $([\phi],[\psi])$ in $F(A)\times\mathbb{I}(A)$ such that $\phi\equiv 1$ or $\psi\equiv 0$666The easiest way to show this is simply to verify directly that this definition satisfies the universal property of the pushout. In fact one can show that this map is a cofibration, but we won’t cover this in more detail here.. It follows that $\delta_{0}\hat{\times}\top$ is also locally decidable. It follows again by theorem 6.14 that there is a (fibred) awfs cofibrantly generated by the family of maps below, which we refer to as the awfs of Kan trivial cofibrations and fibrations.

[TABLE]

9 Conclusion

9.1 Comparison With Existing Constructions of Higher Inductive Type

As remarked in the introduction, $W$-types with reductions may be a special cases of free algebra over varieties (as defined by Blass in [5]), and of QIITs, as developed by Altenkirch, Capriotti, Dijkstra and Forsberg in [1]. We were able to show initial algebras can be constructed in a wide variety of categories. For algebraic varieties, Blass observed that initial algebras can be constructed in any topos with natural number object satisfying the internal axiom of choice, which is a much smaller class than the one we considered. However, the construction in section 3 is fairly flexible, and may lead to a refinement of Blass’ result, as in the conjecture below.

Conjecture 9.1**.**

Free algebras for varieties exist in any $\Pi W$-pretopos that satisfies $\mathbf{WISC}$.

In fact this has already been conjectured in [30, Section 8], where the question is attributed to Alex Simpson.

The question of when QIITs can be constructed remains open, although in loc. cit., Altenkirch et al do make some progress towards a solution. The technique used in section 3 might also be helpful here.

In [15], Lumsdaine and Shulman give a very general approach to the semantics of higher inductive types in homotopy type theory. Although the set up is quite different, the problem of constructing the higher inductive types turns out to be quite similar to the problems we saw in this paper. For this Lumsdaine and Shulman use some general transfinite constructions due to Kelly [14]. Unfortunately this approach is not suitable for the examples we consider here, as we discuss further in the next section.

9.2 Other Approaches to the Construction of Initial Algebras

In section 3.2 we gave a relatively direct proof, in place of an application of existing results from literature. The reader might wonder why this is the case.

A commonly used approach to constructing initial algebras is to use a transfinite construction. Following Garner’s small object argument [11], we might try to use one of the general theorems of Kelly from [14]. However, such constructions have the disadvantage that they make essential use of transfinite colimits of ordinal indexed sequences. This means they will not work for general elementary toposes, which need not be cocomplete. This is critical here, because our examples are based on realizability toposes, which are certainly not cocomplete.

It is also difficult to simply carry out a similar transfinite construction internally in the $\Pi W$-pretopos, since it is unclear how to formulate ordinals in the internal language in way that the set theoretic arguments can be easily transferred.

Another possible approach would be to use an internal version of the special adjoint functor theorem as developed by Day in [8] or Paré and Schumacher in [20]. In fact Paré and Schumacher indicate in [20, Section V.2] how their result can be used to construct free algebras of certain endofunctors. However, it is unclear how to show that the pointed endofunctors here satisfy the necessary conditions to apply the internal special adjoint functor theorem. Indeed in the paragraph at the end of loc cit. Paré and Schumacher remark that the addition of equations makes things more problematic and suggest using in this case the more powerful results of Rosebrugh in [24]. However, Rosebrugh’s proofs apply only to internal toposes of sheaves inside toposes satisfying the axiom of choice. This again would eliminate our examples based on realizability. Blass proved in [5] that some form of the axiom of choice really is necessary for Rosebrugh’s result to hold, although like with our results it may be possible to adapt Rosebrugh’s proofs to use a weak form of choice such as $\mathbf{WISC}$. There is also the issue that the techniques of Rosebrugh and of Paré and Schumacher make heavy use of impredicative notions such as the subobject classifier and the assumptions of well poweredness and cowell poweredness, and will thus not apply to $\Pi W$-pretoposes without further work.

9.3 Directions for Future Work

9.3.1 Is Choice Really Necessary?

In our construction of arbitrary $W$-types with reductions in a $\Pi W$-pretopos we relied on the axiom $\mathbf{WISC}$. It’s natural to ask whether $\mathbf{WISC}$ was really necessary, or whether there’s a way to construct $W$-types with reductions without using any choice.

We saw in section 5 that using classical logic we can derive all $W$-types with reductions from $W$-types without using any choice. It might be possible to generalise this result to all categories of internal presheaves in a boolean topos.

However, we conjecture that in general there are toposes where some form of choice is strictly necessary, even just for monic polynomials with reductions.

Conjecture 9.2**.**

There is a topos with natural number object with a monic polynomial with reductions that does not have an initial algebra. 2. 2.

It is consistent with $\mathbf{IZF}$ that there is a monic polynomial with reductions in the category of sets that does not have an initial algebra.

Note that by theorem 3.19 we know that $\mathbf{WISC}$ has to fail in the above conjecture. Also by theorem 4.16 we know that the topos cannot be a category of internal presheaves over a boolean topos (and in particular cannot be boolean itself).

9.3.2 Applications to the Semantics of Homotopy Type Theory

The main aim of this work is towards the semantics of homotopy type theory and in particular better understanding and generalising the cubical set model of type theory. We have already seen one aspect of this, which is that $W$-types with reductions can be used to construct awfs’s where $R$-algebra structures correspond to Kan filling operators (which in turn are used in the interpretation of dependent types). We note that in fact we don’t need all $W$-types with reductions in order to do this, but only those where the map $f\circ k$ in (1) is a cofibration (assuming cofibrations are closed under coproduct and pullback). We’ll refer to such polynomials with reductions as cofibrant.

Cofibrant $W$-types with reductions may also have further applications to the semantics of type theory. In [7], Coquand et al implement higher inductive types by freely adding an $\mathsf{hcomp}$ operator to a type. This can be seen as a kind of weak fibrant replacement that can be phrased as a cofibrantly generated rawfs, as we developed in section 6.3. An important point is that this construction is stable under pullback, which corresponds to our notion of strongly fibred rawfs. We again notice that we only need cofibrant $W$-types with reductions.

The author hopes to develop these ideas further in a future paper. The following conjecture illustrates the kind of result expected.

Conjecture 9.3**.**

Let $\mathbb{C}$ be a topos with natural number object. Suppose further that $\mathbb{C}$ satisfies all of the axioms considered by Orton and Pitts in [19]. Suppose further that initial algebras exist for all cofibrant polynomials with reductions. Then pushouts, $n$-truncations, set-quotients, suspensions and $n$-spheres can be implemented in the resulting CwF.

9.3.3 Algebraic Model Structures on Realizability Toposes

In section 8 we saw three examples of awfs’s based on realizability. It’s natural to ask whether these in fact form part of algebraic model structures (as defined by Riehl in [22]). We conjecture that in fact this is possible.

Firstly, by generalising results by Sattler in [25] the author expects it will be possible to prove the following conjectures.

Conjecture 9.4**.**

The two awfs’s in section 8.1 form part of an algebraic model structure on the effective topos.

Conjecture 9.5**.**

The two awfs’s in section 8.3 form part of an algebraic model structure on the category of cubical assemblies.

The status of the example in $\mathcal{KV}$ is less clear, but by analogy with the well known model structure on topological spaces by Strøm [27], the following conjecture might also be true.

Conjecture 9.6**.**

The awfs in section 8.2 forms the trivial cofibrations and fibrations part of an algebraic model structure on the Kleene-Vesley topos.

Acknowledgements

I’m grateful to Benno van den Berg for many helpful discussions and suggestions while developing this work.