Pith. sign in

REVIEW 94 references

Logical relations for call-by-push-value models, via internal fibrations in a 2-category

T0 review · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A 2-categorical fibrational framework gives a uniform notion of logical relations for CBPV models, with a pullback theorem that constructs new relational models from old ones.

arxiv 2505.14482 v2 pith:MHP32PL5 submitted 2025-05-20 cs.LO math.CT

Pedro H. Azevedo de Amorim , Satoshi Kura , Philip Saville This is my paper · ORCID
classification cs.LOmath.CT
keywords cbpvmodelsfibrationscategorylogicalappropriatecall-by-push-valueeffect
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Logical relations are a standard tool in programming language theory. A logical relation pairs each program type with a set of related values, and if the relation is set up correctly, almost any program property can be proved by checking a small set of base cases. This paper treats them for call-by-push-value (CBPV), Levy's calculus that subsumes both eager and lazy evaluation. In CBPV a model is an adjunction between a category of values and a category of computations, enriched over a presheaf category.

Previous work developed logical relations for CBPV operationally, or by hand for particular models. The gap this paper attacks is structural: the usual fibration recipe for generating logical relations, which works for the simply typed lambda calculus and for Moggi's monadic calculus, had no clean analogue for CBPV, because CBPV models mix adjunctions and enrichment. The authors' move is to work in a 2-category, where categories, functors, and natural transformations live together. Fibrations can be defined internally to any 2-category, so a locally indexed fibration arises automatically once the right ambient 2-category, called LInd, is chosen.

The central theorem says that pulling back a CBPV fibration along any model morphism yields another CBPV fibration, which is the standard recipe for constructing logical relations models by glueing. The paper verifies the machinery on examples: storage models, a powerset lifting for erratic choice, an effect simulation result, and a version of Katsumata's ⊤⊤-lifting. The main caveat is that the central theorem and the final full-completeness theorem are presented as sketches, with parts of the proofs omitted, so independent verification is needed before the framework is used as a foundation.

Extended reading notes

Core claim

CBPV fibrations, defined as fibrations internal to the 2-category LInd of locally indexed categories that strictly preserve the CBPV model structure, satisfy a pullback theorem: for any CBPV fibration (p,P) and any CBPV^fo_lx morphism (h,H,alpha,beta), the pullback exists in CBPV^fo_lx and the projection (q,Q) is again a CBPV fibration (Theorem V.1). If this is correct, every such pullback (glueing) produces a new logical relations-style model, and the definitions subsume algebra models, adjunction models, Katsumata's ⊤⊤-lifting, and effect simulation.

Load-bearing premise

Proposition IV.6 identifies fibrations internal to LInd with the componentwise lifting property, relying on Weber's characterization of internal fibrations and on the claim (Remark IV.3, Construction IV.4) that comma objects and pullbacks in the 2-Grothendieck construction of change of base are computed pointwise, i.e. that the relevant limits are preserved by change-of-base 2-functors. If comma objects in LInd differ from this componentwise description, the 'canonical' definition of CBPV fibration and the proof of Theorem V.1 would fail. The strictness of the bifibration (used for pullbacks in DistCat) is a second fragile premise, acknowledged by the authors in Example II.8.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Assumptions & free parameters 0 free parameters · 6 assumptions · 3 invented entities

There are no numerical fitted parameters, since the paper is a theory paper with no data-fitting component. The load-bearing assumptions are standard 2-category and enriched-category facts (internal fibrations, limit preservation in 2-Grothendieck constructions, 2-monad algebra fibrations), plus two domain assumptions the paper states explicitly (split fibrations, universe hierarchy, Levy's book CBPV as reference language). The one genuinely paper-specific premise is Lemma IV.15, asserting that the self construction preserves the limits and fibrations needed for the main theorem; it is stated without a detailed proof. Invented entities are mathematical definitions rather than empirical postulates, but they are new structures whose independent value is measured by how well they recover external results.

assumptions (6)
  • standard math Internal fibrations in a 2-category C are characterized by fibration data on each hom-category C(X,E) -> C(X,B), with cartesian-lifting preservation under precomposition (Weber, Street).
    Invoked in Definition II.3 and Proposition IV.6; the paper uses [57, Theorem 2.7] to identify locally indexed fibrations with comma-object conditions in LInd.
  • standard math The 2-Grothendieck construction K: CartCat^coop -> 2-CAT has the limits that exist in CartCat and in each K(C), provided each K(f) preserves them.
    Used in Remark IV.3 and Construction IV.4 to compute comma objects and pullbacks in LInd componentwise, which underlies Proposition IV.6 and Theorem V.1.
  • standard math Fibrations in 2-categories of algebras for a 2-monad are exactly structure-preserving fibrations in the base (Proposition II.4).
    Used to justify that a CBPV fibration can be a locally indexed fibration that strictly preserves the CBPV structure, without checking further algebra-fibration conditions.
  • domain assumption All fibrations in the paper are assumed split, and a hierarchy of universes handles size issues.
    Stated in the Notation paragraph; splitting is needed for clean Grothendieck-style constructions, and the universe hierarchy absorbs the presheaf-category size issues flagged before Section VII.
  • domain assumption Levy's 'book CBPV' with finite products and sums is the reference language, with sound and complete denotational semantics via locally C-indexed adjunctions.
    Section III fixes the language and model class; the paper relies on Levy's syntactic model being initial (Example IV.17) and on the standard adjunction-model semantics.
  • ad hoc to paper self: CartCat/DistCat -> LInd extends to 2-functors preserving products, comma objects, pullbacks, and (co)fibrations with suitable strictness (Lemma IV.15).
    Lemma IV.15 is stated without a full proof; it is load-bearing for Proposition IV.20 (codomain fibration is a CBPV fibration) and for preserving model structure through Theorem V.1's pullback.
invented entities (3)
  • The 2-category LInd of locally indexed categories (Definition IV.2) independent evidence
    purpose: Provides the ambient 2-category whose internal fibrations yield the notion of CBPV fibration.
    LInd is the 2-Grothendieck construction of change of base (Remark IV.3), so it is not freely invented; its usefulness is evidenced by recovering Katsumata's ⊤⊤-lifting, McDermott's logical relations, and effect simulation as instances.
  • CBPV fibrations (Definition IV.16): locally indexed (op)fibrations strictly preserving CBPV model structure independent evidence
    purpose: The fibrational logical-relations structure for CBPV that supports the pullback and lifting theorem.
    The definition is canonical by construction (Remark IV.8) and, via Theorem V.1, reproduces concrete checkable models (erratic choice powerset lifting, storage models, subobject fibrations).
  • Presheaf CBPV model and Yoneda map for CBPV- (Section VII-B) independent evidence
    purpose: Ingredient for the relative full completeness theorem via Lafont's argument.
    The construction is explicit (Definition VII.2), but the validation step, Theorem VII.6, is stated with its proof omitted, so the independent evidence is weaker than for the rest of the paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Logical relations for call-by-push-value models, via internal fibrations in a 2-category." pith.science (2026). https://pith.science/paper/MHP32PL5

@misc{pith2026250514482,
  author       = {Pith},
  title        = {Pith review of: Logical relations for call-by-push-value models, via internal fibrations in a 2-category},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MHP32PL5}},
  note         = {Machine review of arXiv:2505.14482}
}
abstract

We give a denotational account of logical relations for call-by-push-value (CBPV) in the fibrational style of Hermida, Jacobs, Katsumata and others. Fibrations -- which axiomatise the usual notion of sets-with-relations -- provide a clean framework for constructing new, logical relations-style, models. Such models can then be used to study properties such as effect simulation. Extending this picture to CBPV is challenging: the models incorporate both adjunctions and enrichment, making the appropriate notion of fibration unclear. We handle this using 2-category theory. We identify an appropriate 2-category, and define CBPV fibrations to be fibrations internal to this 2-category which strictly preserve the CBPV semantics. Next, we develop the theory so it parallels the classical setting. We give versions of the codomain and subobject fibrations, and show that new models can be constructed from old ones by pullback. The resulting framework enables the construction of new, logical relations-style, models for CBPV. Finally, we demonstrate the utility of our approach with particular examples. These include a generalisation of Katsumata's $\top\top$-lifting to CBPV models, an effect simulation result, and a relative full completeness result for CBPV without sum types.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

94 extracted references · 52 canonical work pages

  1. [1]

    Call-by-push-value,

    P. B. Levy, “Call-by-push-value,” Ph.D. dissertation, Queen Mary and Westfield College, University of London, 2001. [Online]. Available: https://qmro.qmul.ac.uk/xmlui/handle/123456789/4742

    arXiv 2001

  2. [2]

    Springer Netherlands, 2003

    ——,Call-By-Push-Value. Springer Netherlands, 2003. [Online]. Available: https://doi.org/10.1007/978-94-007-0954-6

    doi:10.1007/978-94-007-0954-6 2003

  3. [3]

    Fibrations, logical predicates and indeterminates,

    C. A. Hermida, “Fibrations, logical predicates and indeterminates,” Ph.D. dissertation, University of Edinburgh, 1993. [Online]. Available: http://hdl.handle.net/1842/14057

    1993

  4. [4]

    LCF considered as a programming language,

    G. D. Plotkin, “LCF considered as a programming language,” Theoretical Computer Science, vol. 5, no. 3, pp. 223–255, Dec. 1977. [Online]. Available: https://doi.org/10.1016/0304-3975(77)90044-5

    doi:10.1016/0304-3975(77)90044-5 1977

  5. [5]

    Reasoning about sequential functions via logical relations,

    K. Sieber, “Reasoning about sequential functions via logical relations,” inApplications of Categories in Computer Science. Cambridge University Press, Jun. 1992, pp. 258–269. [Online]. Available: https://doi.org/10.1017/cbo9780511525902.015

    work page doi:10.1017/cbo9780511525902.015 1992

  6. [6]

    An indexed model of recursive types for foundational proof-carrying code,

    A. W. Appel and D. McAllester, “An indexed model of recursive types for foundational proof-carrying code,”ACM Trans. Program. Lang. Syst., vol. 23, no. 5, p. 657–683, Sep. 2001. [Online]. Available: https://doi.org/10.1145/504709.504712

    arXiv 2001

  7. [7]

    Step-Indexed Biorthogonality: a Tutorial Example,

    A. M. Pitts, “Step-Indexed Biorthogonality: a Tutorial Example,” inModelling, Controlling and Reasoning About State, ser. Dagstuhl Seminar Proceedings (DagSemProc), A. Ahmed, N. Benton, L. Birkedal, and M. Hofmann, Eds., vol. 10351. Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum f ¨ur Informatik, 2010, pp. 1–10. [Online]. Available: https://drops.d...

    2010

  8. [8]

    Logical step-indexed logical relations,

    D. Dreyer, A. Ahmed, and L. Birkedal, “Logical step-indexed logical relations,”Logical Methods in Computer Science, vol. V olume 7, Issue 2, Jun. 2011. [Online]. Available: https://doi.org/10.2168/lmcs-7(2:16)2011

    work page doi:10.2168/lmcs-7(2:16)2011 2011

Show all 94 references
  1. [9]

    Types, abstraction, and parametric polymorphism, part 2,

    Q. M. Ma and J. C. Reynolds, “Types, abstraction, and parametric polymorphism, part 2,” inLecture Notes in Computer Science. Springer Berlin Heidelberg, 1992, pp. 1–40. [Online]. Available: https://doi.org/10.1007/3-540-55511-0 1

    1992 doi

  2. [10]

    Notes on sconing and relators,

    J. C. Mitchell and A. Scedrov, “Notes on sconing and relators,” in Computer Science Logic. Springer Berlin Heidelberg, 1993, pp. 352–

    1993

  3. [11]

    A new characterization of lambda definability,

    A. Jung and J. Tiuryn, “A new characterization of lambda definability,” inTyped Lambda Calculi and Applications, M. Bezem and J. F. Groote, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 1993, pp. 245–257. [Online]. Available: https://doi.org/10.1007/BFb0037110

    1993 doi

  4. [12]

    A characterization of lambda definability in categorical models of implicit polymorphism,

    M. Alimohamed, “A characterization of lambda definability in categorical models of implicit polymorphism,”Theor. Comput. Sci., vol. 146, no. 1-2, pp. 5–23, Jul. 1995. [Online]. Available: http://dx.doi.org/10.1016/0304-3975(94)00283-O

    1995 doi

  5. [13]

    Jacobs,Categorical Logic and Type Theory, ser

    B. Jacobs,Categorical Logic and Type Theory, ser. Studies in Logic and the Foundations of Mathematics. Amsterdam: North Holland, 1999, no. 141

    1999

  6. [14]

    A characterisation of lambda definability with sums viaJJ-closure operators,

    S. Katsumata, “A characterisation of lambda definability with sums viaJJ-closure operators,” inComputer Science Logic, M. Kaminski and S. Martini, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 278–292. [Online]. Available: https: //doi.org/10.1007/978-3-540-87531-4 21

    2008 doi

  7. [15]

    Relating computational effects byJJ-lifting,

    ——, “Relating computational effects byJJ-lifting,”Information and Computation, vol. 222, pp. 228 – 246, 2013, 38th International Colloquium on Automata, Languages and Programming (ICALP 2011). [Online]. Available: https://doi.org/10.1016/j.ic.2012.10.014

    2013 doi

  8. [16]

    Notions of computation and monads,

    E. Moggi, “Notions of computation and monads,”Inf. Comput., vol. 93, no. 1, pp. 55–92, 1991. [Online]. Available: https: //doi.org/10.1016/0890-5401(91)90052-4

    1991 doi

  9. [17]

    R. L. Crole,Categories for Types. Cambridge University Press, Jan

  10. [18]

    Logical relations for monadic types,

    J. Goubault-Larrecq, S. Lasota, and D. Nowak, “Logical relations for monadic types,” inComputer Science Logic. Springer Berlin Heidelberg, 2002, pp. 553–568. [Online]. Available: https://doi.org/10. 1007/3-540-45793-3 37

    2002

  11. [19]

    Logical relations for monadic types,

    ——, “Logical relations for monadic types,”Mathematical Structures in Computer Science, vol. 18, no. 06, p. 1169, Oct. 2008. [Online]. Available: https://doi.org/10.1017/S0960129508007172

    2008 doi

  12. [20]

    A semantic formulation ofJJ-lifting and logical predicates for computational metalanguage,

    S. Katsumata, “A semantic formulation ofJJ-lifting and logical predicates for computational metalanguage,” inComputer Science Logic. Springer Berlin Heidelberg, 2005, pp. 87–102. [Online]. Available: https://doi.org/10.1007/11538363 8

    2005 doi

  13. [21]

    Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics,

    O. Kammar and D. McDermott, “Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics,” Electronic Notes in Theoretical Computer Science, vol. 341, pp. 239 – 260, 2018, proceedings of the Thirty-Fourth Conference on the Mathematical F...

    2018 doi

  14. [22]

    Codensity lifting of monads and its dual,

    S.-y. Katsumata, T. Sato, and T. Uustalu, “Codensity lifting of monads and its dual,”Logical Methods in Computer Science, vol. 14, no. 4,

  15. [23]

    Fully abstract models for effectfulλ-calculi via category-theoretic logical relations,

    O. Kammar, S. Katsumata, and P. Saville, “Fully abstract models for effectfulλ-calculi via category-theoretic logical relations,”Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, pp. 1–28, Jan. 2022. [Online]. Available: https://doi.org/10.1145/3498705

    2022 doi

  16. [24]

    Strong functors and monoidal monads,

    A. Kock, “Strong functors and monoidal monads,”Archiv der Mathematik, vol. 23, no. 1, pp. 113–120, dec 1972. [Online]. Available: https://doi.org/10.1007/BF01304852

    1972 doi

  17. [25]

    What makes a strong monad?

    D. McDermott and T. Uustalu, “What makes a strong monad?” Electronic Proceedings in Theoretical Computer Science, vol. 360, pp. 113–133, Jun. 2022. [Online]. Available: https://doi.org/10.4204/ EPTCS.360.6

    2022

  18. [26]

    P. J. Freyd and A. ˘S˘cedrov,Categories, allegories, transferred to digital print. ed., ser. North Holland mathematical library. Amsterdam [u.a.]: North-Holland, 2006, no. 39

    2006

  19. [27]

    Artin glueing,

    G. Wraith, “Artin glueing,”Journal of Pure and Applied Algebra, vol. 4, no. 3, pp. 345–348, Jun. 1974. [Online]. Available: https://doi.org/10.1016/0022-4049(74)90014-0

    1974 doi

  20. [28]

    Connected limits, familial representability and artin glueing,

    A. Carboni and P. Johnstone, “Connected limits, familial representability and artin glueing,”Mathematical Structures in Computer Science, vol. 5, no. 4, pp. 441–459, Dec. 1995, See also the corrigendaCorrigenda for ‘Connected limits, familial representability and Artin glueing...

    1995 doi

  21. [29]

    Actegories for the working amthematician,

    M. Capucci and B. Gavranovi ´c, “Actegories for the working amthematician,” 2022. [Online]. Available: https://doi.org/10.48550/ ARXIV .2203.16351

    2022 doi arXiv

  22. [30]

    The formal semantics of computer languages and their interpretations,

    R. Milner, “The formal semantics of computer languages and their interpretations,” University of Oxford, Tech. Rep., 1974, available online at cs.ox.ac.uk/files/3286/PRGX13.pdf

    1974

  23. [31]

    Framed bicategories and monoidal fibrations,

    M. Shulman, “Framed bicategories and monoidal fibrations,”Theory and Applications of Categories, vol. 20, no. 18, 2008. [Online]. Available: tac.mta.ca/tac/volumes/20/18/20-18.pdf

    2008

  24. [32]

    On enriched fibrations,

    C. Vasilakopoulou, “On enriched fibrations,”Cahiers de topologie et g ´eom´etrie diff ´erentielle cat ´egoriques, vol. LIX, no. 4, 2018. [Online]. Available: https://cahierstgdc.com/wp-content/uploads/2018/ 10/Vasilakopoulou-LIX-4.pdf

    2018

  25. [33]

    Monoidal Grothendieck construction,

    J. Moeller and C. Vasilakopoulou, “Monoidal Grothendieck construction,”Theory and Applications of Categories, vol. 35, no. 31,

  26. [34]

    Logiques, cat ´egories et machines,

    Y . Lafont, “Logiques, cat ´egories et machines,” Ph.D. dissertation, Uni- versit´e Paris VII, 1987

    1987

  27. [35]

    Semantic analysis of normalisation by evaluation for typed lambda calculus,

    M. Fiore, “Semantic analysis of normalisation by evaluation for typed lambda calculus,” inProceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, ser. PPDP ’02. New York, NY , USA: ACM, 2002, pp. 26–37. [Online]. Avail...

    2002

  28. [36]

    Towards a mathematical operational semantics,

    D. Turi and G. Plotkin, “Towards a mathematical operational semantics,” inProceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, 1997, pp. 280–291. [Online]. Available: https://doi.org/10.1109/LICS.1997.614955

    1997

  29. [37]

    Goncharov, A

    S. Goncharov, A. Santamaria, L. Schr ¨oder, S. Tsampas, and H. Urbat,Logical Predicates in Higher-Order Mathematical Operational Semantics. Springer Nature Switzerland, 2024, pp. 47–69. [Online]. Available: https://doi.org/10.1007/978-3-031-57231-9 3

    2024 doi

  30. [38]

    Bialgebraic reasoning on higher-order program equivalence,

    S. Goncharov, S. Milius, S. Tsampas, and H. Urbat, “Bialgebraic reasoning on higher-order program equivalence,” inProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, ser. LICS ’24. New York, NY , USA: Association for Computing Machinery,

  31. [39]

    Abstract operational methods for call-by-push-value,

    S. Goncharov, S. Tsampas, and H. Urbat, “Abstract operational methods for call-by-push-value,”Proceedings of the ACM on Programming Languages, vol. 9, no. POPL, pp. 1013–1039, Jan. 2025

    2025

  32. [40]

    An algebraic theory of type-and-effect systems,

    O. Kammar, “An algebraic theory of type-and-effect systems,” Ph.D. dissertation, University of Edinburgh, 2014. [Online]. Available: http://hdl.handle.net/1842/8910

    2014

  33. [41]

    Reasoning about effectful programs and evaluation order,

    D. McDermott, “Reasoning about effectful programs and evaluation order,” Ph.D. dissertation, University of Cambridge, 2020. [Online]. Available: https://doi.org/10.48456/tr-948

    2020 doi

  34. [42]

    Denotational foundations for expected cost analysis,

    P. H. Azevedo de Amorim, “Denotational foundations for expected cost analysis,”Proc. ACM Program. Lang., vol. 9, no. OOPSLA1, Apr

  35. [43]

    Borceux,Handbook of Categorical Algebra, volume 2

    F. Borceux,Handbook of Categorical Algebra, volume 2. Cambridge University Press, Aug. 1994. [Online]. Available: https://doi.org/10. 1017/CBO9780511525865.008

    1994

  36. [44]

    V-graded categories and V-W-bigraded categories: Functor categories and bifunctors over non-symmetric bases,

    R. B. B. Lucyshyn-Wright, “V-graded categories and V-W-bigraded categories: Functor categories and bifunctors over non-symmetric bases,”

  37. [45]

    Leinster,Higher Operads, Higher Categories

    T. Leinster,Higher Operads, Higher Categories. Cambridge University Press, Jul. 2004, preprint available online at https://doi.org/10.48550/ arXiv.math/0305049

    2004 doi arXiv

  38. [46]

    Johnson and D

    N. Johnson and D. Yau,2-Dimensional Categories. Oxford University Press, 2021, preprint available online at 10.48550/arXiv.2002.06055

    2021 doi arXiv

  39. [47]

    Eine Bemerkung ¨uber Monaden und adjungierte Funktoren,

    D. Pumpl ¨un, “Eine Bemerkung ¨uber Monaden und adjungierte Funktoren,”Mathematische Annalen, vol. 185, pp. 329–337, 1970. [Online]. Available: http://eudml.org/doc/161964

    1970

  40. [48]

    Adjonctions et monades au niveau des 2-cat ´egories,

    C. Auderset, “Adjonctions et monades au niveau des 2-cat ´egories,” Cahiers de Topologie et G ´eom´etrie Diff´erentielle Cat´egoriques, vol. 15, no. 1, pp. 3–20, 1974. [Online]. Available: http://eudml.org/doc/91131

    1974

  41. [49]

    The free adjunction,

    S. Schanuel and R. Street, “The free adjunction,”Cahiers de Topologie et G ´eom´etrie Diff ´erentielle Cat ´egoriques, vol. 27, no. 1, pp. 81– 83, 1986. [Online]. Available: https://www.numdam.org/item/CTGDC 1986 27 1 81 0/

    1986

  42. [50]

    Conspectus of variable categories,

    R. Street, “Conspectus of variable categories,”Journal of Pure and Applied Algebra, vol. 21, no. 3, pp. 307–338, Jun. 1981. [Online]. Available: https://doi.org/10.1016/0022-4049(81)90021-9

    1981 doi

  43. [51]

    Available: https://doi.org/10.48550/ARXIV .2502.18557

    [Online]. Available: https://doi.org/10.48550/ARXIV .2502.18557

    doi arXiv

  44. [52]

    Categorical notions of fibration,

    F. Loregian and E. Riehl, “Categorical notions of fibration,”Expositiones Mathematicae, vol. 38, no. 4, pp. 496–514, Dec. 2020. [Online]. Available: https://doi.org/10.1016/j.exmath.2019.02.004

    2020 doi

  45. [53]

    J. W. Gray,Fibred and Cofibred Categories. Springer Berlin Heidelberg, 1966, pp. 21–83. [Online]. Available: https://doi.org/10. 1007/978-3-642-99902-4 2

    1966

  46. [54]

    Lack,A 2-Categories Companion

    S. Lack,A 2-Categories Companion. Springer New York, Sep. 2009, pp. 105–191. [Online]. Available: https://doi.org/10.1007/ 978-1-4419-1524-5 4

    2009

  47. [55]

    A general coherence result,

    A. Power, “A general coherence result,”Journal of Pure and Applied Algebra, vol. 57, no. 2, pp. 165–173, Mar. 1989. [Online]. Available: https://doi.org/10.1016/0022-4049(89)90113-8

    1989 doi

  48. [56]

    Two-dimensional monad theory,

    R. Blackwell, G. Kelly, and A. Power, “Two-dimensional monad theory,” Journal of Pure and Applied Algebra, vol. 59, no. 1, pp. 1–41, Jul. 1989. [Online]. Available: https://doi.org/10.1016/0022-4049(89)90160-6

    1989 doi

  49. [57]

    Yoneda structures from 2-toposes,

    M. Weber, “Yoneda structures from 2-toposes,”Applied Categorical Structures, vol. 15, no. 3, pp. 259–323, May 2007. [Online]. Available: https://doi.org/10.1007/s10485-007-9079-2

    2007 doi

  50. [58]

    Springer Berlin Heidelberg, 1974, pp

    ——,Fibrations and Yoneda’s lemma in a 2-category. Springer Berlin Heidelberg, 1974, pp. 104–133. [Online]. Available: https: //doi.org/10.1007/bfb0063102

    1974 doi

  51. [59]

    Call-by-push-value: Decomposing call-by-value and call-by- name,

    ——, “Call-by-push-value: Decomposing call-by-value and call-by- name,”Higher-Order and Symbolic Computation, vol. 19, no. 4, pp. 377–414, Dec. 2006. [Online]. Available: https://doi.org/10.1007/ s10990-006-0480-6

    2006

  52. [60]

    G. M. Kelly,Basic Concepts of Enriched Category Theory. Reprints in Theory and Applications of Categories, 2005. [Online]. Available: http://www.tac.mta.ca/tac/reprints/articles/10/tr10.pdf

    2005

  53. [61]

    Computational lambda-calculus and monads,

    E. Moggi, “Computational lambda-calculus and monads,” in Proceedings of the Fourth Annual Symposium on Logic in Computer Science. IEEE Press, 1989, p. 14–23. [Online]. Available: https://doi.org/10.1109/LICS.1989.39155

    1989

  54. [62]

    Eilenberg and G

    S. Eilenberg and G. M. Kelly,Closed Categories. Springer Berlin Heidelberg, 1966, pp. 421–562. [Online]. Available: https: //doi.org/10.1007/978-3-642-99902-4 22

    1966 doi

  55. [63]

    Normed spaces and the change of base for enriched categories,

    G. S. H. Cruttwell, “Normed spaces and the change of base for enriched categories,” Ph.D. dissertation, Dalhousie University, 2008, available online at https://www.reluctantm.com/gcruttw/publications/thesis4.pdf

    2008

  56. [64]

    Grothendieck construction for bicategories,

    I. Bakovi ´c, “Grothendieck construction for bicategories,” 2010. [Online]. Available: https://www2.irb.hr/korisnici/ibakovic/sgc.pdf

    2010

  57. [65]

    Adjunction models for call-by-push-value with stacks,

    P. B. Levy, “Adjunction models for call-by-push-value with stacks,” Electronic Notes in Theoretical Computer Science, vol. 69, pp. 248–271, 2003, cTCS’02, Category Theory and Computer Science. [Online]. Available: https://doi.org/10.1016/S1571-0661(04)80568-1

    2003 doi

  58. [66]

    Factorization systems and fibrations,

    J. Hughes and B. Jacobs, “Factorization systems and fibrations,” Electronic Notes in Theoretical Computer Science, vol. 69, pp. 156–182, Feb. 2003. [Online]. Available: https://doi.org/10.1016/ S1571-0661(04)80564-4

    2003

  59. [67]

    F. E. J. Linton,Coequalizers in categories of algebras. Springer Berlin Heidelberg, 1969, pp. 75–90. [Online]. Available: https: //doi.org/10.1007/BFb0083082

    1969 doi

  60. [68]

    Nishizawa, S.-y

    K. Nishizawa, S.-y. Katsumata, and Y . Komorida,Stone Dualities from Opfibrations. Springer International Publishing, 2020, pp. 221–236. [Online]. Available: https://doi.org/10.1007/978-3-030-43520-2 14

    2020 doi

  61. [69]

    The formal theory of monads,

    R. Street, “The formal theory of monads,”Journal of Pure and Applied Algebra, vol. 2, no. 2, pp. 149 –168, 1972. [Online]. Available: https://doi.org/10.1016/0022-4049(72)90019-9

    1972 doi

  62. [70]

    Categorical glueing and logical predicates for models of linear logic,

    M. Hasegawa, “Categorical glueing and logical predicates for models of linear logic,”Kyoto University. Research Institute for Mathematical Sciences [RIMS], 1999. [Online]. Available: https: //www.kurims.kyoto-u.ac.jp/„hassei/papers/full.pdf

    1999

  63. [71]

    Remarks on isomorphisms in typed lambda calculi with empty and sum types,

    M. Fiore, R. Di Cosmo, and V . Balat, “Remarks on isomorphisms in typed lambda calculi with empty and sum types,” inProceedings 17th Annual IEEE Symposium on Logic in Computer Science, ser. LICS-02. IEEE Comput. Soc, 2002, pp. 147–156. [Online]. Available: https://doi.org/10.1...

    2002 arXiv

  64. [72]

    Fibred 2-categories and bicategories,

    M. Buckley, “Fibred 2-categories and bicategories,”Journal of Pure and Applied Algebra, vol. 218, no. 6, pp. 1034–1074, Jun. 2014. [Online]. Available: https://www.sciencedirect.com/science/article/pii/ S0022404913002065?via=ihub

    2014

  65. [73]

    On the Lambek embedding and the category of product-preserving presheaves,

    P. Fu, K. Kishida, N. J. Ross, and P. Selinger, “On the Lambek embedding and the category of product-preserving presheaves,”arXiv,

  66. [74]

    Normalization by evaluation for call- by-push-value and polarized lambda calculus,

    A. Abel and C. Sattler, “Normalization by evaluation for call- by-push-value and polarized lambda calculus,” inProceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, ser. PPDP ’19. New York, NY , USA: Association for Computing Ma...

    2019

  67. [75]

    Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures,

    M. Fiore, N. Gambino, M. Hyland, and G. Winskel, “Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures,”Selecta Mathematica, vol. 24, no. 3, pp. 2791–2830, Nov

  68. [76]

    Limits for lax morphisms,

    S. Lack, “Limits for lax morphisms,”Applied Categorical Structures, vol. 13, no. 3, pp. 189–203, Jun. 2005. [Online]. Available: https://doi.org/10.1007/s10485-005-2958-5

    2005 doi

  69. [77]

    Enhanced 2-categorical structures, two- dimensional limit sketches and the symmetry of internalisation,

    N. Arkor, J. Bourke, and J. Ko, “Enhanced 2-categorical structures, two- dimensional limit sketches and the symmetry of internalisation,”arXiv,

  70. [78]

    Mac Lane,Categories for the Working Mathematician, 2nd ed., ser

    S. Mac Lane,Categories for the Working Mathematician, 2nd ed., ser. Graduate Texts in Mathematics. Springer-Verlag New York, 1998, vol. 5. APPENDIXA THE BASIC DEFINITIONS OF2-CATEGORY THEORY We briefly review the definitions of 2-categories, 2-functors, transformations, and mo...

    1998

  71. [79]

    Fiore and P

    M. Fiore and P. Saville,Relative Full Completeness for Bicategorical Cartesian Closed Structure. Springer International Publishing, 2020, pp. 277–298. [Online]. Available: https: //doi.org/10.1007/978-3-030-45231-5 15

    2020 doi

  72. [87]

    Available: https://doi.org/10.48550/arXiv.2412.07475

    [Online]. Available: https://doi.org/10.48550/arXiv.2412.07475

    doi arXiv

  73. [89]

    A collection of objectsA, B,

  74. [90]

    For all objectsAandB, a collection of morphisms from AtoB, which are themselves related by morphisms: thus we have ahom-categoryCpA, Bqwhose objectsf, g: AÑBaremorphisms(or1-cells) and whose morphisms are2-cellsσ, τ:fñg

  75. [91]

    The hom-category structure means the following

    For allA, BandCacompositionfunctor˝ A,B,C : CpB,CqˆCpA, BqÑCpA, Cqand, for allAanidentity 1-cellid A :AÑA, such that composition is associative and unital on both 1-cells and 2-cells. The hom-category structure means the following. For any 1-cellf:AÑBthere is an identity 2-cel...

  76. [92]

    A collection|C|of objectsA, B,

  77. [93]

    Thus for eachA, BPCwe have a setC cpA, Bqofmorphisms over c, denotedf:AÝ Ñ c B

    For eachcPCa categoryC c with objects|C|. Thus for eachA, BPCwe have a setC cpA, Bqofmorphisms over c, denotedf:AÝ Ñ c B

  78. [94]

    We drop the subscripts where they are clear from context

    For eachρ:dÑcinCan identity-on-objects functor p´qŸρ:C c ÑC d, subject to the following axioms for ρ1 :eÑd,f:AÝ Ñ c Bandg:BÝ Ñ c C: fŸid c“f fŸpρ˝ρ 1q“pfŸρqŸρ 1 Definition B.2.AlocallyC-indexed functorF:CÑD consists of a mapping|F|:|C| Ñ |D|on objects and, for everycPCandA, BP...

  79. [378]

    Available: https://doi.org/10.1007/3-540-56992-8 21

    [Online]. Available: https://doi.org/10.1007/3-540-56992-8 21

    doi

  80. [1994]

    Available: https://doi.org/10.1017/CBO9781139172707

    [Online]. Available: https://doi.org/10.1017/CBO9781139172707

    doi

  81. [2017]

    Available: https://doi.org/10.1007/s00029-017-0361-3

    [Online]. Available: https://doi.org/10.1007/s00029-017-0361-3

    doi

  82. [2018]

    Available: https://doi.org/10.23638/LMCS-14(4:6)2018

    [Online]. Available: https://doi.org/10.23638/LMCS-14(4:6)2018

    2018 doi

  83. [2020]

    Available: www.tac.mta.ca/tac/volumes/35/31/35-31.pdf

    [Online]. Available: www.tac.mta.ca/tac/volumes/35/31/35-31.pdf

  84. [2022]

    Available: https://doi.org/10.48550/arXiv.2205.06068

    [Online]. Available: https://doi.org/10.48550/arXiv.2205.06068

    doi arXiv

  85. [2024]

    Available: https://doi.org/10.1145/3661814.3662099

    [Online]. Available: https://doi.org/10.1145/3661814.3662099

  86. [2025]

    Available: https://doi.org/10.1145/3720424

    [Online]. Available: https://doi.org/10.1145/3720424

    doi

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.