\documentclass[11pt,reqno]{amsart}
\usepackage[a4paper,textwidth=150mm,textheight=228mm,centering]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{mathrsfs}
\usepackage{tikz-cd}
\usetikzlibrary{calc,fit,arrows.meta}
\usepackage{enumitem}
\setlist{itemsep=1pt,topsep=3pt,parsep=0pt}
\setlist[enumerate]{font=\upshape}
\makeatletter\@beginparpenalty=\@M\makeatother
\makeatletter
\renewcommand\section{\@startsection{section}{1}{\z@}{2.5\linespacing\@plus\linespacing}{1.2\linespacing}{\normalfont\Large\bfseries\def\@secnumfont{\bfseries}}}
\renewcommand\subsection{\@startsection{subsection}{2}{\z@}{.9\linespacing\@plus.4\linespacing}{.35\linespacing}{\normalfont\large\bfseries\def\@secnumfont{\bfseries}}}
\def\l@section{\@tocline{1}{0pt}{0pt}{}{\bfseries}}
\def\l@subsection{\@tocline{2}{0pt}{1.5pc}{5pc}{}}
\makeatother
\usepackage{booktabs,array,tabularx}
\usepackage{placeins}
\usepackage{float}
\setlength{\belowbottomsep}{4pt}
\usepackage{microtype}
\usepackage[colorlinks=true,linkcolor={blue!50!black},citecolor={green!40!black},urlcolor={blue!50!black}]{hyperref}

\numberwithin{equation}{section}
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{example}[theorem]{Example}
\newtheorem{construction}[theorem]{Construction}
\newtheorem{convention}[theorem]{Convention}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\newcommand{\cat}[1]{\mathscr{#1}}
\newcommand{\Span}{\mathbb{S}\mathrm{pan}}
\newcommand{\Cat}{\mathbf{Cat}}
\newcommand{\CAT}{\mathbf{CAT}}
\newcommand{\Set}{\mathrm{Set}}
\DeclareRobustCommand{\stfill}[1]{\raisebox{0.12ex}{\setlength{\fboxsep}{1.15pt}\colorbox{black}{\makebox[1.25ex]{\normalfont\sffamily\scriptsize\bfseries\color{white}#1}}}}
\DeclareRobustCommand{\stK}{\stfill{K}}
\DeclareRobustCommand{\stP}{\stfill{P}}
\newcommand{\yu}{\mathrm{y}}
\DeclareMathOperator{\src}{src}
\DeclareMathOperator{\tgt}{tgt}
\newcommand{\op}{\mathrm{op}}
\newcommand{\Tel}{\mathbf{Tel}}
\newcommand{\fSpan}{\mathbf{fSpan}}
\newcommand{\coKl}{\mathrm{co}\mathbb{K}\mathrm{l}}
\newcommand{\SpanC}{\mathbf{Span}(\cat C)}
\newcommand{\Gext}{\mathrm{P}}
\newcommand{\EM}{\mathbf{EM}}
\newcommand{\Kl}{\mathbb{K}\mathrm{l}}
\newcommand{\Mon}{\mathbf{Mon}}
\newcommand{\lto}{\mathrel{\ooalign{$\rightarrow$\cr\hidewidth$\mapstochar\mkern3mu$\hidewidth\cr}}}
\newcommand{\Dcls}{\mathsf{D}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\sq}{\mathbin{;}}
\newcommand{\semiglyph}[1]{\tikz[baseline=-0.3ex,line join=round,x=1ex,y=1ex]{%
  \path[#1] (0,0.78) circle (0.3);
  \path[#1] (0.32,0.0) arc (0:180:0.32) .. controls (-0.32,-0.24) and (-0.08,-0.3) .. (-0.02,-0.3)
     .. controls (-0.02,-0.52) and (-0.14,-0.76) .. (-0.36,-0.95)
     .. controls (0.08,-0.84) and (0.32,-0.5) .. (0.32,0.0) -- cycle;}}
\newcommand{\wsemi}{\mathbin{\semiglyph{fill=white,draw=black,line width=0.35pt}}}
\medmuskip=4mu plus 2mu minus 1mu

\tikzset{
  sd/.style={x=0.5cm,y=0.5cm,line width=0.8pt,baseline={#1*0.5cm-0.25em}},
  dotn/.style={circle,fill=black,inner sep=0pt,minimum size=4.2pt},
  boxn/.style={draw,rectangle,inner sep=0pt,line width=0.6pt,fill=white},
  lab/.style={font=\scriptsize,inner sep=1pt,text height=1.5ex,text depth=0.35ex}
}
\newcommand{\sdlab}[2]{\node[lab,anchor=south] at (#1,0) {$#2$};}
\newcommand{\sdwire}[1]{\tikz[sd=-1.2]{\draw (0,0) -- (0,-2.4); \sdlab{0}{#1}}}
\newcommand{\sdmul}{\tikz[sd=-1.2]{
  \coordinate (m) at (0.5,-1.2);
  \draw (0,0) to[out=-90,in=120] (m);
  \draw (1,0) to[out=-90,in=60] (m);
  \draw (m) -- (0.5,-2.4);
  \node[dotn] at (m) {};
  \sdlab{0}{P}\sdlab{1}{Q}}}
\newcommand{\sdunit}{\tikz[sd=-1.2]{
  \coordinate (u) at (0,-1.2);
  \draw (u) -- (0,-2.4);
  \node[dotn,label={[lab]right:$I$}] at (u) {};}}
\newcommand{\sdunitL}{\tikz[sd=-1.2]{
  \coordinate (u) at (0,-0.7); \coordinate (m) at (0.5,-1.5);
  \draw (u) to[out=-90,in=120] (m);
  \draw (1,0) -- (1,-0.7) to[out=-90,in=60] (m);
  \draw (m) -- (0.5,-2.4);
  \node[dotn,label={[lab]left:$I$}] at (u) {}; \node[dotn] at (m) {};
  \sdlab{1}{P}}}
\newcommand{\sdunitR}{\tikz[sd=-1.2]{
  \coordinate (u) at (1,-0.7); \coordinate (m) at (0.5,-1.5);
  \draw (0,0) -- (0,-0.7) to[out=-90,in=120] (m);
  \draw (u) to[out=-90,in=60] (m);
  \draw (m) -- (0.5,-2.4);
  \node[dotn,label={[lab]right:$I$}] at (u) {}; \node[dotn] at (m) {};
  \sdlab{0}{P}}}
\tikzset{tel/.style={fill=black,fill opacity=0.1,draw=none},teledge/.style={draw=black!55,line width=0.3pt}}
\newcommand{\telband}[4]{\path[tel] (#1,#3) rectangle (#2,#4); \draw[teledge] (#1,#3) -- (#1,#4); \draw[teledge] (#2,#3) -- (#2,#4);}
\tikzset{spl/.style={line width=0.55pt},spid/.style={double,double distance=1.1pt,line width=0.3pt,shorten <=1.8pt,shorten >=1.8pt},sptc/.style={double,double distance=1.1pt,line width=0.35pt,-{Implies[length=2pt]}},spap/.style={circle,fill=black,inner sep=0pt,minimum size=2.6pt},spft/.style={circle,fill=white,draw,line width=0.5pt,inner sep=0pt,minimum size=2.6pt},spstg/.style={fill=black!14}}
\newcommand{\spanpyr}[3]{%
 \foreach \j in {0,...,#1} {\pgfmathtruncatemacro\m{#1-\j}\foreach \i in {0,...,\m} \coordinate (P-\j-\i) at ({\i+\j/2},{#2*\j});}%
 \pgfmathtruncatemacro\nn{#1-1}%
 \ifnum#3=1 \foreach \i in {0,...,\nn} {\pgfmathtruncatemacro\ii{\i+1}\fill[spstg] (P-0-\i)--(P-1-\i)--(P-0-\ii)--cycle; \draw[spid] (P-0-\i)--(P-0-\ii);}\fi
 \foreach \j in {1,...,#1} {\pgfmathtruncatemacro\m{#1-\j}\pgfmathtruncatemacro\jj{\j-1}\foreach \i in {0,...,\m} {\pgfmathtruncatemacro\ii{\i+1}\draw[spl] (P-\jj-\i)--(P-\j-\i)--(P-\jj-\ii);}}%
 \foreach \j in {1,...,#1} {\pgfmathtruncatemacro\m{#1-\j}\foreach \i in {0,...,\m} \node[spap] at (P-\j-\i) {};}%
 \foreach \i in {0,...,#1} \node[spft] at (P-0-\i) {};}
\newcommand{\spantri}[4]{\coordinate (T) at ({#1+#2/2},{#2*#3});%
 \ifnum#4=1 \fill[spstg] (#1,0)--(T)--({#1+#2},0)--cycle; \draw[spid] (#1,0)--({#1+#2},0);\fi
 \draw[spl] (#1,0)--(T)--({#1+#2},0); \node[spap] at (T) {}; \node[spft] at (#1,0) {}; \node[spft] at ({#1+#2},0) {};}
\newcommand{\telopen}[4]{\telband{#1}{#2}{#3}{#4}\draw[teledge] (#1,#3) -- (#2,#3);}
\newcommand{\sdboxzero}{\tikz[sd=-1.2]{
  \telopen{-0.4}{0.4}{-0.3}{-0.8}
  \node[boxn,fit={(-0.4,-0.8) (0.4,-1.6)}] (b) {}; \node at (b.center) {$a$};
  \draw (b.south) -- (0,-2.4);}}
\newcommand{\sdboxone}{\tikz[sd=-1.2]{
  \telopen{-0.4}{0.4}{-0.3}{-0.8}
  \node[boxn,fit={(-0.4,-0.8) (0.4,-1.6)}] (b) {}; \node at (b.center) {$a$};
  \draw (0,0) -- (b.north); \draw (b.south) -- (0,-2.4);
  \sdlab{0}{P}}}
\newcommand{\sdboxtwo}{\tikz[sd=-1.2]{
  \telopen{-0.4}{1.4}{-0.3}{-0.8}
  \node[boxn,fit={(-0.4,-0.8) (1.4,-1.6)}] (b) {}; \node at (b.center) {$a$};
  \foreach \x in {0,1} \draw (\x,0) -- (b.north -| \x,0);
  \draw (b.south) -- (0.5,-2.4);
  \sdlab{0}{P}\sdlab{1}{Q}}}
\newcommand{\sdassocL}{\tikz[sd=-1.4]{
  \coordinate (m1) at (0.5,-0.9); \coordinate (m2) at (1.25,-1.9);
  \draw (0,0) to[out=-90,in=120] (m1);
  \draw (1,0) to[out=-90,in=60] (m1);
  \draw (m1) to[out=-90,in=120] (m2);
  \draw (2,0) -- (2,-0.9) to[out=-90,in=60] (m2);
  \draw (m2) -- (1.25,-2.8);
  \node[dotn] at (m1) {}; \node[dotn] at (m2) {};
  \sdlab{0}{P}\sdlab{1}{Q}\sdlab{2}{R}}}
\newcommand{\sdassocR}{\tikz[sd=-1.4]{
  \coordinate (m1) at (1.5,-0.9); \coordinate (m2) at (0.75,-1.9);
  \draw (1,0) to[out=-90,in=120] (m1);
  \draw (2,0) to[out=-90,in=60] (m1);
  \draw (0,0) -- (0,-0.9) to[out=-90,in=120] (m2);
  \draw (m1) to[out=-90,in=60] (m2);
  \draw (m2) -- (0.75,-2.8);
  \node[dotn] at (m1) {}; \node[dotn] at (m2) {};
  \sdlab{0}{P}\sdlab{1}{Q}\sdlab{2}{R}}}
\newcommand{\sdcomb}{\tikz[sd=-2]{
  \coordinate (m1) at (2.5,-0.95); \coordinate (m2) at (1.75,-2); \coordinate (m3) at (0.875,-3.05);
  \draw (2,0) to[out=-90,in=120] (m1);
  \draw (3,0) to[out=-90,in=60] (m1);
  \draw (1,0) -- (1,-0.95) to[out=-90,in=120] (m2);
  \draw (m1) to[out=-90,in=60] (m2);
  \draw (0,0) -- (0,-2) to[out=-90,in=120] (m3);
  \draw (m2) to[out=-90,in=60] (m3);
  \draw (m3) -- (0.875,-4);
  \node[dotn] at (m1) {}; \node[dotn] at (m2) {}; \node[dotn] at (m3) {};
  \sdlab{0}{P_0}\sdlab{1}{P_1}\sdlab{2}{P_2}\sdlab{3}{P_3}}}
\newcommand{\sdmuL}{\tikz[sd=-2.3]{
  \path[tel] (-1.2,0) rectangle (1.2,-2.9); \path[tel] (-0.6,0) rectangle (0.6,-1.2);
  \draw[teledge] (-1.2,0) -- (-1.2,-2.9); \draw[teledge] (1.2,0) -- (1.2,-2.9);
  \draw[teledge] (-0.6,0) -- (-0.6,-1.2); \draw[teledge] (0.6,0) -- (0.6,-1.2);
  \node[boxn,fit={(-1.2,-1.2) (1.2,-1.9)}] (m) {}; \node at (m.center) {$\mu$};
  \node[boxn,fit={(-1.2,-2.9) (1.2,-3.6)}] (b) {}; \node at (b.center) {$a$};
  \draw (0,0) -- (m.north); \draw (m.south) -- (b.north); \draw (b.south) -- (0,-4.6);
  \sdlab{0}{\cat M}}}
\newcommand{\sdmuR}{\tikz[sd=-2.3]{
  \path[tel] (-1.2,0) rectangle (1.2,-2.9); \path[tel] (-0.6,0) rectangle (0.6,-1.2);
  \draw[teledge] (-1.2,0) -- (-1.2,-2.9); \draw[teledge] (1.2,0) -- (1.2,-2.9);
  \draw[teledge] (-0.6,0) -- (-0.6,-1.2); \draw[teledge] (0.6,0) -- (0.6,-1.2);
  \node[boxn,fit={(-0.6,-1.2) (0.6,-1.9)}] (b1) {}; \node at (b1.center) {$a$};
  \node[boxn,fit={(-1.2,-2.9) (1.2,-3.6)}] (b2) {}; \node at (b2.center) {$a$};
  \draw (0,0) -- (b1.north); \draw (b1.south) -- (b2.north); \draw (b2.south) -- (0,-4.6);
  \sdlab{0}{\cat M}}}
\newcommand{\sdbigbox}{\tikz[sd=-2]{
  \telopen{-0.4}{3.9}{-0.5}{-1.6}
  \node[boxn,fit={(-0.4,-1.6) (3.9,-2.4)}] (b) {}; \node at (b.center) {$a$};
  \foreach \x in {0,1,2.5,3.5} \draw (\x,0) -- (b.north -| \x,0);
  \draw (b.south) -- (1.75,-4);
  \sdlab{0}{P_0}\sdlab{1}{P_1}\sdlab{2.5}{P_2}\sdlab{3.5}{P_3}}}
\tikzset{stw/.style={line width=1.6pt,black!30}}
\tikzset{dotw/.style={circle,fill=white,draw,line width=0.6pt,inner sep=0pt,minimum size=4.6pt}}
\newcommand{\sdchi}[2]{\node[boxn,minimum width=3.7mm,minimum height=3.4mm] (#1) at (#2) {$\scriptstyle\chi$};}
\newcommand{\sdSigChi}{\tikz[x=5.4mm,y=4.7mm,line width=0.6pt,baseline={([yshift=-.5ex]current bounding box.center)}]{
 \begin{scope}[sw/.style={line width=1.8pt,black!30},sbx/.style={draw,fill=white,font=\scriptsize,inner sep=1pt,minimum height=3.2mm,minimum width=3.6mm}]
 \telband{-0.07}{3.07}{-2.85}{-3.71}
 \foreach \x/\l in {0.5/F_0,1.5/F_1,2.5/F_2} {\node[font=\scriptsize] at (\x,-2.5) {$\l$}; \draw[sw] (\x,-2.85)--(\x,-3.76);}
 \node[sbx,minimum width=17mm] (S) at (1.5,-4.05) {$\Sigma$};
 \node[sbx] (X) at (1.5,-5.55) {$\chi$};
 \draw[sw] (S.south)--(X.north); \draw (X.south)--(1.5,-6.75);
 \end{scope}}}
\newcommand{\sdTelChiA}{\tikz[x=5.4mm,y=4.7mm,line width=0.6pt,baseline={([yshift=-.5ex]current bounding box.center)}]{
 \begin{scope}[sw/.style={line width=1.8pt,black!30},sbx/.style={draw,fill=white,font=\scriptsize,inner sep=1pt,minimum height=3.2mm,minimum width=3.6mm}]
 \telband{-0.07}{3.07}{-2.85}{-5.21}
 \foreach \x/\l/\i in {0.5/F_0/0,1.5/F_1/1,2.5/F_2/2} {\node[font=\scriptsize] at (\x,-2.5) {$\l$}; \node[sbx] (c\i) at (\x,-4.05) {$\chi$}; \draw[sw] (\x,-2.85)--(c\i.north); \draw (c\i.south)--(\x,-5.26);}
 \node[sbx,minimum width=17mm] (A) at (1.5,-5.55) {$a$};
 \draw (A.south)--(1.5,-6.75);
 \end{scope}}}
\title[The Grothendieck Construction, Telescopes and Contextads]{The Grothendieck Construction between\\ the Telescope Monad and Contextads}
\author{Kotaro Kamiya}
\date{October 2026}

\raggedbottom
\hyphenpenalty=1000
\exhyphenpenalty=1000
\widowpenalty=10000
\clubpenalty=10000
\displaywidowpenalty=10000
\makeatletter
\newcommand\leitfadenhead{\par\@startsection{}\@M\z@{\linespacing\@plus\linespacing}{.5\linespacing}{\centering\scshape}{Dependencies}\par}
\makeatother

\begin{document}

\begin{abstract}
A telescope is a list of stages in which each stage is a family indexed over the Grothendieck construction of the previous ones. The telescope monad stacks stages as the free-monoid 2-monad on spans, whereas a contextad collapses two stages into one by a dependent sum. This paper derives both from the span of single stages, and thereby explains why the strict algebras of the telescope monad are contextads. The link is the Grothendieck extension of a span. Because it is monoidal and preserves coproducts, it turns the telescopes into the free monad on the extension of the span of stages and the stage contextad into the Grothendieck monad, whose Kleisli arrows are the contextful arrows. The main theorem identifies the stage contextad with the pseudo-algebra of the telescope monad transported from the display contextad. Its structure map is the dependent sum, which the extension turns into the iterated multiplication of the Grothendieck monad.
\end{abstract}

\maketitle
\vfill
\begin{center}
\begin{tikzpicture}[x=9.5mm,y=9.5mm,
 lb/.style={font=\scriptsize,inner sep=1pt},
 mb/.style={draw=black!70,rounded corners=2pt,font=\footnotesize,align=center,fill=black!4,inner sep=3.5pt,text width=47mm,minimum height=10mm},
 mp/.style={->,thick,shorten <=2mm,shorten >=2mm}]
\def\h{0.866}
\begin{scope}[shift={(4.85,5.0)},scale=1.3]
 \spantri{0}{1}{\h}{1} \node[lb,above=2pt] at (T) {$\int S$}; \node[lb,below=2pt] at (0,0) {$\cat C$}; \node[lb,below=2pt] at (1,0) {$\cat C$};
 \node[lb,left=1pt] at (0.25,0.43) {$p$}; \node[lb,right=1pt] at (0.75,0.43) {$\odot$}; \draw[sptc] (0.64,0.22)--(0.36,0.22); \node[lb] at (0.5,0.4) {$d$};
\end{scope}
\node[mb] at (5.5,7.75) {\textbf{Grothendieck construction}\\ the span of stages $\int S$};
\begin{scope}[shift={(0,0)}]
 \spanpyr{3}{\h}{1} \node[lb,above=2pt] at (P-3-0) {$(\int S)^{\ltimes3}$};
\end{scope}
\node[mb,fill=black!16] at (1.5,-1.05) {\textbf{Telescope monad} $\Tel$\\ stacks stages, $\Tel(\int S)=\coprod_n(\int S)^{\ltimes n}$};
\begin{scope}[shift={(6.6,0)}]
 \spanpyr{2}{\h}{1} \node[lb,above=2pt] at (P-2-0) {$(\int S)^{\ltimes2}$};
 \draw[mp] (2.05,0.75)--node[lb,above]{$\wsemi$}(3.25,0.75);
 \begin{scope}[shift={(3.3,0)}] \spantri{0}{2}{\h}{1} \node[lb,above=2pt] at (T) {$\int S$}; \end{scope}
\end{scope}
\node[mb,fill=black!16] at (9.25,-1.05) {\textbf{Stage contextad}\\ collapses two stages by $\wsemi$};
\draw[mp] (4.75,5.2)--node[lb,above left]{stack, free}(2.3,3.2);
\draw[mp] (6.55,5.2)--node[lb,above right]{collapse, $\wsemi$}(9.05,2.5);
\draw[<->,thick,shorten <=2mm,shorten >=2mm] (3.3,1.1)--node[lb,above]{$\Sigma$, the iterated $\wsemi$}node[lb,below]{algebras}(6.3,1.1);
\end{tikzpicture}

{\footnotesize The pictures are pasting diagrams of spans in $\CAT$. Black dots are categories, and white dots are the base $\cat C$. Edges are functors and run downwards. Diamonds are pullbacks. Grey is the display 2-cell. $\ltimes$ composes spans.}
\end{center}
\vfill

\clearpage

\setcounter{tocdepth}{2}
{\small\tableofcontents}
\vfill
\leitfadenhead
\begin{center}
\resizebox{0.7\textwidth}{!}{\begin{tikzpicture}[>=Stealth,x=1cm,y=1cm,
 box/.style={draw,rounded corners=2pt,font=\small,align=center,fill=white,text width=35mm,minimum height=11mm,inner sep=3pt},
 thk/.style={box,very thick},
 band/.style={fill=black!5,draw=none,rounded corners=3pt},
 slab/.style={font=\footnotesize\bfseries,black!65},
 dep/.style={->,thick,rounded corners=4pt}]
 \fill[band] (-0.75,1.25) rectangle (12.75,-3.35);
 \fill[band] (-0.75,-3.85) rectangle (12.75,-8.25);
 \fill[band] (-0.75,-8.75) rectangle (12.75,-10.95);
 \node[slab,anchor=north west] at (-0.65,1.18) {\S\ref*{sec:prelim} Preliminaries};
 \node[slab,anchor=north east] at (12.65,-3.92) {\S\ref*{sec:tele} The Grothendieck monad};
 \node[slab,anchor=south west] at (-0.65,-10.9) {\S\ref*{sec:main} The dependent sum as a transported algebra};
 \node[box] (TM) at (1.5,-0.1)   {\stK\ Telescope monad\\Def.~\ref*{def:telemonad}, Cor.~\ref*{cor:alg}};
 \node[box] (FC) at (6,-0.1)     {\stK\ Spans, free monoids\\Prop.~\ref*{prop:monad}, Lemma~\ref*{lem:transport}};
 \node[box] (CX) at (10.5,-0.1)  {\stK\ Contextads\\Def.~\ref*{def:ctxd}, \ref*{def:dispctx}};
 \node[box] (CO) at (10.5,-2.3)  {\stK\ Comprehension\\Def.~\ref*{def:comp}, Lemma~\ref*{lem:adjeq}};
 \node[box] (GE) at (5.2,-4.9)     {\stP\ Grothendieck extension\\Prop.~\ref*{prop:gext}};
 \node[box] (G1) at (1.5,-7.1)   {\stP\ Telescopes as a free monad\\Prop.~\ref*{prop:freemonad}};
 \node[box] (G2) at (10.5,-7.1)  {\stP\ Stage contextad, Kleisli arrows\\Prop.~\ref*{prop:stagectx}, \ref*{prop:kleisli}};
 \node[thk] (MT) at (5.4,-9.85)    {\stP\ Dependent sum\\Thm.~\ref*{thm:main}, Prop.~\ref*{prop:klalg}};
 \draw[dep] (FC) -- (TM);
 \draw[dep] (TM) -- (G1);
 \draw[dep] (CX) -- (CO);
 \draw[dep] (CX.south west) -- (GE.north east);
 \draw[dep] (GE.south west) -- (G1.north east);
 \draw[dep] (GE.south east) -- (G2.north west);
 \draw[dep] (CO) -- (G2);
 \draw[dep] (CX.north) to[out=160,in=20] (TM.north);
 \draw[dep] (CO.west) -| ([xshift=8mm]G1.north);
 \draw[dep] (G1.south east) -- (MT.north west);
 \draw[dep] (G2.south west) -- (MT.north east);
 \node[font=\footnotesize,anchor=north] at (6,-11.15) {\stK~known, with the source in the text\qquad\stP~proved here};
\end{tikzpicture}}
\end{center}
\vfill

\clearpage

\section{Introduction}

A telescope is a list of stages in which each stage depends on the previous ones. The word goes back to de~Bruijn's Automath~\cite[Sec.~10.2]{Zuc75}, \cite{dB91}, where a telescope is an iterated dependent pair type, and the contexts of Cartmell~\cite{Car86} have the same shape. Categorically, a telescope is an iterated Grothendieck construction because each stage is an indexed family over the total category of the previous ones. In this form Palmgren built presheaf models of dependent types from iterated categories of elements. His category of telescopes has the functors over the base as morphisms, and Forssell observed that it is equivalent to the presheaf category~\cite[Sec.~1, 3]{Pal13}.

This paper separates the telescope technique from the setting to which it is applied, although its ingredients are known. A span of categories $\cat C\leftarrow\cat M\rightarrow\cat C$ is drawn as a triangle on two feet, and composing spans then stacks triangles into pyramids. Fix $S\colon\cat C^{\op}\to\CAT$ and a comprehension equivalence $\chi\colon\int S\to\cat M$, which is a comprehension category in the sense of Jacobs that is an equivalence onto the display maps $\cat M$. The Grothendieck construction then gives the \emph{span of stages} $\int S$, whose legs are $\chi\sq\mathrm{cod}$ and $\chi\sq\mathrm{dom}$. From this span the paper builds two structures. The \emph{telescope monad} $\Tel$ is the free-monoid 2-monad on spans, and it stacks stages. A \emph{contextad} of Capucci and Myers is a pseudomonoid in left fibrant spans, and its multiplication collapses two stages into one. Strict contextads are double categories, and by the free-monoid construction they are the algebras of $\Tel$ on left fibrant spans with normal cleavage. The \emph{stage contextad} is then the contextad on $\int S$ that is transported along $\chi$ from the display maps. Since both structures are built from the span of stages, this shared source explains why algebras of $\Tel$ are contextads, and the three form the triangle of the visual abstract. The \emph{Grothendieck extension} makes the triangle precise because it turns a span $\cat M$ into an endo-2-functor $\Gext_{\cat M}$ of indexed categories. In particular it turns the span of stages into $\int:=\Gext_{\int S}$, and it yields the following three results.
\begin{enumerate}[label=(\alph*),leftmargin=*]
\item \emph{Telescopes.} $\Gext_{\Tel(\int S)}$ is the free monad $\coprod_n\int^n$ on $\int$ by Proposition~\ref{prop:freemonad}.
\item \emph{Stage contextad.} Its extension is the Grothendieck monad $(\int,\eta^{\int},\mu^{\int})$ by Proposition~\ref{prop:kleisli}.
\item \emph{Dependent sum.} The transported structure map $\Sigma$ satisfies $\Gext_\Sigma\cong\coprod_n\mu^{(n)}$ by Theorem~\ref{thm:main}.
\end{enumerate}
The transport in (c) needs $\Tel$ as a pseudomonad on colax maps of spans, which Lemma~\ref{lem:telpseudo} provides.

The setting is formal because it only needs a display contextad on $\cat C$ in the sense of Definition~\ref{def:dispctx}. Its display maps are closed under pullback and composition, and it chooses squares between them. Since the category of elements of presheaves and the Grothendieck construction of indexed categories are comprehension equivalences, both are instances. Section~\ref{sec:prelim} collects the ingredients, and Section~\ref{sec:tele} builds the two edges of the triangle from the span of stages. Then Section~\ref{sec:main} proves that the stage contextad is the transported pseudo-algebra. The companion paper~\cite{Kam26b} runs the same constructions for double categories through the double Grothendieck construction of Cruttwell, Lambert, Pronk and Szyld~\cite{CLPS22}.

Free monoids for a tensor preserving coproducts are due to Kelly~\cite[Thm.~23.4]{Kel80}, while the transport of algebra structure along equivalences is due to Kelly and Lack~\cite{KL04}. Contextads with the display and stage contextads are due to Capucci and Myers. They identify the Kleisli construction of a polynomial monad with the co-Kleisli construction of its contextad, and they sketch the argument for parametric right adjoint monads~\cite[Thm.~A.4, Rem.~A.5]{CM24}. On the side of monads, the Grothendieck construction of fibrations is a 2-monad~\cite[Prop.~4.2.3]{Web15}, and for discrete stages the Grothendieck monad is the polynomial pseudomonad of a natural model~\cite[Thm.~4.1]{AN18}. Telescopes as iterated Grothendieck constructions with their $n$-ary sums also appear as contextual slices~\cite[Def.~6]{ALN24} and internally~\cite[Sec.~2]{Boc21}. Newstead hoped that the polynomial pseudomonad of a natural model would resemble the free monad on its polynomial functor, but he set this aside~\cite[4.5.15]{New18}.

Against this background, the fibred Grothendieck extension and its monoidality are new, and so is the description of telescopes as the free monad on $\int$. The paper also proves the Kleisli and co-Kleisli sketch of Capucci and Myers for the Grothendieck monad, even for non-discrete stages. Finally, it identifies the transported structure map with the dependent sum and shows that the extension turns it into the iterated multiplication up to isomorphism. The rest is organisation, because universal properties, transport and diagrams carry the proofs.

The reader is assumed to know 2-monads and their strict algebras~\cite{BKP89} and pseudomonads~\cite{Lac00}. The appendix recalls fibrations and collects the conventions, the diagram calculi of Table~\ref{tab:diag} and $\Tel$ on colax maps. The dependencies after the contents show how the sections build on each other, where an arrow means that the definition or proof of its target uses its source.

\FloatBarrier
\section{Preliminaries}\label{sec:prelim}

The ingredients of the paper are free constructions in a monoidal 2-category of spans, the telescope monad, contextads and the Grothendieck construction, and this section lays them out over a fixed category $\cat C$. Their conventions and diagram calculi are collected in the appendix.

\subsection{Spans, free monoids and transport}\label{sec:free}

\begin{definition}[Spans]\label{def:endospan}
The 2-category $\SpanC$ of spans on $\cat C$ has the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Objects.} The spans $\cat C\xleftarrow{p}\cat M\xrightarrow{\odot}\cat C$ of categories. Such a span is written $\cat M$. The fibre of $p$ at $A\in\cat C$ is $\cat M_A$, and the right leg gives $A\odot P:=\odot(P)$ for $P\in\cat M_A$.
\item \emph{1-cells.} The functors $k\colon\cat M\to\cat M'$ with $k\sq p'=p$ and $k\sq\odot'=\odot$.
\item \emph{2-cells.} The transformations $\sigma\colon k\Rightarrow k'$ with $\sigma\sq p'=\id$ and $\sigma\sq\odot'=\id$.
\item \emph{Tensor.} The composite $\cat M\ltimes\cat N$ of spans, which is the strict pullback
\begin{equation}\label{eq:ltimes}
\begin{tikzcd}[column sep=1.6em,row sep=1.4em]
 & & \cat M\ltimes\cat N \arrow[dl] \arrow[dr] & & \\
 & \cat M \arrow[dl,"p_{\cat M}"'] \arrow[dr,"\odot_{\cat M}"] & & \cat N \arrow[dl,"p_{\cat N}"'] \arrow[dr,"\odot_{\cat N}"] & \\
 \cat C & & \cat C & & \cat C
\end{tikzcd}
\end{equation}
with the outer legs. Hence its objects are the pairs $(P,Q)$ with $A\in\cat C$, $P\in\cat M_A$ and $Q\in\cat N_{A\odot P}$. On 1-cells $k\colon\cat M\to\cat M'$ and $h\colon\cat N\to\cat N'$ the tensor $k\ltimes h$ is induced by $k$ and $h$ between the pullbacks.
\item \emph{Unit.} The span $\cat C\xleftarrow{\id}\cat C\xrightarrow{\id}\cat C$, written $\cat C$.
\end{enumerate}
\end{definition}

\begin{lemma}[Spans form a monoidal 2-category]\label{lem:monoidal}
$(\SpanC,\ltimes,\cat C)$ is a monoidal 2-category whose coproducts are those of $\CAT$, and $\ltimes$ preserves them in each variable.
\end{lemma}
\begin{proof}
The strictly commuting map $(k,\id_{\cat C},h)$ of cospans induces $k\ltimes h$ on strict pullbacks. Likewise, the coherence isomorphisms are the canonical isomorphisms of iterated pullbacks, which are unique and hence coherent. Finally, $\ltimes$ preserves coproducts in each variable because pullback in $\CAT$ preserves them.
\end{proof}

A monoid $(\cat M,I,\otimes)$ in $\SpanC$ is a strict double category with tight category $\cat C$, loose category $\cat M$, source $p$, target $\odot$, loose units $I$ and loose composition $\otimes$~\cite[Sec.~1.3]{CM24}.

\begin{proposition}[Free monoids as coproducts of powers]\label{prop:monad}
Let $(\mathbf K,\boxtimes)$ be a monoidal 2-category with countable coproducts, preserved by $\boxtimes$ in each variable. The 2-category $\Mon$ of monoids in $\mathbf K$ has the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Objects.} The monoids in $\mathbf K$.
\item \emph{1-cells.} The 1-cells of $\mathbf K$ preserving unit and multiplication.
\item \emph{2-cells.} The 2-cells of $\mathbf K$ compatible with unit and multiplication.
\end{enumerate}
The forgetful 2-functor $U\colon\Mon\to\mathbf K$ has a left 2-adjoint $\mathrm{Fr}$, and the free monoid $\mathrm{Fr}(X)$ is $\coprod_{n\ge0}X^{\boxtimes n}$, with concatenation as multiplication and the injection of $X^{\boxtimes0}$ as unit.
\end{proposition}
\begin{proof}
The free monoid is Kelly's construction, and its universal property extends to 2-cells. Indeed, a 2-cell out of $\coprod_nX^{\boxtimes n}$ compatible with the multiplication is determined by its restriction $\sigma$ along the injection of $X$, and conversely every $\sigma$ extends by $\sigma^{\boxtimes n}$ on the $n$-th summand. Hence the adjunction is a 2-adjunction.
\end{proof}

\begin{definition}[Pseudo-algebras, {\cite[Def.~1.2]{LN19}}]\label{def:psalg}
Let $T$ be a pseudomonad on $\mathbf K$.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Pseudo-algebras.} A \emph{pseudo-algebra} $(\cat N,x,\bar x,\bar x_0)$ of $T$ has the following parts.
\begin{enumerate}[label=(\alph*),leftmargin=*]
\item \emph{Carrier.} An object $\cat N$ of $\mathbf K$.
\item \emph{Structure map.} A 1-cell $x\colon T(\cat N)\to\cat N$.
\item \emph{Multiplication constraint.} An invertible 2-cell $\bar x\colon T(x)\sq x\Rightarrow\mu\sq x$.
\item \emph{Unit constraint.} An invertible 2-cell $\bar x_0\colon\id\Rightarrow\eta\sq x$.
\item \emph{Axioms.} Two coherence axioms, which are equations between 2-cells from $T^3(\cat N)$ and from $T(\cat N)$ into $\cat N$.
\end{enumerate}
\item \emph{Strict algebras.} A \emph{strict algebra} $(\cat M,a)$ is a pseudo-algebra whose constraints are identities.
\item \emph{Pseudomorphisms.} A \emph{pseudomorphism} $(f,\bar f)\colon(\cat N,x)\to(\cat N',y)$ has the following parts.
\begin{enumerate}[label=(\alph*),leftmargin=*]
\item \emph{1-cell.} A 1-cell $f\colon\cat N\to\cat N'$.
\item \emph{Constraint.} An invertible 2-cell $\bar f\colon T(f)\sq y\Rightarrow x\sq f$.
\item \emph{Axioms.} Compatibility of $\bar f$ with the constraints of $x$ and $y$, which consists of equations between 2-cells into $\cat N'$.
\end{enumerate}
\item \emph{Transformations and equivalences.} The transformations of pseudomorphisms and the adjoint equivalences of pseudo-algebras are those of the same paper.
\end{enumerate}
\end{definition}

\begin{lemma}[Transport of structure, {\cite[Thm.~6.1]{KL04}}, {\cite[Cor.~4.4]{ASS25}}]\label{lem:transport}
Let $T$ be a pseudomonad on $\mathbf K$ with a strict algebra $(\cat M,a)$, and let $(\chi,\psi,\zeta,e)$ be an adjoint equivalence with $\chi\colon\cat N\to\cat M$, unit $\zeta\colon\id\Rightarrow\chi\sq\psi$ and counit $e\colon\psi\sq\chi\Rightarrow\id$. Then the following hold.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Transported pseudo-algebra.} $(\cat N,x,\bar x,\zeta)$ is a pseudo-algebra whose structure map is $x:=T(\chi)\sq a\sq\psi$ and whose unit constraint is $\zeta$. Its multiplication constraint is $\bar x:=(T^2(\chi)\sq T(a))\ast T(e)\ast(a\sq\psi)$ up to the constraints of $T$.
\item \emph{Equivalence.} The pseudomorphism $(\chi,\bar\chi)$ with $\bar\chi:=(T(\chi)\sq a)\ast e^{-1}$ is an adjoint equivalence of pseudo-algebras $(\cat N,x)\simeq(\cat M,a)$.
\end{enumerate}
\end{lemma}

Theorem~\ref{thm:main} applies this lemma to the telescope monad and the display contextad.

\subsection{The telescope monad}\label{sec:tel}

\begin{definition}[Powers and chains of a span]\label{def:tuples}
For a span $\cat M$ on $\cat C$ and $n\ge0$, the $n$-th power $\cat M^{\ltimes n}$ is the span with the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Apex.} $\cat M^{\ltimes0}=\cat C$ and $\cat M^{\ltimes(n+1)}=\cat M^{\ltimes n}\ltimes\cat M$.
\item \emph{Chains.} The objects of $\cat M^{\ltimes n}$ are the \emph{chains} $(A\mid\vec P)=(A\mid P_0,\dots,P_{n-1})$ with $A\in\cat C$ and $P_i\in\cat M_{A\odot P_0\odot\cdots\odot P_{i-1}}$ for $0\le i<n$, where the iterated $\odot$ is bracketed to the left.
\item \emph{Legs.} By pasting of pullbacks, $\cat M^{\ltimes n}$ is the apex of a pyramid of pullbacks, shown for $n=3$,
\begin{equation}\label{eq:pyramid}
\begin{tikzcd}[column sep=1.2em,row sep=1.3em]
 & & & \cat M^{\ltimes3} \arrow[dl] \arrow[dr] & & & \\
 & & \cat M^{\ltimes2} \arrow[dl] \arrow[dr] & & \cat M^{\ltimes2} \arrow[dl] \arrow[dr] & & \\
 & \cat M \arrow[dl,"p"'] \arrow[dr,"\odot"] & & \cat M \arrow[dl,"p"'] \arrow[dr,"\odot"] & & \cat M \arrow[dl,"p"'] \arrow[dr,"\odot"] & \\
 \cat C & & \cat C & & \cat C & & \cat C
\end{tikzcd}
\end{equation}
The legs are the outer edges of the pyramid, and hence for $n\ge1$ the right leg is the projection to the last factor $\cat M$ followed by $\odot$.
\end{enumerate}
\end{definition}

\begin{lemma}[Powers of a left fibrant span]\label{lem:tuples}\leavevmode
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item If $p$ is a cloven fibration, then so is the left leg of $\cat M^{\ltimes n}$, and its cartesian morphisms are the morphisms with $p$-cartesian components.
\item Concatenation gives $\cat M^{\ltimes n}\ltimes\cat M^{\ltimes m}\cong\cat M^{\ltimes(n+m)}$.
\end{enumerate}
\end{lemma}
\begin{proof}
Part (i) follows from Lemmas~\ref{lem:comp} and~\ref{lem:pb} because $\cat M^{\ltimes(n+1)}\to\cat M^{\ltimes n}$ is a pullback of $p$. Part (ii) holds because the powers are bracketed to the left.
\end{proof}

\begin{definition}[Telescope monad]\label{def:telemonad}
The \emph{telescope monad} $(\Tel,\eta,\mu)$ on $\SpanC$ consists of the following.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Objects.} $\Tel(\cat M)=\coprod_{n\ge0}\cat M^{\ltimes n}$ with the legs of the summands. By Proposition~\ref{prop:monad} it is the free monoid on $\cat M$, which is also called the Kleene star of $\cat M$.
\item \emph{1-cells and 2-cells.} $\Tel(k)=\coprod_nk^{\ltimes n}$ and $\Tel(\sigma)=\coprod_n\sigma^{\ltimes n}$.
\item \emph{Unit.} $\eta$ is the coproduct injection $\iota_1$ of $\cat M=\cat M^{\ltimes1}$.
\item \emph{Multiplication.} $\mu$ is the coproduct of the concatenation isomorphisms $\cat M^{\ltimes n_1}\ltimes\cdots\ltimes\cat M^{\ltimes n_r}\cong\cat M^{\ltimes(n_1+\cdots+n_r)}$ of Lemma~\ref{lem:tuples}(ii), whose domains are the summands of $\Tel^2(\cat M)$ by Lemma~\ref{lem:monoidal}.
\end{enumerate}
\end{definition}

Therefore $\Tel$ is the free-monoid 2-monad of $(\SpanC,\ltimes)$ by Proposition~\ref{prop:monad} and Lemma~\ref{lem:monoidal}.

\begin{definition}[Eilenberg--Moore 2-category]\label{def:telealg}
The 2-category $\EM(\Tel)$ of strict Eilenberg--Moore algebras of $\Tel$ has the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Objects.} The pairs $(\cat M,a)$ of $\cat M\in\SpanC$ and a structure map $a\colon\Tel(\cat M)\to\cat M$ in $\SpanC$, subject to the unit law $\eta\sq a=\id$ and the multiplication law $\mu\sq a=\Tel(a)\sq a$.
\item \emph{1-cells.} The $k\colon\cat M\to\cat M'$ of $\SpanC$ with $a\sq k=\Tel(k)\sq a'$, from $(\cat M,a)$ to $(\cat M',a')$.
\item \emph{2-cells.} The $\sigma\colon k\Rightarrow k'$ of $\SpanC$ with $a\sq\sigma=\Tel(\sigma)\sq a'$.
\item \emph{Composition.} That of $\SpanC$.
\end{enumerate}
The same parts in $\fSpan_{\mathrm s}(\cat C)$ give $\EM(\Tel)$ there.
\end{definition}

\subsection{Contextads}\label{sec:emkl}

\begin{definition}[Left fibrant spans, {\cite[Def.~3.10, 2.16, Lemma~3.11, Thm.~4.18]{CM24}}]\label{def:lfs}
The 2-category $\fSpan^{\Rightarrow}(\cat C)$ has the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Objects.} The \emph{left fibrant spans}, which are the spans $(\cat M,p,\odot)$ whose left leg $p$ is a cloven fibration in the sense of Definition~\ref{def:fib}. On such a span, the chosen lift $\tilde u_P\colon u^*P\to P$ of $u\colon A'\to A$ at $P\in\cat M_A$ gives $u\odot P:=\odot(\tilde u_P)\colon A'\odot u^*P\to A\odot P$.
\item \emph{1-cells.} The \emph{right colax maps} $(k,\kappa)\colon\cat M\to\cat M'$. Each consists of a cartesian functor $k$ with $k\sq p'=p$ and a \emph{colaxator} $\kappa\colon k\sq\odot'\Rightarrow\odot$, and it is written $k$ when $\kappa$ is clear. Two right colax maps compose by $(k,\kappa)\sq(h,\nu)=\bigl(k\sq h,(k\sq\nu)\sq\kappa\bigr)$ for $(h,\nu)\colon\cat M'\to\cat M''$.
\item \emph{2-cells.} The $\sigma\colon k\Rightarrow k'$ with $\sigma\sq p'=\id$ and $(\sigma\sq\odot')\sq\kappa'=\kappa$.
\item \emph{Tensor.} On objects, $\ltimes$ is that of Definition~\ref{def:endospan}. On 1-cells $(k,\kappa)\colon\cat M\to\cat M'$ and $(h,\nu)\colon\cat N\to\cat N'$, it is given by $((k,\kappa)\ltimes(h,\nu))(P,Q)=(kP,\ \kappa_P^*hQ)$, where $hQ\in\cat N'_{A\odot P}$ is reindexed along $\kappa_P\colon A\odot_{\cat M'}kP\to A\odot_{\cat M}P$. Its colaxator $(\kappa_P\odot_{\cat N'}hQ)\sq\nu_Q$ is isomorphic to the composite (3.2.5) of the cited paper because $h$ is cartesian. Finally, on 2-cells $\ltimes$ is as in (3.2.7) of the cited paper.
\item \emph{Monoidal structure.} Since the left fibrant spans on $\cat C$ form the endo-hom of the tricategory of Capucci and Myers, $\fSpan^{\Rightarrow}(\cat C)$ is a monoidal bicategory under $\ltimes$.
\item \emph{Sub-2-categories.} The locally full sub-2-categories $\fSpan^{\cong}(\cat C)$ and $\fSpan_{\mathrm s}(\cat C)$ have the 1-cells with invertible and with identity colaxators, and the first is closed under $\ltimes$. The second is the sub-2-category of $\SpanC$ on the left fibrant spans and the cartesian 1-cells, and it is closed under $\ltimes$ by Lemmas~\ref{lem:comp} and~\ref{lem:pb} and under coproducts and $\Tel$ by Lemma~\ref{lem:tuples}.
\end{enumerate}
\end{definition}

\begin{definition}[Contextad, {\cite[Def.~3.15]{CM24}}]\label{def:ctxd}
A \emph{contextad} on $\cat C$ is a tuple
\[(\cat M,I,\varepsilon,\otimes,\delta,\lambda,\rho,\alpha)\]
making a left fibrant span a pseudomonoid for $\ltimes$ in $\fSpan^{\Rightarrow}(\cat C)$. Equivalently, it is a pseudomonad on $\cat C$ in the bicategory of left fibrant spans, and it has the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Carrier.} A left fibrant span $\cat M=(\cat M,p,\odot)$ on $\cat C$.
\item \emph{Unit.} A 1-cell $(I,\varepsilon)\colon\cat C\to\cat M$ of $\fSpan^{\Rightarrow}(\cat C)$ with colaxator $\varepsilon\colon I\sq\odot\Rightarrow\id_{\cat C}$, whose components at $A\in\cat C$ are $I_A\in\cat M_A$ and $\varepsilon_A\colon A\odot I_A\to A$.
\item \emph{Multiplication.} A 1-cell $(\otimes,\delta)\colon\cat M\ltimes\cat M\to\cat M$ of $\fSpan^{\Rightarrow}(\cat C)$ with colaxator $\delta\colon\otimes\sq\odot\Rightarrow\odot_{\cat M\ltimes\cat M}$, whose components at $P\in\cat M_A$ and $Q\in\cat M_{A\odot P}$ are $P\otimes Q\in\cat M_A$ and $\delta_{P,Q}\colon A\odot(P\otimes Q)\to(A\odot P)\odot Q$.
\item \emph{Coherence.} Invertible 2-cells $\lambda$, $\rho$, $\alpha$ of $\fSpan^{\Rightarrow}(\cat C)$ as listed in Definition~\ref{def:ctxdcoh}(i).
\item \emph{Axioms.} Those of the cited definition as listed in Definition~\ref{def:ctxdcoh}(ii).
\end{enumerate}
\end{definition}

\begin{definition}[Strict contextad]\label{def:strict}
A contextad is \emph{strict} when the following hold.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Identity colaxators.} $\varepsilon=\id$ and $\delta=\id$.
\item \emph{Strict laws.} $(I\ltimes\cat M)\sq\otimes=\id=(\cat M\ltimes I)\sq\otimes$ and $(\otimes\ltimes\cat M)\sq\otimes=(\cat M\ltimes\otimes)\sq\otimes$, in pasting and string diagrams
\begin{equation}\label{eq:ctxlaws}
\begin{array}{c@{\qquad\qquad}c}
\begin{tikzcd}[ampersand replacement=\&]
\cat M \arrow[r,"I\ltimes\cat M"] \arrow[dr,equal] \& \cat M\ltimes\cat M \arrow[d,"\otimes"] \& \cat M \arrow[l,"\cat M\ltimes I"'] \arrow[dl,equal]\\
\& \cat M \&
\end{tikzcd}
&
\underset{\scriptstyle (I\ltimes\cat M)\sq\otimes}{\sdunitL}\ =\ \underset{\scriptstyle \id}{\sdwire{P}}\ =\ \underset{\scriptstyle (\cat M\ltimes I)\sq\otimes}{\sdunitR}\\[6mm]
\begin{tikzcd}[ampersand replacement=\&]
\cat M^{\ltimes3} \arrow[r,"\otimes\ltimes\cat M"] \arrow[d,"\cat M\ltimes\otimes"'] \& \cat M^{\ltimes2} \arrow[d,"\otimes"]\\
\cat M^{\ltimes2} \arrow[r,"\otimes"'] \& \cat M
\end{tikzcd}
&
\underset{\scriptstyle (\otimes\ltimes\cat M)\sq\otimes}{\sdassocL}\ =\ \underset{\scriptstyle (\cat M\ltimes\otimes)\sq\otimes}{\sdassocR}
\end{array}
\end{equation}
\item \emph{Normal coherence.} The cleavage is normal and $\lambda$, $\rho$, $\alpha$ are identities.
\end{enumerate}
\end{definition}

\begin{definition}[Strict morphism of contextads, {\cite[Def.~4.25, Not.~4.28]{CM24}}]\label{def:strictmor}
A \emph{strict morphism} $k\colon\cat N\to\cat M$ of contextads has the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{1-cell.} A 1-cell $k$ of $\fSpan_{\mathrm s}(\cat C)$.
\item \emph{Unitor.} An invertible 2-cell $I^{\cat N}\sq k\cong I^{\cat M}$ of $\fSpan^{\Rightarrow}(\cat C)$.
\item \emph{Multiplicator.} An invertible 2-cell $\otimes^{\cat N}\sq k\cong(k\ltimes k)\sq\otimes^{\cat M}$ of $\fSpan^{\Rightarrow}(\cat C)$.
\item \emph{Axioms.} Compatibility with $\lambda$, $\rho$ and $\alpha$, as for a morphism of pseudomonoids.
\end{enumerate}
\end{definition}

As for monoids in $\SpanC$, a strict contextad on $\cat C$ is a strict double category with tight category $\cat C$ and loose category $\cat M$, whose source $p$ is a fibration with normal cleavage and whose target is $\odot$. Moreover, its loose units $I$ and loose composition $\otimes$ are cartesian, and its loose morphisms are the objects of $\cat M$, called the one-step extensions.

The display spans below have morphisms $P\colon E\to B$ of $\cat C$ as objects and squares between them as morphisms. Here a square $(h,u)\colon Q\to P$ from $Q\colon E'\to B'$ to $P\colon E\to B$ is a commuting square $h\sq P=Q\sq u$ of $\cat C$ whose top is $h\colon E'\to E$ and whose bottom is $u\colon B'\to B$.

\begin{definition}[Display class]\label{def:dispclass}
A \emph{display class} $(\Dcls,(-)^*)$ on $\cat C$ has the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Display maps.} A class $\Dcls$ of morphisms of $\cat C$ that is closed under composition with isomorphisms and whose members are called the \emph{display maps}.
\item \emph{Chosen pullbacks.} For each $P\colon E\to B$ in $\Dcls$ and $u\colon B'\to B$, a pullback square $(\bar u,u)\colon u^*P\to P$ with $u^*P\colon u^*E\to B'$ in $\Dcls$.
\item \emph{Normality.} $\id^*P=P$.
\end{enumerate}
\end{definition}
Throughout, $(\Dcls,(-)^*)$ is a display class on $\cat C$.

\begin{definition}[Display span]\label{def:dispspan}
A \emph{display span} for $\Dcls$ is a subcategory $\cat M$ of the arrow category of $\cat C$ with the morphisms in $\Dcls$ as objects, subject to the following.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Pullbacks.} Every pullback square between morphisms in $\Dcls$ lies in $\cat M$.
\item \emph{Factorisation.} If $(h,u)\in\cat M$ factors as $(g,\id)\sq(h',u)$ through a pullback square $(h',u)$, then $(g,\id)\in\cat M$.
\end{enumerate}
The display span $\cat M^{\mathrm{all}}_{\Dcls}$ has all squares.
\end{definition}

\begin{proposition}[Display spans are left fibrant]\label{prop:dispspan}
For a display span $\cat M$, $\cat C\xleftarrow{\mathrm{cod}}\cat M\xrightarrow{\mathrm{dom}}\cat C$ is a left fibrant span whose left leg $\mathrm{cod}$ has the chosen pullback squares as a normal cleavage and the pullback squares as cartesian morphisms.
\end{proposition}
\begin{proof}
Consider morphisms $u\colon B'\to B$ and $v\colon B''\to B'$ and a square $(h,v\sq u)\colon Q\to P$ of $\cat M$. Since pasting the chosen squares of $P$ along $u$ and of $u^*P$ along $v$ gives a pullback, $(h,v\sq u)$ factors through it as $(g,\id)\sq(\bar v,v)\sq(\bar u,u)$ for a unique $g$. Then $(g,\id)\in\cat M$ by Definition~\ref{def:dispspan}(ii) and $(\bar v,v)\in\cat M$ by (i), and hence $(\bar u,u)$ is cartesian for $\mathrm{cod}$. Moreover, the cleavage is normal since $\id^*P=P$. Finally, cartesian morphisms and pullback squares agree because each differs from a chosen square by an isomorphism above an identity.
\end{proof}

\begin{definition}[Display contextad]\label{def:dispctx}
A display span $\cat M$ is a \emph{display contextad} when it satisfies the following.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Identities and composites.} $\Dcls$ contains the identities and is closed under composition.
\item \emph{Vertical pasting.} $\cat M$ is closed under vertical pasting, which takes two stacked squares to one square,
\begin{equation}\label{eq:vpaste}
\begin{tikzcd}[row sep=normal]
E_2 \arrow[r,"h_2"] \arrow[d,"Q"'] & E'_2 \arrow[d,"Q'"] \\
E_1 \arrow[r,"h_1"] \arrow[d,"P"'] & E'_1 \arrow[d,"P'"] \\
A \arrow[r,"u"'] & A'
\end{tikzcd}
\qquad\rightsquigarrow\qquad
\begin{tikzcd}[row sep=5.2em]
E_2 \arrow[r,"h_2"] \arrow[d,"Q\sq P"'] & E'_2 \arrow[d,"Q'\sq P'"] \\
A \arrow[r,"u"'] & A'
\end{tikzcd}
\end{equation}
\end{enumerate}
\end{definition}

\begin{proposition}[Display contextads are strict, {\cite[Ex.~3.21]{CM24}}]\label{prop:dispctx}
A display contextad is a strict contextad with the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Unit.} The functor $I\colon\cat C\to\cat M$ of identity arrows and identity squares, with $I_A=\id_A$.
\item \emph{Multiplication.} Vertical pasting $\otimes\colon\cat M\ltimes\cat M\to\cat M$~\eqref{eq:vpaste}, with $P\otimes Q=Q\sq P$.
\end{enumerate}
\end{proposition}
\begin{proof}
The arrow category gives a monoid $(\cat C\xleftarrow{\mathrm{cod}}\cat C^{\to}\xrightarrow{\mathrm{dom}}\cat C,\id,\otimes)$ in $\SpanC$ whose multiplication $\otimes$ is the vertical pasting~\eqref{eq:vpaste}, and this monoid is the double category of commuting squares of $\cat C$. By Definition~\ref{def:dispctx}, $\cat M$ is a submonoid and therefore inherits the strict laws. Moreover, $\cat M$ is a left fibrant span by Proposition~\ref{prop:dispspan}, and its $I$ and $\otimes$ are cartesian by the pasting lemma for pullbacks. Since pullbacks along identities are identities, the cleavage is normal, and $\lambda$, $\rho$, $\alpha$ are identities.
\end{proof}

In the instances, $\cat C$ is a category of category-like structures, and its display maps are fibrations between them. For example, $\Cat$ with the Grothendieck fibrations and the squares with cartesian top is a display contextad by Lemmas~\ref{lem:comp} and~\ref{lem:pb} when pullbacks along identities are chosen to be identities. Likewise, $\Cat$ with the discrete fibrations and all squares between them is a display contextad, and the companion paper~\cite{Kam26b} verifies that the strict double functors and the double fibrations of~\cite[Def.~2.25]{CLPS22} form another.

\begin{definition}[Co-Kleisli construction, {\cite[Def.~3.17, Sec.~3.5]{CM24}}]\label{def:ctx}
The \emph{co-Kleisli construction} of a contextad $\cat N$ on $\cat C$ is the pseudo double category $\coKl(\cat N)$ of contextful arrows, and it has the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Objects and tight morphisms.} Those of $\cat C$.
\item \emph{Loose morphisms.} A loose morphism $A\lto B$ is a pair $(P,f)$ of $P\in\cat N_A$ and a \emph{body} $f\colon A\odot P\to B$.
\item \emph{Cells.} A cell from $(P,f)\colon A\lto B$ to $(P',f')\colon A'\lto B'$ over $u\colon A\to A'$ and $v\colon B\to B'$ is a $\theta\colon P\to P'$ in $\cat N$ above $u$ with $f\sq v=\odot(\theta)\sq f'$.
\item \emph{Loose composition.} For $(Q,g)\colon B\lto D$, $(P,f)\sq(Q,g)=(P\otimes f^*Q,\ \delta_{P,f^*Q}\sq(f\odot Q)\sq g)$.
\item \emph{Loose identities.} $(I_A,\varepsilon_A)\colon A\lto A$.
\end{enumerate}
\end{definition}

\begin{corollary}[Strict contextads as algebras]\label{cor:alg}
$\Tel$ restricts to $\fSpan_{\mathrm s}(\cat C)$, where $\EM(\Tel)\cong\Mon(\fSpan_{\mathrm s}(\cat C),\ltimes)$. Hence the algebras with normal cleavage are the strict contextads, which are the monoids $(\cat M,I,\otimes)$ of Definition~\ref{def:ctxd}(i)--(iii) subject to Definition~\ref{def:strict}(i), (ii). Along the coproduct injections $\iota_n\colon\cat M^{\ltimes n}\to\Tel(\cat M)$, an algebra $(\cat M,a)$ and its monoid $(\cat M,I,\otimes)$ correspond by
\begin{equation}\label{eq:algsd}
\begin{array}{c@{\qquad\qquad}c}
\begin{tikzcd}[ampersand replacement=\&]
\cat C \arrow[r,"\iota_0"] \arrow[dr,"I"'] \& \Tel(\cat M) \arrow[d,"a"]\\
\& \cat M
\end{tikzcd}
&
\underset{\scriptstyle \iota_0\sq a}{\sdboxzero}\ =\ \underset{\scriptstyle I}{\sdunit}\\[5mm]
\begin{tikzcd}[ampersand replacement=\&]
\cat M \arrow[r,"\iota_1"] \arrow[dr,equal] \& \Tel(\cat M) \arrow[d,"a"]\\
\& \cat M
\end{tikzcd}
&
\underset{\scriptstyle \iota_1\sq a}{\sdboxone}\ =\ \underset{\scriptstyle \id}{\sdwire{P}}\\[5mm]
\begin{tikzcd}[ampersand replacement=\&]
\cat M\ltimes\cat M \arrow[r,"\iota_2"] \arrow[dr,"\otimes"'] \& \Tel(\cat M) \arrow[d,"a"]\\
\& \cat M
\end{tikzcd}
&
\underset{\scriptstyle \iota_2\sq a}{\sdboxtwo}\ =\ \underset{\scriptstyle \otimes}{\sdmul}\\[5mm]
\begin{tikzcd}[ampersand replacement=\&]
\cat M^{\ltimes4} \arrow[r,"\iota_4"] \arrow[d,"\cat M^{\ltimes2}\ltimes\otimes"'] \& \Tel(\cat M) \arrow[dr,"a"] \&\\
\cat M^{\ltimes3} \arrow[r,"\cat M\ltimes\otimes"'] \& \cat M^{\ltimes2} \arrow[r,"\otimes"'] \& \cat M
\end{tikzcd}
&
\underset{\scriptstyle \iota_4\sq a}{\sdbigbox}\ =\ \underset{\scriptstyle (\cat M^{\ltimes2}\ltimes\otimes)\sq(\cat M\ltimes\otimes)\sq\otimes}{\sdcomb}
\end{array}
\end{equation}
with the \emph{comb formula} $\iota_n\sq a=(\cat M^{\ltimes(n-2)}\ltimes\otimes)\sq\cdots\sq(\cat M\ltimes\otimes)\sq\otimes$ for $n\ge2$.
\end{corollary}
\begin{proof}
By Lemma~\ref{lem:tuples}(i), $\Tel$ restricts to $\fSpan_{\mathrm s}(\cat C)$, and the comparison 2-functor from monoids to $\EM(\Tel)$ of $\mathrm{Fr}\dashv U$ sends a monoid to its comb maps. Its inverse restricts $a$ along the coproduct injections $\iota_0$ and $\iota_2$, and the laws below make both well defined and mutually inverse. They follow from the multiplication law $\mu\sq a=\Tel(a)\sq a$, which reads in string diagrams as
\begin{equation}\label{eq:blocks}
\begin{tikzcd}
\Tel^2(\cat M) \arrow[r,"\mu"] \arrow[d,"\Tel(a)"'] & \Tel(\cat M) \arrow[d,"a"]\\
\Tel(\cat M) \arrow[r,"a"'] & \cat M
\end{tikzcd}
\qquad\qquad
\underset{\scriptstyle \mu\sq a}{\sdmuL}\ =\ \underset{\scriptstyle \Tel(a)\sq a}{\sdmuR}\ ,
\end{equation}
with $\Tel$ a grey stripe around the wire as in Proposition~\ref{prop:sound}(ii), and Figure~\ref{fig:stack} draws it. On the summands $\cat M^{\ltimes n}\ltimes\cat M^{\ltimes m}$ of $\Tel^2(\cat M)$ with $(n,m)=(0,1),(1,0),(2,1),(1,2)$, this law yields the laws~\eqref{eq:ctxlaws} of Definition~\ref{def:strict}(ii) by~\eqref{eq:algsd}. On the summands $\cat M\ltimes\cat M^{\ltimes(n-1)}$ it likewise yields the comb formula as for unbiased monoidal categories~\cite[after Cor.~3.2.5]{Lei04}. Finally, the colaxators are identities because $a\sq\odot_{\cat M}=\odot_{\Tel(\cat M)}$, and for a normal cleavage so is the coherence.
\end{proof}

\begin{figure}[htb]\centering
\begin{tikzpicture}[x=5.2mm,y=5.2mm,line width=0.6pt,
 ap/.style={circle,fill=black,inner sep=0pt,minimum size=2.4pt},
 ft/.style={circle,fill=white,draw,line width=0.5pt,inner sep=0pt,minimum size=2.4pt},
 lb/.style={font=\scriptsize,inner sep=1pt},
 blk/.style={draw,densely dashed,rounded corners=2pt,line width=0.4pt,black!60},
 bx/.style={draw,rectangle,inner sep=0pt,line width=0.6pt,fill=white,minimum height=3.4mm},
 mp/.style={->,thick,shorten <=1.5mm,shorten >=1.5mm}]
\newcommand{\tri}[3]{\draw (#2)--(#1)--(#3); \node[ap] at (#1) {};}
\newcommand{\feet}[2]{\foreach \x in {#2} \node[ft] at ($(#1)+(\x,0)$) {};}
\begin{scope}[shift={(0,7)},scale=1.25]
 \foreach \j/\i/\x/\y in {0/0/0/0,0/1/1/0,0/2/2/0,0/3/3/0,1/0/0.5/0.866,1/1/1.5/0.866,1/2/2.5/0.866,2/0/1/1.732,3/0/1.5/2.598} \coordinate (P-\j-\i) at (\x,\y);
 \draw[spl] (P-0-0)--(P-1-0)--(P-0-1)--(P-1-1)--(P-0-2)--(P-1-2)--(P-0-3); \draw[spl] (P-1-0)--(P-2-0)--(P-1-1); \draw[spl] (P-2-0)--(P-3-0)--(P-1-2);
 \foreach \q in {P-1-0,P-1-1,P-1-2,P-2-0,P-3-0} \node[spap] at (\q) {}; \foreach \i in {0,...,3} \node[spft] at (P-0-\i) {};
 \node[lb,above=2pt] at (P-3-0) {$\cat M^{\ltimes2}\ltimes\cat M$};
\end{scope}
\begin{scope}[shift={(7,7)},scale=1.25]
 \spanpyr{3}{0.866}{0} \node[lb,above=2pt] at (P-3-0) {$\cat M^{\ltimes3}$};
\end{scope}
\begin{scope}[shift={(0,-0.5)},scale=1.25]
 \spantri{0}{2}{0.866}{0} \coordinate (A) at (T); \spantri{2}{1}{0.866}{0} \coordinate (R) at (T);
 \coordinate (Y) at (1.5,2.598); \draw[spl] (A)--(Y)--(R); \node[spap] at (Y) {};
 \node[lb,above=2pt] at (Y) {$\cat M\ltimes\cat M$};
\end{scope}
\begin{scope}[shift={(7,-0.5)},scale=1.25]
 \spantri{0}{3}{0.866}{0} \node[lb,above=2pt] at (T) {$\cat M$};
\end{scope}
\draw[mp] (4.4,8.2) -- node[above,lb]{$\mu$} (6.7,8.2);
\draw[mp] (4.4,0.9) -- node[above,lb]{$a$} (6.7,0.9);
\draw[mp] (1.9,6.6) -- node[left,lb]{$\Tel(a)$} (1.9,3.6);
\draw[mp] (8.9,6.6) -- node[right,lb]{$a$} (8.9,3.6);
\begin{scope}[shift={(15,0)}]
\begin{scope}[shift={(0,7)}]
 \telband{-0.55}{2.95}{2.4}{0} \telband{-0.32}{1.32}{2.4}{0} \telband{2.06}{2.74}{2.4}{0}
 \foreach \x/\l in {0/P_0,1/P_1,2.4/P_2} {\draw (\x,2.6) -- (\x,0); \node[lb,above] at (\x,2.6) {$\l$};}
\end{scope}
\begin{scope}[shift={(7,7)}]
 \telband{-0.45}{2.45}{2.4}{0}
 \foreach \x/\l in {0/P_0,1/P_1,2/P_2} {\draw (\x,2.6) -- (\x,0); \node[lb,above] at (\x,2.6) {$\l$};}
\end{scope}
\begin{scope}[shift={(0,0)}]
 \telband{-0.55}{2.95}{2.7}{0} \telband{-0.32}{1.32}{2.7}{1.83} \telband{2.06}{2.74}{2.7}{1.83}
 \node[bx,minimum width=8.5mm] (b) at (0.5,1.5) {$\scriptstyle a$};
 \node[bx,minimum width=3.6mm] (b2) at (2.4,1.5) {$\scriptstyle a$};
 \draw (0,2.9) -- (0,1.5 |- b.north); \draw (1,2.9) -- (1,1.5 |- b.north); \draw (b.south) -- (0.5,0);
 \draw (2.4,2.9) -- (b2.north); \draw (b2.south) -- (2.4,0);
 \foreach \x/\l in {0/P_0,1/P_1,2.4/P_2} \node[lb,above] at (\x,2.9) {$\l$};
\end{scope}
\begin{scope}[shift={(7,0)}]
 \telband{-0.3}{2.3}{2.7}{1.83}
 \node[bx,minimum width=13.5mm] (b) at (1,1.5) {$\scriptstyle a$};
 \foreach \x/\l in {0/P_0,1/P_1,2/P_2} {\draw (\x,2.9) -- (\x,1.5 |- b.north); \node[lb,above] at (\x,2.9) {$\l$};}
 \draw (b.south) -- (1,0);
\end{scope}
\draw[mp] (3.4,8.2) -- node[above,lb]{$\mu$} (6.6,8.2);
\draw[mp] (3.4,1.2) -- node[above,lb]{$a$} (6.6,1.2);
\draw[mp] (1.2,6.0) -- node[left,lb]{$\Tel(a)$} (1.2,3.9);
\draw[mp] (8,6.0) -- node[right,lb]{$a$} (8,3.9);
\end{scope}
\end{tikzpicture}
\caption{Stacking and collapsing for $(\cat M,a)\in\EM(\Tel)$. Pasting diagrams in $\CAT$ stand on the left and stripe diagrams on the right, and Table~\ref{tab:diag} matches them. The summand $\cat M^{\ltimes2}\ltimes\cat M$ of $\Tel^2(\cat M)$ keeps its blocks as sub-pyramids of its lattice and as the inner stripes. On it, $\mu$ is the canonical isomorphism of iterated pullbacks onto the pyramid of $\cat M^{\ltimes3}$, which $a$ then collapses to $\cat M$. Alternatively, $\Tel(a)$ first collapses each block into an $a$ drawn in its inner stripe, and then $a$ collapses the rest. All four pictures stand on the same feet, and the triangles stay unfilled as for a general span.}\label{fig:stack}
\end{figure}

\subsection{Comprehensions and the span of stages}\label{sec:comp}

Let $S\colon\cat C^{\op}\to\CAT$ be a functor with reindexing $u^*:=S(u)$. Its Grothendieck construction is then the split fibration $\int S\to\cat C$ with the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Objects.} The pairs $(B,F)$ of $B\in\cat C$ and a \emph{stage} $F\in S(B)$ over $B$. Such a pair is written $F$ when $B$ is clear.
\item \emph{Morphisms.} The pairs $(u,\tau)\colon(A,G)\to(B,F)$ of $u\colon A\to B$ and $\tau\colon G\to u^*F$ in $S(A)$.
\item \emph{Composition.} $(w,\sigma)\sq(u,\tau)=(w\sq u,\ \sigma\sq w^*\tau)$ for $(w,\sigma)\colon(A',H)\to(A,G)$.
\item \emph{Projection and cleavage.} The projection sends $(u,\tau)$ to $u$, and the chosen cartesian morphisms are the $(u,\id)$.
\end{enumerate}

\begin{definition}[Comprehension]\label{def:comp}
A \emph{comprehension} $(S,\chi)$ into a display span $\cat M$ on $\cat C$ has the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Indexed category.} A functor $S\colon\cat C^{\op}\to\CAT$.
\item \emph{Comprehension functor.} A functor $\chi\colon\int S\to\cat M$.
\item \emph{Conditions.} $\chi\sq\mathrm{cod}$ is the projection, and $\chi$ sends chosen cartesian morphisms to pullback squares.
\item \emph{Components.} For $(B,F)\in\int S$ and $(u,\tau)\colon(A,G)\to(B,F)$ the comprehension gives
\begin{equation}\label{eq:compsq}
\chi F\colon B.F\to B,\qquad \chi(u,\tau)=(u.\tau,\ u)\colon\chi G\to\chi F,\qquad
\begin{tikzcd}[column sep=large,row sep=large]
A.u^*F \arrow[r,"u.\id"] \arrow[d,"\chi(u^*F)"'] \arrow[dr, phantom, "\lrcorner", very near start] & B.F \arrow[d,"\chi F"] \\
A \arrow[r,"u"'] & B
\end{tikzcd}
\end{equation}
\end{enumerate}
It is a \emph{comprehension equivalence} when each restriction $\chi_B\colon S(B)\to\cat M_B$ is an equivalence. Through the Grothendieck construction, a comprehension is a pseudonatural transformation $S\Rightarrow\cat M_{(-)}$, where the fibres $\cat M_{(-)}$ of $\mathrm{cod}$ form a pseudofunctor with reindexing by chosen pullbacks. Accordingly, a comprehension equivalence is a pseudonatural equivalence.
\end{definition}

A comprehension is a comprehension category in the sense of Jacobs~\cite{Jac93} with a split fibration and values in $\cat M$. Jacobs calls a comprehension category full when $\chi$ is fully faithful into the arrow category, but this condition differs from being a comprehension equivalence. Two instances are comprehension equivalences by~\cite[Thm.~2.1.2, 2.2.3]{LR20}, namely the category of elements of presheaves into the discrete fibrations~\cite[Sec.~3.1]{CE24} and the Grothendieck construction of pseudofunctors into the Grothendieck fibrations with the squares with cartesian top. In the second instance, $S(B)$ is the category of pseudofunctors $B^{\op}\to\Cat$. Their telescopes are the lists of presheaves of Palmgren and the telescopes of fibrations, whose binary dependent sum is that of~\cite[Thm.~4.1]{Str23}.

\begin{lemma}[The span of stages is left fibrant]\label{lem:compspan}
The \emph{span of stages} $\cat C\leftarrow\int S\rightarrow\cat C$ has the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Left leg.} The projection $p_{\int S}$.
\item \emph{Right leg.} $\odot_{\int S}:=\chi\sq\mathrm{dom}$, through which the span depends on $\chi$. The notation $B.F$ abbreviates $B\odot_{\int S}F$.
\item \emph{Display 2-cell.} $d:=\chi\ast(\mathrm{dom}\Rightarrow\mathrm{cod})\colon\odot\Rightarrow p$, with $d_F=\chi F$.
\end{enumerate}
It is a left fibrant span, and $\chi$ is a 1-cell of $\fSpan_{\mathrm s}(\cat C)$ into $\cat M$.
\end{lemma}
\begin{proof}
$\chi$ sends the chosen lifts $(u,\id)$ to pullback squares, and these are cartesian by Proposition~\ref{prop:dispspan}. Since every cartesian morphism is a chosen lift preceded by an isomorphism above an identity, $\chi$ is cartesian. Finally, $\chi$ is compatible with the legs because they are $\chi\sq\mathrm{cod}$ and $\chi\sq\mathrm{dom}$ by definition.
\end{proof}

\begin{lemma}[Comprehension equivalences are adjoint equivalences]\label{lem:adjeq}
Let $\chi$ be a comprehension equivalence into a display span $\cat M$. Then $\chi$ is part of an adjoint equivalence $(\chi,\psi,\zeta,e)$ in $\fSpan^{\cong}(\cat C)$ with the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Pseudo-inverse.} A cartesian functor $\psi\colon\cat M\to\int S$ over $\cat C$.
\item \emph{Unit.} An isomorphism $\zeta\colon\id\cong\chi\sq\psi$ above identities.
\item \emph{Counit.} An isomorphism $e\colon\psi\sq\chi\cong\id$ above identities.
\item \emph{Colaxator.} The top $\kappa_\psi:=e\sq\mathrm{dom}\colon\psi\sq\odot_{\int S}\Rightarrow\odot_{\cat M}$ of $e$, which makes $\psi=(\psi,\kappa_\psi)$ a 1-cell of $\fSpan^{\cong}(\cat C)$.
\end{enumerate}
\end{lemma}
\begin{proof}
By Lemma~\ref{lem:compspan}, $\chi$ is cartesian, and it is an equivalence on each fibre by assumption. Since a cartesian functor over $\cat C$ that is an equivalence on each fibre has a cartesian pseudo-inverse over $\cat C$~\cite[Sec.~3]{Str23}, $\chi$ is an equivalence of fibrations with a cartesian pseudo-inverse $\psi$ and a counit $e$ above identities. Because $\chi$ is fully faithful, the unit $\zeta$ is determined by $\zeta\ast\chi=\chi\ast e^{-1}$, and then the first triangle identity is $e^{-1}\sq e=\id$. The second triangle identity holds after whiskering with the faithful $\chi$, where it reduces to $(\psi\sq\chi)\ast e=e\ast(\psi\sq\chi)$. This equation holds because the interchange law gives $\bigl((\psi\sq\chi)\ast e\bigr)\sq e=\bigl(e\ast(\psi\sq\chi)\bigr)\sq e$ and $e$ is invertible. Finally, the top $e\sq\mathrm{dom}$ of $e$ is an invertible $\kappa_\psi\colon\psi\sq\odot_{\int S}\Rightarrow\odot_{\cat M}$, and hence $e$ and $\zeta$ are 2-cells of $\fSpan^{\cong}(\cat C)$ by Definition~\ref{def:lfs}.
\end{proof}

\begin{lemma}[Hom-categories into display spans are thin]\label{lem:thin}
Let $\cat N$ be a left fibrant span whose legs form a faithful functor $(p,\odot)\colon\cat N\to\cat C\times\cat C$. Then at most one 2-cell lies between two 1-cells $(k,\kappa),(k',\kappa')\colon\cat X\to\cat N$ of $\fSpan^{\cong}(\cat C)$. In particular, this applies to a display span $\cat M$ and to $\int S$ for a comprehension equivalence $\chi$.
\end{lemma}
\begin{proof}
A 2-cell $\sigma$ has $\sigma\sq p=\id$ and $\sigma\sq\odot=\kappa\sq\kappa'^{-1}$, which determine $\sigma$ because $(p,\odot)$ is faithful. For $\cat M$ the legs form a faithful functor because they are $\mathrm{cod}$ and $\mathrm{dom}$ on a subcategory of the arrow category. For $\int S$ the legs are $\chi$ followed by those of $\cat M$ by Lemma~\ref{lem:compspan}, and $\chi$ is faithful because it is an equivalence of categories with pseudo-inverse $\psi$ by Lemma~\ref{lem:adjeq}.
\end{proof}

Whereas Corollary~\ref{cor:alg} matches the algebras of $\Tel$ with the strict contextads, Sections~\ref{sec:tele} and~\ref{sec:main} show that the stage contextad is the pseudo-algebra of $\Tel$ transported along $\chi$. Lemma~\ref{lem:thin} makes every coherence axiom in that argument automatic.



\section{The Grothendieck monad}\label{sec:tele}

This section builds the two edges that leave the span of stages through the Grothendieck extension, and Section~\ref{sec:main} then shows why they correspond. Table~\ref{tab:three} sets the three vertices of the resulting triangle side by side.
\begin{table}[htb]\centering\small\setlength{\tabcolsep}{4pt}
\renewcommand{\arraystretch}{1.15}
\begin{tabularx}{\textwidth}{@{}>{\raggedright\arraybackslash}p{21mm}>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}X@{}}
\toprule
& Span of stages $\int S$ & Telescope monad $\Tel$ & Stage contextad $(\int S,I^{\int S},\wsemi)$\\
\midrule
Structure & span of stages, and its extension $\int=\Gext_{\int S}$ on $[\cat C^{\op},\CAT]$ & free-monoid 2-monad on $\SpanC$, restricting to $\fSpan_{\mathrm s}(\cat C)$ & pseudomonoid in $\fSpan^{\Rightarrow}(\cat C)$, colaxators from $e$\\
At $1$ & $\int1=S$ & $\Gext_{\Tel(\int S)}1\cong\coprod_n\int^n1\cong\Tel_S$ & $S$ with $I^{\int S}$ and $\wsemi$\\
Unit & & $\eta$, length one & $I^{\int S}=I^{\cat M}\sq\psi$, and $\eta^{\int}_1=I^{\int S}$\\
Multiplication & & $\mu$, concatenation & $\wsemi=(\chi\ltimes\chi)\sq\otimes^{\cat M}\sq\psi$, and $\mu^{\int}_1=\wsemi$\\
Triangles & the 2-cell $d=\chi\ast(\mathrm{dom}\Rightarrow\mathrm{cod})$ & pyramids of $\ltimes$-powers (Fig.~\ref{fig:stack}) & $\wsemi$ from a pyramid of two to one triangle\\
Arrows & & & Kleisli 1-cells $s$, $t$, $\coKl(\int S)\simeq\Kl(\int)\simeq\coKl(\cat M)$\\
Algebra of $\Tel$ & & free, $(\Tel(\int S),\mu)$ & pseudo, $(\int S,\Sigma)\simeq(\cat M,a)$, $\Sigma$ the iterated $\wsemi$, $\Gext_\Sigma\cong\coprod_n\mu^{(n)}$\\
Defined in & Lemma~\ref{lem:compspan}, Prop.~\ref{prop:freemonad} & Def.~\ref{def:telemonad} & Prop.~\ref{prop:stagectx}, \ref{prop:kleisli}\\
\bottomrule
\end{tabularx}
\caption{The vertices of the triangle, whose symbols are defined where the last row points. The stage contextad is transported from the display contextad, which is a strict algebra.}\label{tab:three}
\end{table}


\subsection{The Grothendieck extension of a span}\label{sec:gext}

\begin{construction}[Grothendieck extension]\label{cons:gext}
Let $[\cat C^{\op},\CAT]$ be the 2-category of functors $\cat C^{\op}\to\CAT$, pseudonatural transformations and modifications, with terminal object $1$ and Yoneda embedding $\yu$. A left fibrant span $(\cat M,p,\odot)$ with split $p$ then has a \emph{Grothendieck extension} $\Gext_{\cat M}$, which is the endo-2-functor of $[\cat C^{\op},\CAT]$ with the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Values.} At $Y\in[\cat C^{\op},\CAT]$ and $B\in\cat C$, the value of $\Gext_{\cat M}$ is the Grothendieck construction
\[(\Gext_{\cat M}Y)(B)=\int_{P\in\cat M_B}Y(B\odot P).\]
whose objects are the pairs $(P,y)$ of $P\in\cat M_B$ and $y\in Y(B\odot P)$ and whose morphisms $(P,y)\to(P',y')$ are the pairs $(\theta,\gamma)$ of $\theta\colon P\to P'$ in $\cat M_B$ and $\gamma\colon y\to Y(\odot\theta)y'$.
\item \emph{Reindexing.} Along $u\colon A\to B$, $u^*(P,y)=(u^*P,\ Y(u\odot P)y)$.
\item \emph{On right colax maps.} At $(k,\kappa)\colon\cat M\to\cat M'$, the transformation $\Gext_k\colon\Gext_{\cat M}\Rightarrow\Gext_{\cat M'}$ is $\Gext_k(P,y)=(kP,\ Y(\kappa_P)y)$.
\item \emph{On 2-cells.} At $\sigma\colon k\Rightarrow k'$, the modification $\Gext_\sigma$ has components $(\sigma_P,\id)$.
\end{enumerate}
\end{construction}
$\Gext_{\cat M}$ is restriction along $\odot$ followed by the fibrewise Grothendieck construction along $p$. Hence it is the fibred version of the linear functor $\mathrm P_{\cat M}$ of a span~\cite[Thm.~3.2.6]{Web15}, \cite[Ex.~1.7]{GK13}, and it keeps that notation. When the fibres are discrete, it is the polynomial functor of a natural model, whose maps from a representable are the pairs of a type and a map out of the extended context~\cite[Lemma~5]{Awo18}.

\begin{proposition}[The Grothendieck extension is monoidal]\label{prop:gext}
On left fibrant spans with split left legs, $\Gext$ is a monoidal pseudofunctor with the following parts and properties.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Source and target.} $\Gext$ runs from $(\fSpan^{\Rightarrow}(\cat C),\ltimes,\cat C)$ to the endo-2-functors of $[\cat C^{\op},\CAT]$ under composition, whose 1-cells and 2-cells are the pseudonatural transformations and modifications.
\item \emph{Constraints.} $\Gext_{\cat M\ltimes\cat N}\cong\Gext_{\cat N}\sq\Gext_{\cat M}$ and $\Gext_{\cat C}\cong\id$.
\item \emph{Coproducts.} $\Gext$ preserves coproducts, as does each $\Gext_{\cat M}$.
\item \emph{Monads.} $\Gext$ sends pseudomonoids to pseudomonads.
\end{enumerate}
\end{proposition}
\begin{proof}
The fibre of $\cat M\ltimes\cat N$ at $B$ is the Grothendieck construction $\int_{P\in\cat M_B}\cat N_{B\odot P}$, which is split by Lemmas~\ref{lem:comp} and~\ref{lem:pb} since $p_{\cat M}$ and $p_{\cat N}$ are. Since a Grothendieck construction over a Grothendieck construction is that over the composite fibration, the two sides of $\int_{(P,Q)\in(\cat M\ltimes\cat N)_B}Y(B\odot P\odot Q)\cong\int_{P\in\cat M_B}\int_{Q\in\cat N_{B\odot P}}Y((B\odot P)\odot Q)$ agree up to a canonical isomorphism that is natural in $Y$ and $B$ and coherent. The unit constraint exists because the fibres of the identity span are points. On 1-cells, a cartesian $k$ commutes with reindexing up to the canonical isomorphisms $u^*\sq k\cong k\sq u^*$, and these isomorphisms make $\Gext_{k}$ pseudonatural. Because composites of right colax maps go to composites, $\Gext$ is a pseudofunctor. It preserves coproducts because fibres of a coproduct are coproducts of fibres and a Grothendieck construction over a fixed category preserves coproducts of the integrand. Finally, $\Gext$ sends pseudomonoids to pseudomonads because a monoidal pseudofunctor carries the structure 2-cells and axioms of a pseudomonoid along its constraints.
\end{proof}

\subsection{Telescopes as a free monad}\label{sec:grtel}

From here on, $\chi\colon\int S\to\cat M$ is a comprehension equivalence into a display contextad $(\cat M,a)$ on $\cat C$ whose algebra structure $a$ is that of Corollary~\ref{cor:alg}, and $(\chi,\psi,\zeta,e)$ is the adjoint equivalence of Lemma~\ref{lem:adjeq}.

\begin{definition}[Telescopes]\label{def:tele}
$\Tel(\int S)$ is the span of \emph{telescopes} of $S$, which has the following parts.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Objects.} A \emph{telescope} of length $n$ at $B$ is a chain $(B\mid\vec F)=(B\mid F_0,\dots,F_{n-1})$ of $\int S$ whose entries are $F_i\in S(B^{(i)})$ for $0\le i<n$, where $B^{(0)}:=B$ and $B^{(i+1)}:=B^{(i)}.F_i$.
\item \emph{Tower.} The display maps of a telescope form its tower
\begin{equation}\label{eq:tower}
\begin{tikzcd}[column sep=large]
B^{(n)} \arrow[r, "\chi F_{n-1}"] & B^{(n-1)} \arrow[r, "\chi F_{n-2}"] & \cdots \arrow[r, "\chi F_1"] & B^{(1)} \arrow[r, "\chi F_0"] & B^{(0)}.
\end{tikzcd}
\end{equation}
\item \emph{Morphisms.} A morphism $(u_0\mid\vec\tau)$ from $(A\mid G_0,\dots,G_{n-1})$ to $(B\mid F_0,\dots,F_{n-1})$ is a list of morphisms $(u_i,\tau_i)\colon(A^{(i)},G_i)\to(B^{(i)},F_i)$ of $\int S$, with $u_0\colon A\to B$ and $u_{i+1}:=u_i.\tau_i$ for $0\le i<n$.
\item \emph{Fibres.} The fibre $\Tel_S(B)$ at $B$ consists of the telescopes at $B$ and the morphisms with $u_0=\id_B$, and these fibres together form $\Tel_S\colon\cat C^{\op}\to\CAT$.
\end{enumerate}
\end{definition}


\begin{proposition}[Telescopes as a free monad]\label{prop:freemonad}
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Extension of the span of stages.} The Grothendieck extension of the span of stages is the endo-2-functor $\int:=\Gext_{\int S}$ of $[\cat C^{\op},\CAT]$, with $(\int Y)(B)=\int_{F\in S(B)}Y(B.F)$ and $\int1=S$. The bare symbol $\int$ denotes this endo-2-functor, whereas $\int S$ keeps denoting the span of stages.
\item \emph{Free monad.} The free monad $\coprod_n\int^n$ on $\int$ is isomorphic to $\Gext_{\Tel(\int S)}$.
\item \emph{Telescopes.} At $1$ it gives the functor of telescopes $\coprod_n\int^n1\cong\Tel_S$, whose summand $\int^n1$ is the functor of telescopes of length $n$. In turn, the Grothendieck construction of $\Tel_S$ is $\Tel(\int S)$, which is a split fibration over $\cat C$.
\end{enumerate}
\end{proposition}
\begin{proof}
Since the left leg of $\int S$ is split, Proposition~\ref{prop:gext} gives $\Gext_{\Tel(\int S)}\cong\coprod_n\int^n$. The same proposition places every $\Gext_{\cat M}$ in the monoidal 2-category of coproduct-preserving endo-2-functors under composition, and there $\coprod_n\int^n$ is the free monoid on $\int$ by Proposition~\ref{prop:monad}. At $1$, $\Gext_{\cat N}1$ is the functor of fibres of $p_{\cat N}$. Hence $\int^n1$ is the functor of fibres of $(\int S)^{\ltimes n}$, which Definition~\ref{def:tele} calls the telescopes of length $n$. Finally, each $(\int S)^{\ltimes(n+1)}\to(\int S)^{\ltimes n}$ is a pullback of the split fibration $\int S\to\cat C$. Therefore $p_{\Tel(\int S)}$ is split by Lemmas~\ref{lem:comp} and~\ref{lem:pb}, and it is the Grothendieck construction of its fibres because every split fibration is.
\end{proof}

\subsection{The stage contextad and its Kleisli arrows}\label{sec:grctx}

\begin{proposition}[The stage contextad, {\cite[Ex.~3.20, 3.21]{CM24}}]\label{prop:stagectx}
A contextad on $\int S$ making $\chi$ a strict morphism of contextads in the sense of Definition~\ref{def:strictmor} exists and is unique up to unique isomorphism. One choice is the \emph{stage contextad}, which has the following parts. In them $\kappa_\psi$ denotes the top of $e$ from Lemma~\ref{lem:adjeq}.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Unit.} The unit $I^{\int S}:=I^{\cat M}\sq\psi$ is transported along $\psi$ and has colaxator $\varepsilon:=I^{\cat M}\ast\kappa_\psi$.
\item \emph{Multiplication.} The multiplication $\otimes^{\int S}:=(\chi\ltimes\chi)\sq\otimes^{\cat M}\sq\psi$ is transported likewise and has colaxator $\delta:=((\chi\ltimes\chi)\sq\otimes^{\cat M})\ast\kappa_\psi$. It is also denoted $\wsemi$, and like $\sq$ this white semicolon composes in diagrammatic order.
\item \emph{Invertible colaxators.} The components $\varepsilon_B$ and $\delta_{F,G}$ are invertible.
\item \emph{Strict morphism $\chi$.} The unitor of $\chi$ is $I^{\cat M}\ast e$ and its multiplicator is $((\chi\ltimes\chi)\sq\otimes^{\cat M})\ast e$. Hence $\otimes^{\int S}\sq\chi$ is $(\chi\ltimes\chi)\sq\otimes^{\cat M}$ up to $e$, and the latter composes the display maps down the tower. As a pasting diagram and as a string diagram in $\fSpan^{\Rightarrow}(\cat C)$, the multiplicator is
\begin{equation}\label{eq:strongsd}
\begin{tikzcd}
(\int S)\ltimes(\int S) \arrow[r,"\chi\ltimes\chi"] \arrow[d,"\otimes^{\int S}"'] \arrow[dr,phantom,"\cong"] & \cat M\ltimes\cat M \arrow[d,"\otimes^{\cat M}"]\\
\int S \arrow[r,"\chi"'] & \cat M
\end{tikzcd}
\qquad\qquad
\underset{\scriptstyle \otimes^{\int S}\sq\chi}{\tikz[sd=-1.6]{
  \coordinate (m) at (0.5,-1.0);
  \draw[stw] (0,0) to[out=-90,in=120] (m); \draw[stw] (1,0) to[out=-90,in=60] (m);
  \node[dotw] at (m) {};
  \sdchi{c}{0.5,-2.0}
  \draw[stw] (m) -- (c.north); \draw (c.south) -- (0.5,-3.2);
  \sdlab{0}{F}\sdlab{1}{G}}}
\ \cong\
\underset{\scriptstyle (\chi\ltimes\chi)\sq\otimes^{\cat M}}{\tikz[sd=-1.6]{
  \sdchi{c1}{0,-0.9}
  \sdchi{c2}{1.5,-0.9}
  \coordinate (m) at (0.75,-2.2);
  \draw[stw] (0,0) -- (c1.north); \draw[stw] (1.5,0) -- (c2.north);
  \draw (c1.south) to[out=-90,in=120] (m); \draw (c2.south) to[out=-90,in=60] (m);
  \node[dotn] at (m) {}; \draw (m) -- (0.75,-3.2);
  \sdlab{0}{F}\sdlab{1.5}{G}}}
\end{equation}
Here the white dot is the multiplication $\wsemi$ of the stage contextad and the black dot is composition of display maps. The white dot is the \emph{binary dependent sum}, and following Table~\ref{tab:diag} grey wires carry $\int S$ while black wires carry $\cat M$.
\end{enumerate}
\end{proposition}
\begin{proof}
Since $\chi$ is an equivalence by Lemma~\ref{lem:adjeq}, whiskering with $\chi$ is an equivalence of the hom-categories of $\fSpan^{\Rightarrow}(\cat C)$ into $\int S$ and into $\cat M$. Because the coherence of $\cat M$ is the identity, isomorphisms $\lambda$, $\rho$, $\alpha$ of the required types exist, and Lemma~\ref{lem:thin} makes them the only 2-cells of their types. The same lemma proves every axiom of Definition~\ref{def:ctxdcoh}, since each axiom is an equation of 2-cells into $\int S$. Since $\chi$, $\otimes^{\cat M}$ and $I^{\cat M}$ have identity colaxators, the colaxators of $\otimes^{\int S}$ and $I^{\int S}$ are those of $\psi$. The axioms of Definition~\ref{def:strictmor} are equations of 2-cells into $\cat M$, and hence they hold by Lemma~\ref{lem:thin} for $\cat M$. For uniqueness, let $(I',\otimes',\lambda',\rho',\alpha')$ be another such contextad with unitor $\upsilon'$ and multiplicator $m'$. Then the colaxators of $I'$ and $\otimes'$ are $\odot(\upsilon')$ and $\odot(m')$ and hence invertible. Since whiskering with $\chi$ is an equivalence of hom-categories, $I'$ and $\otimes'$ are isomorphic to $I^{\int S}$ and $\otimes^{\int S}$ by unique 2-cells whose whiskerings with $\chi$ are $\upsilon'\sq(I^{\cat M}\ast e^{-1})$ and $m'\sq\bigl(((\chi\ltimes\chi)\sq\otimes^{\cat M})\ast e^{-1}\bigr)$. By Lemma~\ref{lem:thin} they form an isomorphism of pseudomonoids that is compatible with the coherence isomorphisms, the unitors and the multiplicators. Finally, the stage contextad is the contextad of the cited Example~3.20 for the strong sums given by composition of display maps.
\end{proof}

\begin{proposition}[Kleisli arrows are contextful arrows]\label{prop:kleisli}
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Monad.} The extension $\Gext$ makes $\int$ a pseudomonad on $[\cat C^{\op},\CAT]$, which is called the \emph{Grothendieck monad} and whose unit and multiplication are
\[\eta^{\int}:=\Gext_{(I^{\int S},\varepsilon)},\qquad\mu^{\int}:=\Gext_{(\otimes^{\int S},\delta)},\]
composed with the constraints of $\Gext$. In particular, $\eta^{\int}_1=I^{\int S}$ and $\mu^{\int}_1=\wsemi$ on $\int1=S$.
\item \emph{Kleisli is co-Kleisli.} The Kleisli construction $\Kl(\int)$ of $\int$ on representables is the pseudo double category with the following parts.
\begin{enumerate}[label=(\alph*),leftmargin=*]
\item \emph{Objects and tight morphisms.} Those of $\cat C$.
\item \emph{Loose morphisms.} The 1-cells $s\colon\yu B\to\int \yu X$ of $[\cat C^{\op},\CAT]$, drawn as $B\lto X$.
\item \emph{Cells.} The modifications $s\sq\int \yu v\Rightarrow \yu u\sq s'$, from $s$ to $s'\colon\yu B'\to\int\yu X'$ over $u\colon B\to B'$ and $v\colon X\to X'$.
\item \emph{Loose composition.} $s\sq\int t\sq\mu^{\int}_{\yu Z}$, for $t\colon\yu X\to\int\yu Z$.
\item \emph{Loose identities.} $\eta^{\int}_{\yu B}$.
\end{enumerate}
Up to equivalence, the Kleisli 1-cells $\yu B\to\int \yu X$ are the pairs $(F,f)$ of $F\in S(B)$ and $f\colon B.F\to X$, and their Kleisli composites and identities are those of $\coKl(\int S)$. Thus $\Kl(\int)\simeq\coKl(\int S)$ by an equivalence that is the identity on objects and tight morphisms.
\item \emph{Binary dependent sum.} A stage $F\in S(B)$ is the loose arrow $(F,\id)\colon B\lto B.F$, and for $G\in S(B.F)$
\begin{equation}\label{eq:kleisli}
(F,\id)\sq(G,\id)=\bigl(F\wsemi G,\ \delta_{F,G}\colon B.(F\wsemi G)\to(B.F).G\bigr).
\end{equation}
\item \emph{Equivalence.} $\coKl(\chi)\colon\coKl(\int S)\to\coKl(\cat M)$ is an equivalence of pseudo double categories that is the identity on tight data. On loose morphisms it is $\chi\times_{\cat C}\cat C^{\to}$, which $\chi$ induces on the pullbacks of $\odot$ and $\mathrm{dom}$. Its compositor is the multiplicator of $\chi$, and at $(F,\id)$ and $(G,\id)$ this compositor is $e_{\chi G\sq\chi F}\colon(\chi(F\wsemi G),\delta_{F,G})\cong(\chi G\sq\chi F,\id)$.
\end{enumerate}
Here the loose morphisms of $\coKl(\cat M)$ are the spans in $\cat C$ with left leg in $\Dcls$, and its cells are the squares of $\cat M$. In particular, for $\cat M=\cat M^{\mathrm{all}}_{\Dcls}$ it is the double category of spans with left leg in $\Dcls$ of~\cite[Ex.~3.22]{CM24}.
\end{proposition}
\begin{proof}
(i) Since the left leg of the pseudomonoid $\int S$ of Proposition~\ref{prop:stagectx} is split, Proposition~\ref{prop:gext} sends it to this pseudomonad. Its components at $1$ are $I^{\int S}$ and $\wsemi$ because $\Gext$ takes a span to its fibres at $1$. (ii) By the 2-Yoneda lemma, $[\cat C^{\op},\CAT](\yu B,\int \yu X)\simeq(\int \yu X)(B)$, whose objects are the pairs $(F,f)$ with $f\in\cat C(B.F,X)$. Let $t=(G,g)$ with $G\in S(X)$ and $g\colon X.G\to Z$. At the generic element, $\int t$ sends $(F,f)$ to $(F,(f^*G,(f.\id)\sq g))$, which $\mu^{\int}_{\yu Z}$ then sends to $(F\wsemi f^*G,\ \delta_{F,f^*G}\sq(f.\id)\sq g)$. Since $f\odot G=f.\id$, the result is the composite of Definition~\ref{def:ctx}, and likewise $\eta^{\int}$ gives $(I^{\int S}_B,\varepsilon_B)$. At the generic element, a modification $s\sq\int \yu v\Rightarrow \yu u\sq s'$ is a morphism from $(F,f\sq v)$ to $u^*(F',f')$, which amounts to a $\theta\colon F\to u^*F'$ with $f\sq v=\odot(u,\theta)\sq f'$. Hence the cells are those of $\coKl(\int S)$ above $u$. When $S$ is the terminal functor, the stage contextad is a comonad $W$ on $\cat C$ with $\int=W^*$, and then (ii) is the Yoneda isomorphism $[\cat C^{\op},\CAT](\yu B,W^*\yu X)\cong\cat C(WB,X)$. (iii) is the case of (ii) in which $f$ and $g$ are identities. (iv) $\coKl(-)$ is functorial in strict morphisms of contextads with the multiplicator as compositor~\cite[Def.~4.36, after Rem.~4.39]{CM24}. Moreover, the category of loose morphisms of $\coKl(\cat N)$ is the strict pullback $\cat N\times_{\cat C}\cat C^{\to}$ of $\odot$ and the fibration $\mathrm{dom}$. Since $\mathrm{dom}$ is a fibration and hence an isofibration, this strict pullback is a pseudo-pullback, and pseudo-pullbacks are invariant under equivalence of cospans~\cite{JS93}. Therefore $\coKl(\chi)$ is an equivalence on loose morphisms and cells over $\cat C\times\cat C$.
\end{proof}

\section{The dependent sum as a transported algebra}\label{sec:main}

The stage contextad is a pseudo-algebra of the pseudomonad $\Tel$ on $\fSpan^{\cong}(\cat C)$ rather than an algebra in $\EM(\Tel)$, because the structure map of an algebra in $\EM(\Tel)$ has identity colaxators whereas the multiplication of the stage contextad has invertible ones. This pseudomonad acts on 1-cells by powers under $\ltimes$ according to Definition~\ref{def:telcolax}, but its constraints $\varphi_{k,h}$ and $\bar\mu_k$ are identities at strict 1-cells $k$ by Lemmas~\ref{lem:telcons} and~\ref{lem:telpseudo}.

For a pseudomonoid $\cat N$ in $\fSpan^{\Rightarrow}(\cat C)$, the \emph{comb} $\mathrm{comb}^n_{\cat N}\colon\cat N^{\ltimes n}\to\cat N$ is the 1-cell
\[\mathrm{comb}^n_{\cat N}:=\begin{cases}I^{\cat N} & n=0,\\ \id & n=1,\\ (\cat N^{\ltimes(n-2)}\ltimes\otimes^{\cat N})\sq(\cat N^{\ltimes(n-3)}\ltimes\otimes^{\cat N})\sq\cdots\sq\otimes^{\cat N} & n\ge2.\end{cases}\]
For the display contextad the comb recovers the structure map, since $\iota_n\sq a=\mathrm{comb}^n_{\cat M}$ by Corollary~\ref{cor:alg}.


\begin{proposition}[Flattening of telescopes]\label{prop:telcomp}
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Equivalence.} $\Tel(\chi)$ is an equivalence in $\fSpan^{\cong}(\cat C)$ and in particular an equivalence of fibrations over $\cat C$
\begin{equation}\label{eq:bridge}
\Tel(\chi)\colon\Tel\Bigl(\int S\Bigr)\xrightarrow{\ \simeq\ }\Tel(\cat M),
\end{equation}
which restricts to $\Tel_S(B)\simeq\Tel(\cat M)_B$ for each $B\in\cat C$.
\item \emph{Flattening.} $\Tel(\chi)\sq a\colon(\Tel(\int S),\mu)\to(\cat M,a)$ is a cartesian 1-cell of $\EM(\Tel)$ and the transpose of $\chi$ under the free and forgetful 2-adjunction
\[\EM(\Tel)\Bigl(\Bigl(\Tel\Bigl(\int S\Bigr),\mu\Bigr),(\cat M,a)\Bigr)\cong\fSpan_{\mathrm s}(\cat C)\Bigl(\int S,\cat M\Bigr).\]
This transpose is the \emph{flattening}, which is $\chi^{\ltimes n}\sq\mathrm{comb}^n_{\cat M}$ on the $n$-th summand and hence takes a telescope to the composite of its tower~\eqref{eq:tower}. Its composites with $\mathrm{dom}$ and $\mathrm{cod}$ are the legs of $\Tel(\int S)$ from Definition~\ref{def:tele}. As a 1-cell of $\EM(\Tel)$ it moreover satisfies $\mu\sq\Tel(\chi)\sq a=\Tel(\Tel(\chi)\sq a)\sq a$, whose right side flattens the blocks first.
\end{enumerate}
\end{proposition}
\begin{proof}
(i) By Lemma~\ref{lem:adjeq}, $\chi$ is an equivalence in $\fSpan^{\cong}(\cat C)$, and $\ltimes$ is a pseudofunctor there by Definition~\ref{def:lfs}. Hence $\Tel(\chi)=\coprod_n\chi^{\ltimes n}$ is an equivalence in $\fSpan^{\cong}(\cat C)$ with pseudo-inverse $\Tel(\psi)=\coprod_n\psi^{\ltimes n}$ by Lemma~\ref{lem:telcons}, and in particular an equivalence of fibrations over $\cat C$. (ii) The transpose of $\chi$ under $\mathrm{Fr}\dashv U$ is the 1-cell $\Tel(\chi)\sq a$ of $\EM(\Tel)$, which gives~\eqref{eq:blocks} on blocks. Since $\iota_n\sq a=\mathrm{comb}^n_{\cat M}$, on the $n$-th summand it is $\chi^{\ltimes n}\sq\mathrm{comb}^n_{\cat M}$, which composes the tower because $\otimes^{\cat M}$ is the composition of display maps by Proposition~\ref{prop:dispctx}. Finally, its composites with $\mathrm{dom}=\odot_{\cat M}$ and $\mathrm{cod}=p_{\cat M}$ are the legs of $\Tel(\int S)$ because $\Tel(\chi)$ and $a$ are 1-cells of spans.
\end{proof}



\begin{theorem}[The dependent sum is the transported structure map]\label{thm:main}
Let $\Sigma:=\Tel(\chi)\sq a\sq\psi\colon\Tel(\int S)\to\int S$ in $\fSpan^{\cong}(\cat C)$ be the \emph{dependent sum}. Its value at a telescope $(B\mid F_0,\dots,F_{n-1})$ is denoted $F_0\wsemi\cdots\wsemi F_{n-1}$, and its pseudo-algebra structure uses $\hat e:=\varphi_{\psi,\chi}\sq\Tel(e)\colon\Tel(\psi)\sq\Tel(\chi)\Rightarrow\id$.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Pseudo-algebra.} Let $\bar\Sigma:=\bigl(\Tel^2(\chi)\sq\Tel(a)\bigr)\ast\hat e\ast(a\sq\psi)\colon\Tel(\Sigma)\sq\Sigma\Rightarrow\mu\sq\Sigma$. Then $(\int S,\Sigma,\bar\Sigma,\zeta)$ is the pseudo-algebra transported from $(\cat M,a)$ along $\chi$. Moreover, $(\chi,\bar\chi)$ with $\bar\chi:=\bigl(\Tel(\chi)\sq a\bigr)\ast e^{-1}$ is an equivalence of pseudo-algebras $(\int S,\Sigma)\simeq(\cat M,a)$, and $\bar\chi$ fills the square
\begin{equation}\label{eq:three}
\begin{tikzcd}[column sep=huge]
\Tel(\int S) \arrow[r, "\Tel(\chi)"] \arrow[d, "\Sigma"'] \arrow[dr, phantom, "\overset{e}{\cong}"] & \Tel(\cat M) \arrow[d, "a"] \\
\int S \arrow[r, "\chi"'] & \cat M
\end{tikzcd}
\end{equation}
which reads in stripe and string diagrams as
\[
\underset{\scriptstyle\Sigma\sq\chi}{\sdSigChi}\qquad\overset{e}{\cong}\qquad\underset{\scriptstyle\Tel(\chi)\sq a}{\sdTelChiA}\ .
\]
Hence $\Sigma\sq\chi$ is the flattening $\Tel(\chi)\sq a$ of Proposition~\ref{prop:telcomp}(ii), up to $e$.
\item \emph{Contextad.} Along $\iota_0$ and $\iota_2$, $\Sigma$ restricts to $I^{\int S}$ and $\otimes^{\int S}$, with their colaxators.
\item \emph{Grothendieck monad.} On the $n$-th summand $\Sigma\cong\mathrm{comb}^n_{\int S}$. Hence $\Gext_{\Sigma}\colon\coprod_n\int^n\to\int$ is isomorphic to the iterated multiplication $\coprod_n\mu^{(n)}$, where $\mu^{(n)}:=\int^{n-2}\mu^{\int}\sq\cdots\sq\int\mu^{\int}\sq\mu^{\int}\colon\int^n\to\int$ for $n\ge2$ while $\mu^{(0)}:=\eta^{\int}$ and $\mu^{(1)}:=\id$.
\item \emph{Uniqueness.} $\bar\Sigma$, $\zeta$, $\bar\chi$ and the coherence isomorphisms $\lambda$, $\rho$, $\alpha$ of the stage contextad are the only 2-cells of their types.
\end{enumerate}
\end{theorem}
\begin{proof}
(i) $\Tel$ is a pseudomonad on $\fSpan^{\cong}(\cat C)$ by Lemma~\ref{lem:telpseudo}, and its constraints are identities at the strict 1-cells $\chi$ and $a$ by Lemma~\ref{lem:telcons}. Since $(\chi,\psi,\zeta,e)$ also lies in $\fSpan^{\cong}(\cat C)$ by Lemma~\ref{lem:adjeq}, the construction of Lemma~\ref{lem:transport} applies and gives the stated 2-cells with their types, where $\varphi_{\psi,\chi}$ is the constraint of $\Tel$. Every axiom of Definition~\ref{def:psalg} for them is an equation of 2-cells into $\int S$ or $\cat M$ and therefore holds by Lemma~\ref{lem:thin}. In string diagrams $\bar\chi$ is the isomorphism displayed in (i). (ii) Along $\iota_0$ and $\iota_2$, $\Tel(\chi)$ restricts to the identity and to $\chi\ltimes\chi$, while $a$ restricts to $I^{\cat M}$ and $\otimes^{\cat M}$ by Corollary~\ref{cor:alg}. Hence $\Sigma$ restricts to the stage contextad of Proposition~\ref{prop:stagectx} with its colaxators. (iii) On the $n$-th summand, $e$ gives $\Sigma\sq\chi\cong\chi^{\ltimes n}\sq a$. Likewise the unitor and the multiplicators of $\chi$ give $\mathrm{comb}^n_{\int S}\sq\chi\cong\chi^{\ltimes n}\sq\mathrm{comb}^n_{\cat M}$ because they are whiskerings of $e$, and the right side is $\chi^{\ltimes n}\sq a$ by Corollary~\ref{cor:alg}. Since whiskering with $\chi$ is an equivalence of hom-categories, $\Sigma\cong\mathrm{comb}^n_{\int S}$ on the $n$-th summand, and this isomorphism is unique by Lemma~\ref{lem:thin}. Moreover, $\Gext$ takes $I^{\int S}$ and $\otimes^{\int S}$ to $\eta^{\int}$ and $\mu^{\int}$ by Proposition~\ref{prop:kleisli}(i), and it takes $\Tel(\int S)$ to $\coprod_n\int^n$ up to its constraints by Proposition~\ref{prop:freemonad}. Because $\Gext$ is monoidal by Proposition~\ref{prop:gext}, it takes $\mathrm{comb}^n_{\int S}$ to $\mu^{(n)}$ on the $n$-th summand and $\Sigma$ to $\coprod_n\mu^{(n)}$. (iv) is Lemma~\ref{lem:thin}, whose proof applies to 2-cells into $\int S$ or $\cat M$ between 1-cells with invertible colaxators.
\end{proof}

Thus $\Sigma$ collapses each summand $(\int S)^{\ltimes n}$ to $\int S$ just as $\wsemi$ collapses $(\int S)^{\ltimes2}$, and up to isomorphism $\Gext$ takes the two collapses to $\coprod_n\mu^{(n)}$ and to $\mu^{\int}$. The theorem holds for every normal cleavage of $\cat M$ and every category $\cat C$ when $S$ is valued in $\CAT$.

The Kleisli construction gives a second model of the transported pseudo-algebra in which the stages are loose arrows.

\begin{proposition}[A Kleisli model of the transported algebra]\label{prop:klalg}
Let $\cat L_{\cong}$ be the span with the following parts.
\begin{enumerate}[label=(\alph*),leftmargin=*]
\item \emph{Apex.} The full subcategory of the arrows with invertible bodies in $\cat L=\int S\times_{\cat C}\cat C^{\to}$. Here $\cat L$ is the strict pullback of $\odot_{\int S}$ and $\mathrm{dom}$, which is the category of loose morphisms of $\Kl(\int)\simeq\coKl(\int S)$.
\item \emph{Left leg.} The projection to $\int S$ followed by $p_{\int S}$.
\item \emph{Right leg.} The projection to $\cat C^{\to}$ followed by $\mathrm{cod}$.
\item \emph{Cleavage.} The chosen lifts of $\int S$, with identity bodies at their domains.
\end{enumerate}
Then the following hold.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Pseudo-algebra.} With the loose identities and the Kleisli composite of $\coKl(\int S)$, $\cat L_{\cong}$ is a pseudomonoid in $(\fSpan_{\mathrm s}(\cat C),\ltimes)$. Hence it is a pseudo-algebra $(\cat L_{\cong},b,\bar b,\id)$ of $\Tel$ by the argument of Corollary~\ref{cor:alg}, and its structure map $b$ is the 1-cell $\mathrm{comb}^n_{\cat L_{\cong}}$ of $\fSpan_{\mathrm s}(\cat C)$ on the $n$-th summand. Its 2-cell $\bar b$ is built from the associators of $\coKl(\int S)$.
\item \emph{Equivalence.} Let $j\colon\int S\to\cat L_{\cong}$ be induced on the pullback by $\id_{\int S}$ and $\odot_{\int S}\sq\Delta$, where $\Delta\colon\cat C\to\cat C^{\to}$ is the diagonal. Then $j$ is an adjoint equivalence of pseudo-algebras $(\int S,\Sigma)\simeq(\cat L_{\cong},b)$, and on the second summand its 2-cell $\bar j$ has the components $\bar j_{(F,G)}:=(\id,\delta_{F,G})\colon(F\wsemi G,\id)\cong(F\wsemi G,\delta_{F,G})$.
\end{enumerate}
\end{proposition}
\begin{proof}
A morphism $(\theta,v)\colon(F,f)\to(F',f')$ of $\cat L_{\cong}$ has $\odot(\theta)=f\sq v\sq f'^{-1}$ and is hence determined by its legs because Lemma~\ref{lem:thin} holds for $\int S$. Therefore Lemma~\ref{lem:thin} applies to $\cat L_{\cong}$. (i) The Kleisli composite $(F\wsemi f^*G,\ \delta_{F,f^*G}\sq(f.\id)\sq g)$ of two arrows of $\cat L_{\cong}$ has an invertible body, since $\delta_{F,f^*G}$ is invertible and $f.\id$ is the image of a lift along an isomorphism. This composite commutes strictly with both legs and preserves the chosen lifts. Moreover, the associators and unitors of $\coKl(\int S)$ are identities on both legs and hence 2-cells of $\fSpan_{\mathrm s}(\cat C)$. Thus $\cat L_{\cong}$ is a pseudomonoid there, and on the $n$-th summand of $\Tel(\cat L_{\cong})=\coprod_n\cat L_{\cong}^{\ltimes n}$ its structure map $b$ is $\mathrm{comb}^n_{\cat L_{\cong}}$ with $\eta\sq b=\id$ by the argument of Corollary~\ref{cor:alg}. The associators give $\bar b$, and the axioms of Definition~\ref{def:psalg} hold by Lemma~\ref{lem:thin}. (ii) $j$ is a 1-cell of $\fSpan_{\mathrm s}(\cat C)$, and it is full and faithful on fibres because the morphisms $(F,\id)\to(F',\id)$ are those of $\int S$. Since moreover every $(F,f)$ is isomorphic to $(F,\id)$ by $(\id,f)$, $j$ is an equivalence in $\fSpan^{\cong}(\cat C)$ with the projection to $\int S$ as pseudo-inverse and with colaxator $f$. By~\eqref{eq:kleisli}, $\Tel(j)\sq b$ and $\Sigma\sq j$ differ by the bodies $\delta$, which give $\bar j$. Finally, the axioms of $\bar j$ and those of the adjoint equivalence hold by Lemma~\ref{lem:thin}.
\end{proof}

\section*{Acknowledgements}
The author thanks Masayuki Hiyama for discussions.

\addtocontents{toc}{\protect\setcounter{tocdepth}{1}}
\renewcommand{\thesection}{A}\setcounter{section}{1}\setcounter{theorem}{0}\setcounter{equation}{0}
\section*{Appendix}\label{app:background}

\subsection*{Conventions}

\begin{enumerate}[label=(\alph*),leftmargin=*]
\item Double categories are pseudo and normalised unless called strict. Their tight morphisms are vertical, whereas their loose morphisms are horizontal and drawn $\lto$.
\item Composition is diagrammatic, and $f\sq g$ means $f$ then $g$. Whiskering is likewise denoted $\ast$ or $\sq$.
\item $\CAT$ and $\Cat$ are the 2-categories of large and small categories, and $\Set$ is the category of small sets.
\item Fonts distinguish dimensions. Thus 2-categories such as $\Cat$ and $\fSpan_{\mathrm s}(\cat C)$ are bold, whereas 1-categories such as $\cat C$ and $\cat M$ are script unless they are named like $\Set$, which is upright. Classes of morphisms such as $\Dcls$ are sans-serif.
\end{enumerate}

\subsection*{Diagram calculi}

Pasting diagrams and string diagrams are the two kinds of diagram in this paper, and Table~\ref{tab:diag} matches them row by row. Triangle pictures are no third kind, since they draw pasting diagrams of spans. \emph{Pasting diagrams} are commutative diagrams in a category or a 2-category, and they prove properties of single objects and morphisms. Specifically, display maps, squares, pullbacks and towers are pasted in $\cat C$, whereas spans and their composites are pasted in $\CAT$ and squares of 1-cells in $\fSpan^{\cong}(\cat C)$ or $\EM(\Tel)$. The composite of a pasting diagram is unique by the pasting theorem~\cite[Thm.~3.3.7]{JY21}.

\emph{String diagrams} are drawn in the monoidal 2-category $(\fSpan_{\mathrm s}(\cat C),\ltimes,\cat C)$ of Lemma~\ref{lem:monoidal} and Definition~\ref{def:lfs}, or in $\fSpan^{\Rightarrow}(\cat C)$ when a 1-cell has a non-identity colaxator. They prove equations and isomorphisms between composites of 1-cells, such as the laws of monoids and algebras and their transport. Each such equation is therefore drawn twice, first as a pasting diagram and then as a string diagram that reads the same composites. In a string diagram a wire is a left fibrant span labelled by a generic object of it, and juxtaposition of wires is $\ltimes$ with the empty diagram as its unit $\cat C$. Boxes are 1-cells, and a dot with only an output wire is the unit $I\colon\cat C\to\cat M$ of a contextad. This unit is a 1-cell, whereas the unit $\cat C$ of $\ltimes$ is an object.

In string diagrams $\Tel$ is a shaded stripe around the wires it is applied to, just as McCurdy drew monoidal functors~\cite[Sec.~3]{McC12}. His rules are stated for monoidal functors, whereas Proposition~\ref{prop:sound}(ii) justifies the stripes for $\Tel$ on $\ltimes$. Hence $\Tel(k)$ is the box $k$ inside a stripe, and the box $\mu$ merges two nested stripes into one. Likewise the box $\eta$ opens a stripe, while the box of an algebra $a$ closes one. More generally, a stripe opened around $n$ wires is the injection $\iota_n$ of $\cat M^{\ltimes n}$ with $\eta=\iota_1$, and the inner stripes of $\Tel^2(\cat M)$ are its blocks.

\emph{Triangle pictures} are pasting diagrams of spans in $\CAT$ in which a white dot is $\cat C$ and a black dot is a category such as the apex $\cat M$ of a span or an iterated pullback $\cat M^{\ltimes n}$. Edges are functors, and the legs $p$ and $\odot$ and the projections are plain lines running downwards. Thus a composite $\cat M^{\ltimes n}$ is the lattice of its strict pullback squares inside the similar triangle of width $n$. A 1-cell is an arrow between two pictures on the same feet, and its colaxator is left implicit. For display maps and stages the legs carry a 2-cell $\odot\Rightarrow p$ over $\id_{\cat C}$, which is drawn as a double line. On $\cat M$ this 2-cell is $\mathrm{dom}\Rightarrow\mathrm{cod}$, and on $\int S$ it is $d$ with $d_F=\chi F$. In both cases its components are display maps, and it fills the triangle in white for display maps and in grey for stages. The two 2-cells satisfy $d=\chi\ast(\mathrm{dom}\Rightarrow\mathrm{cod})$, whereas a general left fibrant span carries no such 2-cell and its triangles stay unfilled. An object is drawn in $\cat C$ as the component of this 2-cell at it, which is its display map. Hence a telescope is drawn as its tower~\eqref{eq:tower}, and pasting the 2-cells of a pyramid composes display maps. By Proposition~\ref{prop:kleisli} the result is the loose composite of the arrows $(\chi F,\id)$ in $\coKl(\cat M)$. Finally, figures that juxtapose kinds follow Table~\ref{tab:diag} row by row.

\begin{proposition}[Soundness of the diagrams]\label{prop:sound}
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{String diagrams.} A string diagram is read as the composite of its layers from top to bottom, where each layer is the $\ltimes$ of the boxes and wires at one height. In $\fSpan_{\mathrm s}(\cat C)$ any two layerings of a diagram give the same 1-cell up to the canonical isomorphisms of iterated pullbacks. In $\fSpan^{\Rightarrow}(\cat C)$ they give isomorphic 1-cells instead, and the isomorphism is unique when the 1-cells lie in $\fSpan^{\cong}(\cat C)$ and the codomain satisfies Lemma~\ref{lem:thin}.
\item \emph{Stripes.} For a choice of lengths of the stripes, erasing the stripes repeats a box inside a stripe on each of its wires and reads $\eta$ as $\iota_1$ and $\mu$ as concatenation. Two stripe diagrams with the same boundary then denote the same 1-cell of $\fSpan_{\mathrm s}(\cat C)$ when they agree after erasing the stripes for every choice of lengths.
\end{enumerate}
\end{proposition}
\begin{proof}
(i) Lying above one another along a wire partially orders the boxes of a diagram, and a layering is a linear extension of this order. Two linear extensions are joined by exchanges of adjacent incomparable boxes as in bubble sort, and such boxes lie on disjoint wires. Since $\ltimes$ is a 2-functor on $\fSpan_{\mathrm s}(\cat C)$ by Definition~\ref{def:endospan}(iv), $(k\ltimes\cat N)\sq(\cat M'\ltimes h)=k\ltimes h=(\cat M\ltimes h)\sq(k\ltimes\cat N')$, and hence each exchange is an equality there. The canonical isomorphisms of iterated pullbacks are unique and hence satisfy the coherence axioms. The argument is thereby the planar case of the theorem of Joyal and Street~\cite[Thm.~1.2]{JS91}, and Selinger states this planar case in~\cite[Thm.~3.1]{Sel11}. By Definition~\ref{def:lfs}, $\ltimes$ is only a pseudofunctor on $\fSpan^{\Rightarrow}(\cat C)$, and there an exchange is its invertible constraint. The cartesian $h$ induces this constraint by $h(\kappa_P^*Q)\cong\kappa_P^*(hQ)$, and its uniqueness is Lemma~\ref{lem:thin}. (ii) Since $\ltimes$ preserves coproducts in each variable by Lemma~\ref{lem:monoidal}, a $\ltimes$ of iterated $\Tel$s is the coproduct of the $\ltimes$-powers indexed by the lengths of the stripes. By the universal property of the coproduct, a 1-cell out of it is determined by its restrictions along the coproduct injections, along which $\Tel(k)$ restricts to $k^{\ltimes n}$ and $\mu$ to the concatenation isomorphism of Lemma~\ref{lem:tuples}(ii). Likewise $\eta$ is $\iota_1$, and a stripe opened by $\iota_n$ restricts to its summand. The restricted diagrams are therefore those of the statement, and (i) compares them.
\end{proof}

\begin{table}[htb]\centering\small\setlength{\tabcolsep}{4pt}
\renewcommand{\arraystretch}{1.15}
\begin{tabularx}{\textwidth}{@{}>{\raggedright\arraybackslash}p{33mm}>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}X@{}}
\toprule
& Pasting diagram & Triangle picture, pasting in $\CAT$ & String diagram\\
\midrule
Lives in & $\cat C$, $\CAT$ or a 2-category & $\CAT$, over the feet & $(\fSpan_{\mathrm s}(\cat C),\ltimes,\cat C)$\\
Left fibrant span $\cat M$ & span $\cat C\xleftarrow{p}\cat M\xrightarrow{\odot}\cat C$ & apex with legs $p$, $\odot$, unfilled & wire\\
Composite $\cat M\ltimes\cat N$ & strict pullback~\eqref{eq:ltimes} & lattice of pullback squares~\eqref{eq:pyramid} & juxtaposition\\
1-cell $k$ & map of spans & arrow between pictures on the same feet & box\\
Multiplication $\otimes$ & vertical pasting for display maps~\eqref{eq:vpaste} & arrow from a pyramid of two to one triangle & dot with two inputs\\
Stage, display map & $F\in S(B)$, $P\colon E\to B$ & 2-cell $d$ or $\mathrm{dom}\Rightarrow\mathrm{cod}$, grey or white fill & grey, black wire\\
Telescope monad $\Tel$ & $\coprod_n\cat M^{\ltimes n}$ & a pyramid for each summand & shaded stripe\\
Used for & pullbacks, squares, towers & spans, their composites and 2-cells & laws of monoids, algebras and transport\\
Justified by & \multicolumn{2}{l}{pasting theorem~\cite[Thm.~3.3.7]{JY21}} & Proposition~\ref{prop:sound}\\
\bottomrule
\end{tabularx}
\caption{The two kinds of diagram, where triangle pictures draw pasting diagrams of spans.}\label{tab:diag}
\end{table}



\subsection*{Fibrations}\label{sec:fibgloss}

A functor $P\colon\cat E\to\cat B$ is read as a family of categories indexed by $\cat B$, and its member at $b\in\cat B$ is the \emph{fibre} $\cat E_b$, which is the strict pullback of $P$ along $b\colon1\to\cat B$. A fibration moreover lets objects be pulled back along morphisms of the base, and a cleavage fixes how.

\begin{definition}[Fibration, {\cite[Def.~2.2.1]{LR20}}]\label{def:fib}
Let $P\colon\cat E\to\cat B$ be a functor.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Cartesian morphisms.} A morphism $g\colon x\to y$ of $\cat E$ is \emph{cartesian} when, for every $z\in\cat E$, the map
\[(-\sq g,P)\colon\cat E(z,x)\to\cat E(z,y)\times_{\cat B(Pz,Py)}\cat B(Pz,Px)\]
is a bijection. Equivalently, every $h\colon z\to y$ with $Ph=w\sq Pg$ factors uniquely as $h=h'\sq g$ with $Ph'=w$.
\item \emph{Lifts.} A \emph{lift} of $u\colon c\to Py$ at $y$ is a cartesian $g\colon x\to y$ with $Pg=u$, and it is unique up to a unique isomorphism in the fibre at $c$.
\item \emph{Fibrations.} $P$ is a \emph{fibration} when every $u\colon c\to Py$ has a lift at $y$.
\item \emph{Cleavages.} A \emph{cleavage} assigns to every $u$ and every $y$ a \emph{chosen lift} $\tilde u_y\colon u^*y\to y$ of $u$ at $y$, and a fibration with a cleavage is \emph{cloven}. Reindexing along $u\colon c\to b$ then sends $y\in\cat E_b$ to $u^*y\in\cat E_c$, and the factorisation of~(i) makes it a functor $u^*$ between the fibres.
\item \emph{Normal and split cleavages.} A cleavage is \emph{normal} when the chosen lifts of identities are identities. Then $\widetilde{(\id_b)}_y=\id_y$ and hence $\id_b^*=\id$. It is \emph{split} when in addition chosen lifts compose as $\widetilde{(v\sq u)}_y=\tilde v_{u^*y}\sq\tilde u_y$ for $v\colon d\to c$, and then $(v\sq u)^*=u^*\sq v^*$.
\item \emph{Cartesian functors.} A functor over $\cat B$ between fibrations is \emph{cartesian} when it preserves cartesian morphisms.
\end{enumerate}
\end{definition}
Cartesian morphisms compose, and those above identities are the isomorphisms. Since lifts are unique up to unique isomorphism, any cartesian morphism differs from the chosen lift by an isomorphism above an identity~\cite[Sec.~2]{Str23}.

\begin{lemma}[Composite fibrations, {\cite[Lemma~1.5.5]{Jac99}}]\label{lem:comp}
For cloven fibrations $\cat E\xrightarrow{P}\cat D\xrightarrow{Q}\cat B$, $P\sq Q$ is a fibration with the composite cleavage, which is split if $P$ and $Q$ are. A morphism $g$ of $\cat E$ is then $(P\sq Q)$-cartesian if and only if $g$ is $P$-cartesian and $P(g)$ is $Q$-cartesian.
\end{lemma}
\begin{lemma}[Pullback fibrations, {\cite[Lemma~1.5.1]{Jac99}}]\label{lem:pb}
For a cloven fibration $P\colon\cat E\to\cat B$ and $U\colon\cat A\to\cat B$, $\cat A\times_{\cat B}\cat E\to\cat A$ is a fibration that is split if $P$ is, and its cartesian morphisms are the $(u,g)$ with $g$ cartesian.
\end{lemma}
\subsection*{Coherence of contextads}\label{app:coh}

\begin{definition}[Coherence of a contextad]\label{def:ctxdcoh}
For a contextad (Definition~\ref{def:ctxd}), the coherence data are the following.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Coherence.} Invertible 2-cells $\lambda\colon\id_{\cat M}\Rightarrow(I\ltimes\cat M)\sq\otimes$, $\rho\colon(\cat M\ltimes I)\sq\otimes\Rightarrow\id_{\cat M}$ and $\alpha\colon(\cat M\ltimes\otimes)\sq\otimes\Rightarrow(\otimes\ltimes\cat M)\sq\otimes$ of $\fSpan^{\Rightarrow}(\cat C)$, up to the unitors and associator of $\ltimes$. For $A\in\cat C$, $P\in\cat M_A$, $Q\in\cat M_{A\odot P}$ and $R\in\cat M_{A\odot P\odot Q}$, Definition~\ref{def:lfs}(iv) gives their components $\lambda_P\colon P\cong I_A\otimes\varepsilon_A^*P$, $\rho_P\colon P\otimes I_{A\odot P}\cong P$ and $\alpha_{P,Q,R}\colon P\otimes(Q\otimes R)\cong(P\otimes Q)\otimes\delta_{P,Q}^*R$.
\item \emph{Axioms.} Those of~\cite[Def.~3.15]{CM24}, which are equations of 2-cells into $\cat M$ relating $\lambda$, $\rho$, $\alpha$ with $\varepsilon$ and $\delta$ and include the pentagon and triangle up to reindexing.
\end{enumerate}
\end{definition}

\subsection*{Telescopes along right colax maps}

The pseudo-algebra structure of Theorem~\ref{thm:main} needs $\Tel$ as a pseudomonad on $\fSpan^{\cong}(\cat C)$, which the following lemmas construct on normally cloven spans such as $\int S$, a display span and their powers.

\begin{definition}[$\Tel$ on right colax maps]\label{def:telcolax}
Let $\cat N$ and $\cat N'$ be normally cloven, and let $(k,\kappa)\colon\cat N\to\cat N'$ and $\sigma\colon(k,\kappa)\Rightarrow(k',\kappa')$ lie in $\fSpan^{\cong}(\cat C)$. All powers below are taken under the pseudofunctor $\ltimes$ of Definition~\ref{def:lfs} and bracketed to the left.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{On 1-cells.} $\Tel(k):=\coprod_n(k,\kappa)^{\ltimes n}$, which sends a chain $(A\mid P_0,\dots,P_{n-1})$ to $(A\mid c_0^*kP_0,\dots,c_{n-1}^*kP_{n-1})$.
\item \emph{Colaxator.} The colaxator of $\Tel(k)$ is $c_n$, where the maps $c_i$ are defined recursively for $0\le i<n$ by
\[c_0:=\id_A,\qquad c_{i+1}:=(c_i\odot'kP_i)\sq\kappa_{P_i}\colon A\odot'c_0^*kP_0\odot'\cdots\odot'c_i^*kP_i\to A\odot P_0\odot\cdots\odot P_i.\]
\item \emph{On 2-cells.} $\Tel(\sigma):=\coprod_n\sigma^{\ltimes n}$.
\end{enumerate}
\end{definition}

\begin{lemma}[$\Tel$ is a pseudofunctor on colax maps]\label{lem:telcons}
On normally cloven left fibrant spans, $\Tel$ is a pseudofunctor on $\fSpan^{\cong}(\cat C)$ that extends the 2-functor of Definition~\ref{def:telemonad} and has the following constraints.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item \emph{Composition.} For $k\colon\cat N\to\cat N'$ and $h\colon\cat N'\to\cat N''$, invertible 2-cells $\varphi_{k,h}\colon\Tel(k)\sq\Tel(h)\Rightarrow\Tel(k\sq h)$.
\item \emph{Multiplication.} $\mu$ is pseudonatural, with invertible constraints $\bar\mu_k\colon\Tel^2(k)\sq\mu\Rightarrow\mu\sq\Tel(k)$.
\item \emph{Unit.} $\eta$ is strictly natural, $\eta\sq\Tel(k)=k\sq\eta$ for every $k$.
\item \emph{Strict 1-cells.} $\varphi_{k,h}$ and $\bar\mu_k$ are identities when $k$ is a 1-cell of $\fSpan_{\mathrm s}(\cat C)$.
\end{enumerate}
\end{lemma}
\begin{proof}
Since $\fSpan^{\cong}(\cat C)$ is closed under the pseudofunctor $\ltimes$ by Definition~\ref{def:lfs}, the powers are 1-cells. The composition constraints of $\ltimes$ then give those of the powers, and their coproduct over $n$ is $\varphi_{k,h}$. This coproduct is formed in $\fSpan^{\Rightarrow}(\cat C)$ because coproducts in $\CAT$ are coproducts there by Lemma~\ref{lem:monoidal}, and a functor, a transformation or a colaxator out of a coproduct is the family of its restrictions along the coproduct injections. Likewise the concatenation isomorphisms of Lemma~\ref{lem:tuples}(ii) are composites of associators and unitors of the monoidal bicategory $\fSpan^{\Rightarrow}(\cat C)$, and their coproduct is $\mu$ because $\ltimes$ preserves coproducts. Their pseudonaturality constraints at $k$ in turn give $\bar\mu_k$ when summed over the blocks. On strict 1-cells $\ltimes$ is the 2-functor of Definition~\ref{def:endospan}(iv), and then every $c_i$ is an identity, as is reindexing along it. Hence $\Tel(k)$ is that of Definition~\ref{def:telemonad}, and the constraints are identities. Finally $(k,\kappa)^{\ltimes1}=(k,\kappa)$ gives $\eta\sq\Tel(k)=k\sq\eta$.
\end{proof}

\begin{lemma}[$\Tel$ is a pseudomonad on colax maps]\label{lem:telpseudo}
On normally cloven left fibrant spans, $(\Tel,\eta,\mu)$ is a pseudomonad on $\fSpan^{\cong}(\cat C)$ with identity associativity and unit modifications, extending the 2-monad of Definition~\ref{def:telemonad}.
\end{lemma}
\begin{proof}
By Lemma~\ref{lem:telcons}, $\Tel$ is a pseudofunctor, $\mu$ is pseudonatural and $\eta$ is strictly natural. Since $\mu$ and $\eta$ are 1-cells of $\fSpan_{\mathrm s}(\cat C)$ and $\Tel$ is the 2-functor of Definition~\ref{def:telemonad} there, the laws $\Tel(\mu)\sq\mu=\mu\sq\mu$ and $\Tel(\eta)\sq\mu=\id=\eta\sq\mu$ hold on the nose. The remaining axioms are the coherence of $\varphi_{k,h}$ and $\bar\mu_k$ and the modification axioms of the identities, and they are equations between composites of the constraint 2-cells. At a chain $(A\mid P_0,\dots,P_{n-1})$ each such 2-cell is a morphism of chains $(\id_A\mid\theta_0,\dots,\theta_{n-1})$ whose entry $\theta_i$ lies above $u_i$, with $u_0=\id_A$ and $u_{i+1}=u_i\odot\theta_i$. These $u_i$ are isomorphisms. Moreover, source and target share an underlying composite cartesian functor $K$, and their entries carry cartesian morphisms to $K(P_i)$ with which $\theta_i$ commutes. Since vertical composites, whiskerings and images under $\Tel$ of such 2-cells are again of this form, induction on $i$ shows that each $\theta_i$ is the unique morphism above $u_i$ that commutes with the cartesian morphism of its target by Definition~\ref{def:fib}(i). Hence any two parallel composites agree.
\end{proof}

\begin{thebibliography}{CLPS22}
\raggedright

\bibitem[ASS25]{ASS25}
N.~Arkor, P.~Saville, A.~Slattery.
\newblock Bicategories of algebras for relative pseudomonads.
\newblock Preprint, \href{https://arxiv.org/abs/2501.12510}{arXiv:2501.12510}, 2025.

\bibitem[Awo18]{Awo18}
S.~Awodey.
\newblock Natural models of homotopy type theory.
\newblock \emph{Math.~Struct.~Comput.~Sci.} 28(2):241--286, 2018. \href{https://arxiv.org/abs/1406.3219}{arXiv:1406.3219}.

\bibitem[ALN24]{ALN24}
B.~Ahrens, P.~LeFanu Lumsdaine, P.~R.~North.
\newblock Comparing semantic frameworks for dependently-sorted algebraic theories.
\newblock Preprint, \href{https://arxiv.org/abs/2412.19946}{arXiv:2412.19946}, 2024.

\bibitem[AN18]{AN18}
S.~Awodey, C.~Newstead.
\newblock Polynomial pseudomonads and dependent type theory.
\newblock Preprint, \href{https://arxiv.org/abs/1802.00997}{arXiv:1802.00997}, 2018.

\bibitem[BKP89]{BKP89}
R.~Blackwell, G.~M.~Kelly, A.~J.~Power.
\newblock Two-dimensional monad theory.
\newblock \emph{J.~Pure Appl.~Algebra} 59(1), 1--41, 1989.

\bibitem[Boc21]{Boc21}
R.~Bocquet.
\newblock Strictification of weakly stable type-theoretic structures using generic contexts.
\newblock Preprint, \href{https://arxiv.org/abs/2111.10862}{arXiv:2111.10862}, 2021.

\bibitem[Car86]{Car86}
J.~Cartmell.
\newblock Generalised algebraic theories and contextual categories.
\newblock \emph{Ann.~Pure Appl.~Logic} 32, 209--243, 1986.

\bibitem[CE24]{CE24}
G.~Coraglia, J.~Emmenegger.
\newblock A 2-categorical analysis of context comprehension.
\newblock Preprint, \href{https://arxiv.org/abs/2403.03085}{arXiv:2403.03085}, 2024.

\bibitem[CLPS22]{CLPS22}
G.~S.~H.~Cruttwell, M.~J.~Lambert, D.~A.~Pronk, M.~Szyld.
\newblock Double fibrations.
\newblock \emph{Theory Appl.~Categ.} 38(35), 1326--1394, 2022.
\newblock Numbers refer to the journal version. Its Definition~2.25 is Definition~2.23 of \href{https://arxiv.org/abs/2205.15240}{arXiv:2205.15240}.

\bibitem[CM24]{CM24}
M.~Capucci, D.~J.~Myers.
\newblock Contextads as wreaths; Kleisli, Para, and Span constructions as wreath~products.
\newblock Preprint, \href{https://arxiv.org/abs/2410.21889}{arXiv:2410.21889}, 2024.

\bibitem[dB91]{dB91}
N.~G.~de~Bruijn.
\newblock Telescopic mappings in typed lambda calculus.
\newblock \emph{Inform.~and Comput.} 91(2), 189--204, 1991.

\bibitem[GK13]{GK13}
N.~Gambino, J.~Kock.
\newblock Polynomial functors and polynomial monads.
\newblock \emph{Math.~Proc.~Cambridge Philos.~Soc.} 154(1):153--192, 2013. \href{https://arxiv.org/abs/0906.4931}{arXiv:0906.4931}.

\bibitem[Jac99]{Jac99}
B.~Jacobs.
\newblock \emph{Categorical Logic and Type Theory}.
\newblock Stud. Logic Found. Math.~141, North-Holland, 1999.

\bibitem[Jac93]{Jac93}
B.~Jacobs.
\newblock Comprehension categories and the semantics of type dependency.
\newblock \emph{Theoret.~Comput.~Sci.} 107(2), 169--207, 1993.

\bibitem[Kam26b]{Kam26b}
K.~Kamiya.
\newblock The contextad of double telescopes.
\newblock Preprint, 2026.

\bibitem[Kel80]{Kel80}
G.~M.~Kelly.
\newblock A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on.
\newblock \emph{Bull.~Austral.~Math.~Soc.} 22(1), 1--83, 1980.

\bibitem[KL04]{KL04}
G.~M.~Kelly, S.~Lack.
\newblock Monoidal functors generated by adjunctions, with applications to transport of structure.
\newblock In \emph{Galois Theory, Hopf Algebras, and Semiabelian Categories}, Fields Inst.~Commun.~43, 319--340. Amer.~Math.~Soc., 2004.

\bibitem[Lac00]{Lac00}
S.~Lack.
\newblock A coherent approach to pseudomonads.
\newblock \emph{Adv.~Math.} 152(2), 179--202, 2000.

\bibitem[JS91]{JS91}
A.~Joyal and R.~Street.
\newblock The geometry of tensor calculus, I.
\newblock \emph{Adv.~Math.} 88(1):55--112, 1991.

\bibitem[JY21]{JY21}
N.~Johnson and D.~Yau.
\newblock \emph{2-Dimensional Categories}.
\newblock Oxford University Press, 2021. \href{https://arxiv.org/abs/2002.06055}{arXiv:2002.06055}.

\bibitem[JS93]{JS93}
A.~Joyal and R.~Street.
\newblock Pullbacks equivalent to pseudopullbacks.
\newblock \emph{Cahiers Topologie G\'eom. Diff\'erentielle Cat\'eg.} 34(2):153--156, 1993.

\bibitem[Lei04]{Lei04}
T.~Leinster.
\newblock \emph{Higher Operads, Higher Categories}.
\newblock London Math.~Soc.~Lecture Note Ser.~298. Cambridge University Press, 2004. \href{https://arxiv.org/abs/math/0305049}{arXiv:math/0305049}.

\bibitem[LN19]{LN19}
F.~Lucatelli Nunes.
\newblock Pseudoalgebras and non-canonical isomorphisms.
\newblock \emph{Appl. Categ. Structures} 27(1):55--63, 2019.

\bibitem[McC12]{McC12}
M.~B.~McCurdy.
\newblock Graphical methods for {T}annaka duality of weak bialgebras and weak {H}opf algebras.
\newblock \emph{Theory Appl. Categ.}, 26(9):233--280, 2012.

\bibitem[LR20]{LR20}
F.~Loregian, E.~Riehl.
\newblock Categorical notions of fibration.
\newblock \emph{Expo.~Math.} 38(4), 496--514, 2020.

\bibitem[New18]{New18}
C.~Newstead.
\newblock \emph{Algebraic Models of Dependent Type Theory}.
\newblock PhD thesis, Carnegie Mellon University, 2018. \href{https://arxiv.org/abs/2103.06155}{arXiv:2103.06155}.

\bibitem[Pal13]{Pal13}
E.~Palmgren.
\newblock The Grothendieck construction and models for dependent types.
\newblock Notes, 2013, revised 2016, \url{https://staff.math.su.se/palmgren/iterated_presheaves_and_dependent_types_v8.pdf}.

\bibitem[Sel11]{Sel11}
P.~Selinger.
\newblock A survey of graphical languages for monoidal categories.
\newblock In \emph{New Structures for Physics}, Lecture Notes in Phys.~813, 289--355. Springer, 2011. \href{https://arxiv.org/abs/0908.3347}{arXiv:0908.3347}.

\bibitem[Str23]{Str23}
T.~Streicher.
\newblock Fibered categories \`a la Jean B\'enabou.
\newblock Preprint, \href{https://arxiv.org/abs/1801.02927}{arXiv:1801.02927}, version~20, 2023.

\bibitem[Web15]{Web15}
M.~Weber.
\newblock Polynomials in categories with pullbacks.
\newblock \emph{Theory Appl.~Categ.} 30(16):533--598, 2015.

\bibitem[Zuc75]{Zuc75}
J.~Zucker.
\newblock Formalization of classical mathematics in Automath.
\newblock In \emph{Colloques Internationaux du CNRS} 249, 135--145, 1975. Reprinted in \emph{Selected Papers on Automath}, Stud. Logic Found. Math.~133, North-Holland, 1994, 127--139, \href{https://doi.org/10.1016/S0049-237X(08)70202-7}{doi:10.1016/S0049-237X(08)70202-7}.

\end{thebibliography}

\end{document}