A contextad is a wreath in the Kleisli completion of the tricategory of spans, specifically the Kleisli completion rather than the Eilenberg–Moore one. Just as a monad is a monoid in an endo-hom-category and a wreath (Lack–Street) is a monad in a Kleisli-completed 2-category, a contextad packages a graded, context-dependent algebraic structure one dimension up. From a contextad the construction builds a double category whose morphisms carry an explicit context or grade. The construction is unificatory. A single recipe recovers the construction, Kleisli categories, and as special cases (Capucci–Myers, arXiv:2410.21889).
The construction is formally Kleisli. The Kleisli completion carries a universal property. There is a trifunctor such that, for any tricategory possessing all Kleisli objects, precomposition is an adjoint triequivalence onto the Kleisli-continuous trihomomorphisms. The wreath product that assembles contextads is induced from this property, exactly as monad multiplication is induced from a Kleisli left adjoint. One caveat applies. The presentation only establishes that is triessentially surjective, and upgrading this to a genuine adjoint triequivalence remains conjectural (the paper’s footnote 17).
Being formally Kleisli does not, however, pin the construction down uniquely (Remark 3.25). Fujii–Katsumata–Melliés give a construction that is also formally Kleisli yet differs from . Its objects are decorated with grades and its morphisms are optics rather than the plain spans/lenses of . The two agree on the abstract Kleisli recipe and diverge only in their choice of ambient, the tricategory inside which the Kleisli object is taken. The phrase “formal Kleisli construction” therefore names a schema, and the ambient is the remaining degree of freedom that fixes an actual theory.
That degree of freedom is organised by the shape of the grading fibration, and reading off shapes recovers the classical constructions in a single table. When is the identity, collapses to a comonad / Kleisli construction. A projection carrying a colax action gives and graded comonads. A codomain / display-map fibration gives and partial-map categories. A general comprehension category gives a dependent-type-flavoured . The other constructions of the fibrational world thus sit as points on one axis, indexed by how much the grading is allowed to vary over the base.
Property. The representable-and-discrete row is a universe
When is representable-and-discrete, i.e. with a fixed classifying map and given by pullback along it, yields polynomial / parametric-right-adjoint monads and their Kleisli categories. Type-theoretically a single classifier is a universe. The general form (§3.5.3) takes to be a dominance, a -closed subuniverse such as , where -closure is precisely the multiplication of the induced monad. In this light is “the big version that does not classify by a universe”. It admits all spans rather than only those whose fibres are named by a fixed classifier.
Applying to the fibration of display maps yields , the double category of spans whose left leg is a display map (Example 3.22). This is the concrete face of the display-map row above. Restricting the left legs to displays is exactly what a display-map ambient enforces, and it is the same move that in type theory keeps context extension well-behaved.
A dimensional subtlety in the Kleisli-object characterisation
The Kleisli-object characterisation of fails to give a clean mapping-out property, because the dimensions do not match. One might hope for . The -cells of are spans rather than functors, namely left-fibrant spans between arrow pseudomonads. So even when genuinely is a Kleisli object, its universal property characterises the left-fibrant spans out of it, a module / bimodule-type statement, rather than functors out of it. This departs from the classical Kleisli initiality that lives inside a functor category.
The Para expansion inside Ctx
The tensor of composes contexts in a fixed order. A context sits over an object , and a second context sits over the extended object , so the composite reads the first context before the second. This ordering is what makes a genuine special case rather than an analogy, because a parameter list is exactly a context that grows as it is consumed.
The multiplication of a contextad is colax, and the discrepancy is where the structure lives. The object appearing in the codomain of is not multiplied literally onto the data. It is the colaxator of a colax morphism, which Lemma 4.9/4.10 identify with a Kleisli morphism for the endofunctor . Making the action colax therefore breaks the distributive law outright, as the paper states rather than works around. The precise home of the assembled structure is Theorem 4.12, whose right-hand side takes to be the Kleisli -category of Definition 4.7, a -category whose -cells are the -cells .
Lenses and where dependent grading actually lives
A lens is the coKleisli category of the store comonad on , so lenses need a cartesian closed ambient. Feeding this into does collapse, yet it collapses onto the graded-comonad row of the classification rather than onto anything new. is therefore not a genuine example of dependent grading, contrary to first appearances.
Dependent grading belongs instead to dependent lenses and the category of polynomial functors. When the base is not cartesian closed the ambient must move from to , since the dependent structure no longer fits inside a span of sets. This is the ambient-choice degree of freedom identified above, now forced by the demand for genuine dependence.
Polynomial monads are transposable
The representable-and-discrete row deserves to be stated as an equivalence rather than a slogan. For a polynomial (container) monad the Kleisli category is equivalent to the category of contextful morphisms of the contextad built from that same functor (§3.5, Definition 3.33). Capucci–Myers verify writer, state, and Maybe individually and leave the general statement as future work. Pinning the construction down gives the dictionary below.
Let be locally cartesian closed and let be a polynomial monad .
contextad datum
polynomial-monad side
grade
, representable and discrete
extension
unit
counit
tensor
pointwise, the position component of
comultiplication
the direction component of ,
The load-bearing line is the last one. is the direction map of and it is not an isomorphism, which is exactly where the colax structure of the contextad comes from. Naturality then forces the unit. Pinning at and pulling back gives , and because the state component is the counit follows with no separate definition.
The proof is short once the dictionary is fixed. The transpose (3.5.1) is a bijection by the distributive law, the unit corresponds to by the forced form of , and agreement of composition is the monad axioms read off directly, since associativity of matches while its unit laws match .
Four checks, and where non-invertibility becomes visible
Writer takes , , , and . State uses , so , , the grade is , corresponds to , and . Reader takes and , whereupon is the diagonal, the case where failing to be an isomorphism is plainly visible. Maybe takes , , , and .
The reason this is not yet a theorem is that the pair is not canonical. A representation-independent statement needs the parametric-right-adjoint structure, which supplies and as the generic morphism. Outside and locally cartesian closed categories the very definition of leans on that PRA structure, so “transposability of PRA monads” names precisely this equivalence. Excluding continuous monads is then consistent, since a continuous monad is not parametric right adjoint.
What is still open
Two threads remain unresolved. The first asks whether the representable-and-discrete row and the codomain / display-map row of the classification connect through Poly or dependent lenses, which would fuse the universe picture with the span picture at the level of examples. The second is the content of §7 (doctrines of wreaths) and §8, unread here because the source is cut at page 42. Section 7 is the load-bearing one, since restricting the right leg of the spans requires the base itself to be a double category, and the statement of Theorem 4.19 together with the two-sided fibration and companion structure and the appearance of the adequate-triple all sit there.
References
M. Capucci, D. J. Myers, Contextads and the Ctx construction (arXiv:2410.21889).
S. Lack, R. Street, The formal theory of monads II, J. Pure Appl. Algebra 175 (2002) 243 (wreaths and the Kleisli/EM completions of a 2-category).
S. Fujii, S. Katsumata, P.-A. Melliés, a formal-Kleisli construction whose objects are graded and whose morphisms are optics, the alternative fixed by a different ambient.