Assume-guarantee reasoning is a technique for compositional model checking in which system specifications are checked under certain assumptions on system parameters or inputs, and provide guarantees on observations of system state. We present a categorical framework for assume-guarantee reasoning for safety problems by viewing systems as lenses, following our earlier work on the compositionality of generalized Moore machines. Generalized Moore machines include ordinary Moore machines, partially observable Markov (decision) processes, and systems of parameterized ODEs (control systems); our framework gives assume-guarantee reasoning specially adapted to each of these cases. In particular, we give a novel formulation of assume-guarantee reasoning for (local) input-to-state stability ((L)ISS) Lyapunov functions on systems of parameterized ODEs.
Our framework is categorically natural and straightforwardly compositional. A flavor of generalized Moore machine is determined by a tangency: a fibration with a section. We show that symmetric monoidal loose right modules of assume-guarantee certified generalized Moore machines over symmetric monoidal double categories of certified wiring diagrams can be constructed 2-functorially from fibrations internal to the 2-category of tangencies.

We study how discrete opfibration classifiers in a(n enhanced) 2-category can be endowed with the structure of a \(T\)-algebra and thereby lift to the enhanced 2-category of 2-algebras and lax morphisms. To support this study, we give a definition of discrete opfibration classifier in the enhanced setting in which tight (e.g. strict) discrete opfibrations are classified by loose (e.g. lax) maps.

We then single out conditions on the 2-monad \(T\) and the classifier that make this possible, and observe these hold in a wide range of examples: double categories (recovering the results of Parè and Lambert), (symmetric) monoidal categories, and all structures encoded by familial 2-monads. We also prove the properties needed on such 2-monads are stable under replacement by pseudo-algebra coclassifiers (when sufficient exactness conditions hold), allowing us to replace a pseudo-algebra structure on the classifier by a strict one.

To get to our main theorem, we introduce the concepts of cartesian maps and cartesian objects of a 2-algebra, which generalize various other notions in category theory such as cartesian monoidal categories, extensive categories, categories with descent, and more. As a corollary, we characterize when representable copresheaves are pseudo rather than lax in terms of the cartesianity at their representing object.

We introduce contextads and the Ctx construction, unifying various structures and constructions in category theory dealing with context and contextful arrows -- comonads and their Kleisli construction, actegories and their Para construction, adequate triples and their Span construction. Contextads are defined in terms of Lack--Street wreaths, suitably categorified for pseudomonads in a tricategory of spans in a 2-category with display maps. The associated wreath product provides the Ctx construction, and by its universal property we conclude trifunctoriality. This abstract approach lets us work up to structure, and thus swiftly prove that, under very mild assumptions, a contextad equipped colaxly with a 2-algebraic structure produces a similarly structured double category of contextful arrows. We also explore the role contextads might play qua dependently graded comonads in organizing contextful computation in functional programming. We show that many side-effects monads can be dually captured by dependently graded comonads, and gesture towards a general result on the `transposability' of parametric right adjoint monads to dependently graded comonads.