arxiv: 2604.03017 · v1 · submitted 2026-04-03 · 💻 cs.LO · math.CT· math.DS

Recognition: 2 theorem links

· Lean Theorem

Compositionality of Lyapunov functions via assume-guarantee reasoning

Matteo Capucci , David Jaz Myers

Authors on Pith no claims yet

Pith reviewed 2026-05-13 18:32 UTC · model grok-4.3

classification 💻 cs.LO math.CTmath.DS

keywords assume-guarantee reasoningLyapunov functionsinput-to-state stabilitycategorical compositionalitylensesgeneralized Moore machinestangenciescontrol systems

0 comments

The pith

Assume-guarantee reasoning for Lyapunov functions on parameterized ODEs becomes compositional through a lens-based categorical framework.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a categorical approach to assume-guarantee reasoning for safety and stability properties of systems. Systems are modeled as lenses, allowing modular composition of specifications that assume certain inputs and guarantee certain outputs. This setup covers generalized Moore machines, including systems of parameterized ODEs used in control theory. For these ODE systems it supplies a new way to compose local input-to-state stability certificates built from Lyapunov functions. A sympathetic reader would care because the method turns large-system verification into a matter of assembling smaller, already-certified pieces.

Core claim

We give a novel formulation of assume-guarantee reasoning for (local) input-to-state stability ((L)ISS) Lyapunov functions on systems of parameterized ODEs. The framework views systems as lenses and constructs symmetric monoidal loose right modules of assume-guarantee certified generalized Moore machines over symmetric monoidal double categories of certified wiring diagrams; these modules arise 2-functorially from fibrations internal to the 2-category of tangencies.

What carries the argument

Lenses as generalized Moore machines, with a tangency (fibration with section) fixing the machine flavor and supporting 2-functorial construction of the assume-guarantee modules.

If this is right

Stability certificates for large interconnected control systems can be assembled from certificates for their subsystems.
The same construction supplies assume-guarantee reasoning for Markov decision processes and ordinary Moore machines.
Verification tasks reduce to checking local contracts at component interfaces rather than global behavior.
The resulting modules remain closed under further composition, preserving the modular structure at every scale.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Control engineers could obtain automated composition rules that turn separate Lyapunov analyses into a single certificate for an entire plant.
The same lens-and-tangency pattern may unify stability results across hybrid and stochastic dynamical systems.
Concrete examples with low-dimensional ODEs would provide direct numerical checks on whether the 2-functorial modules preserve the expected decay rates.

Load-bearing premise

Generalized Moore machines can be modeled uniformly as lenses and a tangency determines the machine flavor in a way that supports the 2-functorial construction of assume-guarantee modules.

What would settle it

An explicit pair of (L)ISS Lyapunov functions whose composition under the assumed wiring diagram yields a combined system whose trajectories violate the predicted input-to-state stability bound.

read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper builds a categorical framework for composing assume-guarantee certificates with (L)ISS Lyapunov functions on parameterized ODEs, but the key step of preserving the decrease condition under lens composition needs explicit verification.

read the letter

This paper gives a categorical treatment of assume-guarantee reasoning for stability certificates, modeling generalized Moore machines as lenses and using tangencies (fibrations with sections) to handle different system types, including parameterized ODEs. It claims a 2-functorial construction of symmetric monoidal loose right modules over wiring diagrams that yields compositional certificates for (L)ISS Lyapunov functions. That is the main new piece: adapting their prior Moore-machine work to Lyapunov decrease conditions in a uniform way. The setup looks clean on the abstract level and makes the compositionality follow from the 2-categorical structure rather than ad-hoc arguments. Credit is due for keeping the framework natural and for targeting a concrete verification problem in control systems. The soft spot is exactly the one in the stress-test note. The construction produces composite certificates only if the chosen section of the fibration preserves the specific form of the ISS estimate (decrease along trajectories plus input gain). The abstract does not show that this holds after lens composition, so it is possible the composite Lyapunov function fails to satisfy the inequality even when the parts do. Without seeing the full derivations it is hard to tell whether this is proven or left implicit. The paper is aimed at readers already comfortable with 2-categories, double categories, and categorical control theory. A serious referee should see it because the framework is new, the target application matters for modular verification, and the potential gap is fixable if the preservation argument is there. I would send it to review rather than desk-reject.

Referee Report

2 major / 2 minor

Summary. The manuscript develops a categorical framework for assume-guarantee reasoning in safety verification by modeling generalized Moore machines (including Moore machines, POMDPs, and parameterized ODEs) as lenses. A 'tangency' is defined as a fibration with section that determines the machine flavor; from internal fibrations in the 2-category of tangencies the authors construct 2-functorially symmetric monoidal loose right modules of assume-guarantee certified machines over symmetric monoidal double categories of certified wiring diagrams. The central novel contribution is a formulation of this machinery that yields compositional certificates for (local) input-to-state stability ((L)ISS) Lyapunov functions on systems of parameterized ODEs.

Significance. If the 2-functorial construction is shown to preserve the Lyapunov decrease condition, the work supplies a uniform, compositional method for building stability certificates across discrete, stochastic and continuous systems. This could enable scalable assume-guarantee verification of complex control systems and offers a categorically natural bridge between formal methods and Lyapunov-based analysis.

major comments (2)

[§4] §4 (2-functorial construction of loose right modules): the argument that the composite certificate remains a valid (L)ISS Lyapunov function relies on the section of the tangency preserving the decrease inequality plus input-gain term under lens composition, but no explicit verification or diagram chase is supplied showing that the ISS estimate is preserved by the monoidal structure of the wiring diagrams.
[Definition of tangency for ODEs] Definition of the tangency for parameterized ODEs (around the control-system case): it is asserted that the chosen fibration+section supports the 2-functor whose modules preserve the Lyapunov condition, yet the manuscript provides no calculation demonstrating that the section maps the specific form of the ISS Lyapunov inequality to a valid inequality on the composite system.

minor comments (2)

[Notation] The notation for 'symmetric monoidal loose right modules' is introduced without a small concrete example of a two-component composition; adding one would clarify the construction.
[§3] A brief comparison table showing how the general framework specializes to ordinary Moore machines versus the ODE case would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading and constructive comments. We address the major comments below by agreeing to supply the requested explicit verifications in a revised manuscript.

read point-by-point responses

Referee: [§4] §4 (2-functorial construction of loose right modules): the argument that the composite certificate remains a valid (L)ISS Lyapunov function relies on the section of the tangency preserving the decrease inequality plus input-gain term under lens composition, but no explicit verification or diagram chase is supplied showing that the ISS estimate is preserved by the monoidal structure of the wiring diagrams.

Authors: We agree that an explicit verification would improve clarity. In the revised manuscript we will add a detailed diagram chase in §4 that computes the composite ISS Lyapunov function explicitly, showing how the section of the tangency maps the decrease inequality plus input-gain term through lens composition and preserves the estimate under the symmetric monoidal structure of the wiring diagrams. revision: yes
Referee: [Definition of tangency for ODEs] Definition of the tangency for parameterized ODEs (around the control-system case): it is asserted that the chosen fibration+section supports the 2-functor whose modules preserve the Lyapunov condition, yet the manuscript provides no calculation demonstrating that the section maps the specific form of the ISS Lyapunov inequality to a valid inequality on the composite system.

Authors: We accept that an explicit calculation for the parameterized ODE case is missing. The revised version will include a direct computation demonstrating that the chosen fibration and section send the ISS Lyapunov inequality on each component to a valid inequality on the composite system, confirming that the 2-functor preserves the local input-to-state stability condition. revision: yes

Circularity Check

0 steps flagged

Minor self-citation to prior Moore machine work; Lyapunov formulation introduces independent content

full rationale

The paper cites its authors' earlier work on generalized Moore machines as lenses to set up the tangency-based framework, but the central contribution—a novel assume-guarantee formulation for (L)ISS Lyapunov functions on parameterized ODEs—is presented as a direct construction via symmetric monoidal loose right modules over wiring diagrams. No equation or claim reduces a derived quantity to a fitted parameter or self-defined input by construction; the 2-functoriality is asserted from the internal fibration structure rather than presupposing the target Lyapunov decrease condition. The self-citation is acknowledged but does not carry the load of the new Lyapunov certificates, leaving the derivation self-contained against external categorical benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The framework rests on categorical assumptions about lenses and tangencies drawn from prior work; no free parameters or invented physical entities are mentioned.

axioms (2)

domain assumption Systems are modeled as lenses following earlier work on generalized Moore machines
Stated in the abstract as the basis for the framework.
domain assumption A flavor of generalized Moore machine is determined by a tangency: a fibration with a section
Central definition used to construct the assume-guarantee modules.

pith-pipeline@v0.9.0 · 5493 in / 1246 out tokens · 32478 ms · 2026-05-13T18:32:38.926002+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

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.
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

an equilibrium of open ODE is local ISS if and only if it is a certified ODE ... dϕ(f(x,a)) + κ(ϕ(x))

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

Enhanced $2$-categories of models of sketches as enhanced $2$-categories of algebras over monads
math.CT 2026-05 unverdicted novelty 7.0

Models of enhanced limit 2-sketches are equivalent to algebras over enhanced 2-monads, including lax morphisms, and inherit w-rigged limits.

Reference graph

Works this paper leans on

44 extracted references · 44 canonical work pages · cited by 1 Pith paper

[1]

arXiv:2405.17304

Alessandro Abate, Mirco Giacobbe & Diptarko Roy (2024):Stochastic Omega-Regular Verification and Control with Supermartingales. arXiv:2405.17304. M. Capucci & D. J. Myers13

work page arXiv 2024
[2]

arXiv:2504.05065

Alessandro Abate, Mirco Giacobbe & Diptarko Roy (2025):Quantitative Supermartingale Certificates. arXiv:2504.05065

work page arXiv 2025
[3]

Ames, Sébastien Mattenet & Joe Moeller (2025):Categorical Lyapunov Theory II: Stability of Systems

Aaron D. Ames, Sébastien Mattenet & Joe Moeller (2025):Categorical Lyapunov Theory II: Stability of Systems. arXiv:2505.22968

work page arXiv 2025
[4]

Ames, Joe Moeller & Paulo Tabuada (2025):Categorical Lyapunov Theory I: Stability of Flows

Aaron D. Ames, Joe Moeller & Paulo Tabuada (2025):Categorical Lyapunov Theory I: Stability of Flows. arXiv:2502.15276

work page arXiv 2025
[5]

arXiv:2412.07475

Nathanael Arkor, John Bourke & Joanna Ko (2024):Enhanced 2-categorical structures, two-dimensional limit sketches and the symmetry of internalisation. arXiv:2412.07475

work page arXiv 2024
[6]

Fleming & Christina Vasilakopoulou (2021):Categorical Semantics of Cyber- Physical Systems Theory.ACM Transactions on Cyber-Physical Systems,5(3), doi:10.1145/3461669

Georgios Bakirtzis, Cody H. Fleming & Christina Vasilakopoulou (2021):Categorical Semantics of Cyber- Physical Systems Theory.ACM Transactions on Cyber-Physical Systems,5(3), doi:10.1145/3461669. Available athttps://doi.org/10.1145/3461669

work page doi:10.1145/3461669 2021
[7]

P ˘as˘areanu & Dimitra Giannakopoulou (2008):Automated Assume- Guarantee Reasoning by Abstraction Refinement

Mihaela Gheorghiu Bobaru, Corina S. P ˘as˘areanu & Dimitra Giannakopoulou (2008):Automated Assume- Guarantee Reasoning by Abstraction Refinement. In:Proceedings of the 20th International Conference on Computer Aided Verification (CA V 2008),Lecture Notes in Computer Science5123, Springer, pp. 135–148, doi:10.1007/978-3-540-70545-1_14

work page doi:10.1007/978-3-540-70545-1_14 2008
[8]

Cobleigh, Dimitra Giannakopoulou & Corina S

Jamieson M. Cobleigh, Dimitra Giannakopoulou & Corina S. P˘as˘areanu (2003):Learning Assumptions for Compositional Verification. In:Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003),Lecture Notes in Computer Science2619, Springer, pp. 331–346, doi:10.1007/3-540-36577-X_24

work page doi:10.1007/3-540-36577-x_24 2003
[9]

Cobleigh, Dimitra Giannakopoulou, Corina S

Jamieson M. Cobleigh, Dimitra Giannakopoulou, Corina S. P˘as˘areanu & Howard Barringer (2008):Learning to Divide and Conquer: Applying the L* Algorithm to Automate Assume-Guarantee Reasoning.Formal Methods in System Design32(3), pp. 175–205, doi:10.1007/s10703-008-0049-6

work page doi:10.1007/s10703-008-0049-6 2008
[10]

Geoffrey S. H. Cruttwell, Michael Lambert, Dorette Pronk & Martin Szyld (2022):Double Fibrations. Theory and Applications of Categories38(35), pp. 1326–1394, doi:10.48550/arXiv.2205.15240. Available at https://arxiv.org/abs/2205.15240

work page doi:10.48550/arxiv.2205.15240 2022
[11]

In Corina Cîrstea, editor:Coalgebraic Methods in Computer Science, Springer International Publishing, Cham, pp

Ulrich Dorsch, Stefan Milius, Lutz Schröder & Thorsten Wißmann (2018):Predicate Liftings and Functor Presentations in Coalgebraic Expression Languages. In Corina Cîrstea, editor:Coalgebraic Methods in Computer Science, Springer International Publishing, Cham, pp. 56–77

work page 2018
[12]

Luca Geatti (2025):Automata Cascades for Model Checking. In Angelo Montanari, Andrea Orlandini, Nicola Saccomanno & Stefano Tonetta, editors:Short Paper Proceedings of the 7th International Workshop on Artificial Intelligence and Formal Verification, Logic, Automata , and Synthesis, OVERLAY 2025, Bologna, Italy, October 26, 2025,CEUR Workshop Proceedings4...

work page 2025
[13]

Long (1994):Model checking and modular verification.ACM Trans

Orna Grumberg & David E. Long (1994):Model checking and modular verification.ACM Trans. Program. Lang. Syst.16(3), p. 843–871, doi:10.1145/177492.177725. Available at https://doi.org/10.1145/ 177492.177725

work page doi:10.1145/177492.177725 1994
[14]

McMillan & Zhaohui Fu (2008):Automated Assumption Generation for Compositional Verification.Formal Methods in System Design32(3), pp

Anubhav Gupta, Kenneth L. McMillan & Zhaohui Fu (2008):Automated Assumption Generation for Compositional Verification.Formal Methods in System Design32(3), pp. 285–301, doi:10.1007/s10703-008- 0050-0

work page doi:10.1007/s10703-008- 2008
[15]

arXiv:2011.11042

Rune Haugseng, Fabian Hebestreit, Sil Linskens & Joost Nuiten (2023):Two-variable fibrations, factorisation systems and∞-categories of spans. arXiv:2011.11042

work page arXiv 2023
[16]

Henzinger, Kaushik Mallik, Pouya Sadeghi & Ðor ¯de Žikeli ´c (2025):Supermartingale Certificates for Quantitative Omega-regular Verification and Control

Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi & Ðor ¯de Žikeli ´c (2025):Supermartingale Certificates for Quantitative Omega-regular Verification and Control. arXiv:2505.18833

work page arXiv 2025
[17]

Henzinger, Shaz Qadeer, Sriram K

Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani & Serdar Ta¸ sıran (2002):An Assume-Guarantee Rule for Checking Simulation.ACM Transactions on Programming Languages and Systems24(1), pp. 51–64, doi:10.1145/509705.509707. 14Compositionality of Lyapunov functions via assume-guarantee reasoning

work page doi:10.1145/509705.509707 2002
[18]

83–109, doi:https://doi.org/10.1016/S0022-4049(97)00129-1

Claudio Hermida (1999):Some properties of Fib as a fibred 2-category.Journal of Pure and Applied Algebra134(1), pp. 83–109, doi:https://doi.org/10.1016/S0022-4049(97)00129-1. Available at https://www. sciencedirect.com/science/article/pii/S0022404997001291

work page doi:10.1016/s0022-4049(97)00129-1 1999
[19]

Cambridge Tracts in Theoretical Computer Science, Cambridge University Press

Bart Jacobs (2016):Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press

work page 2016
[20]

154–167, doi:10.4204/eptcs.333.11

David Jaz Myers (2021):Double Categories of Open Dynamical Systems (Extended Abstract).Electronic Proceedings in Theoretical Computer Science333, p. 154–167, doi:10.4204/eptcs.333.11. Available at http://dx.doi.org/10.4204/EPTCS.333.11

work page doi:10.4204/eptcs.333.11 2021
[21]

Towards a double operadic theory of systems.arXiv preprint arXiv:2505.18329, 2025

Sophie Libkind & David Jaz Myers (2025):Towards a double operadic theory of systems. arXiv:2505.18329

work page arXiv 2025
[22]

Communications and Control Engineering, Springer International Publishing, Cham, doi:10.1007/978-3-031-14674-9

Andrii Mironchenko (2023):Input-to-State Stability: Theory and Applications. Communications and Control Engineering, Springer International Publishing, Cham, doi:10.1007/978-3-031-14674-9. Available at https: //link.springer.com/10.1007/978-3-031-14674-9

work page doi:10.1007/978-3-031-14674-9 2023
[23]

Moore (2016):Gedanken-Experiments on Sequential Machines, pp

Edward F. Moore (2016):Gedanken-Experiments on Sequential Machines, pp. 129–154. Princeton University Press, Princeton, doi:doi:10.1515/9781400882618-006. Available at https://doi.org/10. 1515/9781400882618-006

work page doi:10.1515/9781400882618-006 2016
[24]

Available at https://forest.topos

David Jaz Myers:On the representability of Lyapunov-type functions. Available at https://forest.topos. site/public/djm-00CP/. Unpublished note

work page
[25]

arXiv:2006.14022

David Jaz Myers (2021):Cartesian Factorization Systems and Grothendieck Fibrations. arXiv:2006.14022

work page arXiv 2021
[26]

Available at http://davidjaz.com/Papers/ DynamicalBook.pdf

David Jaz Myers (2021):Categorical Systems Theory. Available at http://davidjaz.com/Papers/ DynamicalBook.pdf

work page 2021
[27]

P˘as˘areanu, Matthew B

Corina S. P˘as˘areanu, Matthew B. Dwyer & Michael Huth (1999):Assume-Guarantee Model Checking of Software: A Comparative Case Study. In:Proceedings of the 6th International SPIN Workshop on Theoretical and Practical Aspects of SPIN Model Checking,Lecture Notes in Computer Science1680, Springer, pp. 168–183, doi:10.1007/3-540-48234-2_14

work page doi:10.1007/3-540-48234-2_14 1999
[28]

In Krzysztof R

Amir Pnueli (1985):In Transition From Global to Modular Temporal Reasoning about Programs. In Krzysztof R. Apt, editor:Logics and Models of Concurrent Systems, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 123–144

work page 1985
[29]

Spivak (2013):The operad of temporal wiring diagrams: formalizing a graphical language for discrete-time processes

Dylan Rupel & David I. Spivak (2013):The operad of temporal wiring diagrams: formalizing a graphical language for discrete-time processes. arXiv:1307.6894

work page arXiv 2013
[30]

Rutten (2000):Universal coalgebra: a theory of systems.Theoretical Computer Science249(1), pp

J.J.M.M. Rutten (2000):Universal coalgebra: a theory of systems.Theoretical Computer Science249(1), pp. 3–80, doi:https://doi.org/10.1016/S0304-3975(00)00056-6. Available at https://www.sciencedirect. com/science/article/pii/S0304397500000566. Modern Algebra

work page doi:10.1016/s0304-3975(00)00056-6 2000
[31]

Spivak & Christina Vasilakopoulou (2019):Dynamical Systems and Sheaves

Patrick Schultz, David I. Spivak & Christina Vasilakopoulou (2019):Dynamical Systems and Sheaves. arXiv:1609.08086

work page arXiv 2019
[32]

Sontag (1989):Smooth Stabilization Implies Coprime Factorization.IEEE transactions on automatic control34(4), pp

Eduardo D. Sontag (1989):Smooth Stabilization Implies Coprime Factorization.IEEE transactions on automatic control34(4), pp. 435–443. Available at https://www.academia.edu/download/48193612/ Smooth_Stabilization_Implies_Coprime_Fac20160820-11625-15xs30o.pdf

work page arXiv 1989
[33]

Sontag (2008):Input to State Stability: Basic Concepts and Results, pp

Eduardo D. Sontag (2008):Input to State Stability: Basic Concepts and Results, pp. 163–220. 1932, Springer Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/978-3-540-77653-6_3. Available at http: //link.springer.com/10.1007/978-3-540-77653-6_3

work page doi:10.1007/978-3-540-77653-6_3 2008
[34]

Spivak (2022):Generalized Lens Categories via functorsC op /∫hortrightarrowCat

David I. Spivak (2022):Generalized Lens Categories via functorsC op /∫hortrightarrowCat. arXiv:1908.02202

work page arXiv 2022
[35]

Spivak & Eugene Lerman (2015):Algebras of Open Dynamical Systems on the Operad of Wiring Diagrams

Dmitry Vagner, David I. Spivak & Eugene Lerman (2015):Algebras of Open Dynamical Systems on the Operad of Wiring Diagrams. arXiv:1408.1598

work page arXiv 2015
[36]

In: Proceedings of the 28th International Colloquium on Automata, Languages and Programming (ICALP 2001), Lecture Notes in Computer Science2076, Springer, pp

Mahesh Viswanathan & Ramesh Viswanathan (2001):Foundations for Circular Compositional Reasoning. In: Proceedings of the 28th International Colloquium on Automata, Languages and Programming (ICALP 2001), Lecture Notes in Computer Science2076, Springer, pp. 142–153, doi:10.1007/3-540-48224-5_68. M. Capucci & D. J. Myers15 A Construction of the double catego...

work page doi:10.1007/3-540-48224-5_68 2001
[37]

Explicitly, this sends α γ to (x,y)↦/∫hortrightarrowα(f(x),f♯(x,y)) x↦/∫hortrightarrowγ(f(x))

For a bundle map f♯ f : F B ⇒ F ′ B′ , Cert acts by precomposition. Explicitly, this sends α γ to (x,y)↦/∫hortrightarrowα(f(x),f♯(x,y)) x↦/∫hortrightarrowγ(f(x)) . This is evidently functorial

work page
[38]

Slacks are considered a category byκ 1 /∫hortrightarrowκ2 whenκ 1 ≥κ 2

For a lens w♯ w : F B ⇆ F ′ G′ , we define Cert w♯ w ⊆K 0 ∞ ×Cert F B ×Cert F ′ B′ to be the full subcategory consisting of triples κ, α γ , α ′ γ ′ for which the lens is certified: w♯ w ⊨ α γ κ ⇆ α ′ γ ′ :⇐ ⇒ ( α ′(w(x),y) +κ(γ(x))≥α(x,w ♯(x,y)) γ(x)≥γ ′(w(x)) (A.3) We refer toκas theslack. Slacks are considered a category byκ 1 /∫hortrightarrowκ2 whenκ 1 ≥κ 2

work page
[39]

For a square as below left, implying the equations below right: F1 B1 F3 B3 F2 B2 F4 B4 f♯ f u♯ u g♯ g w♯ w ( w♯(f(x),g ♯(u(x),y)) =f ♯(x,u ♯(x,y)) w(f(x)) =g(u(x)) (A.4) we need to check that if w♯ w ⊨ α γ κ ⇆ α ′ γ ′ , then u♯ u ⊨ f♯ f ∗ α γ κ ⇆ g♯ g ∗ α ′ γ ′ ; in other words, that ( α ′(g(u(x)),g ♯(u(x),y)) +κ(γ(f(x)))≥α(f(x),f ♯(x,u ♯(f(x),y))) γ(f(x...

work page
[40]

We quite trivially have π2 id ⊨ α γ 0 ⇆ α γ , which handles the unitor

We then need to supply the unitor and compositor. We quite trivially have π2 id ⊨ α γ 0 ⇆ α γ , which handles the unitor. For the compositor, we add the slacks; suppose that w♯ 1 w1 ⊨ α1 γ1 κ1 ⇆ α2 γ2 and w♯ 2 w2 ⊨ α2 γ2 κ2 ⇆ α3 γ3 , seeking to show that w♯ 2 w2 ◦ w♯ 1 w1 ⊨ α1 γ1 κ1+κ2 ⇆ α2 γ2 . We may prove this as follows:    α3(w2(w1(x)),y) ...

work page
[41]

On lenses, we also add the slacks

The laxitorCert F B ×Cert F ′ B′ /∫hortrightarrowCert F×F ′ B×B′ is given by componentwise addition: α γ , α ′ γ ′ ↦/∫hortrightarrow α+α ′ γ+γ ′ . On lenses, we also add the slacks. This is evidently commutative, associative, and monotone. The identity is 0 0 : 1 1 ⇒ R R . It interchanges with compositors because both add the slacks and addition is commut...

work page
[42]

The map of posets (R×R,≥ lexico)/∫hortrightarrow(R,≥)is a Grothendieck fibration but pullback along a strict inequality a⪈b sends every pair (b,b ′) to (a,0)

The lexicographic order prevents bundle predicates from being fibred over predicates ‘in the correct way’. The map of posets (R×R,≥ lexico)/∫hortrightarrow(R,≥)is a Grothendieck fibration but pullback along a strict inequality a⪈b sends every pair (b,b ′) to (a,0). This is not the behaviour we want, what we want is to get (a,b ′) or at most (a,η(b ′)) whe...

work page
[43]

One could fix the first problem by using the product order instead of lexicographic, but this in turns makes Definition 4.13 unsatisfactory, since ϕ↦/∫hortrightarrow(ϕ,dϕ)is not a monotone section of (R×R,≥ × ≥)/∫hortrightarrow(R,≥)

work page
[44]

B Proofs of Section 3 We will make use of the theory ofenhanced sketches[ 5]

Finally,slackis needed, in practice, for good compositional properties, and that cannot be accounted for in any way in a lens construction. B Proofs of Section 3 We will make use of the theory ofenhanced sketches[ 5]. Example 5.15 ofibid.gives the enhanced sketch Tfib for tight fibrations, so that models in the (chordate) enhanced 2-category of categories...

work page