math.CT — Category Theory
The Grothendieck construction between the telescope monad and contextads
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.