We propose a definition of double categories whose composition of 1-cells is weak in both directions. Namely, a doubly weak double category is a double computad—a structure with 2-cells of all possible double-categorical shapes—equipped with all possible composition operations, coherently. We also characterize them using “implicit” double categories, which are double computads having all possible compositions of 2-cells, but no compositions of 1-cells; doubly weak double categories are then obtained by a simple representability criterion. Finally, they can also be defined by adding a “tidiness” condition to the double bicategories of Verity, or to the cubical bicategories of Garner.

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.

Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating not just objects, but also morphisms capturing interactions between objects. Of particular importance in some applications are double categories, which are categories with two classes of morphisms, axiomatizing two different kinds of interactions between objects. These have found applications in many areas of mathematics and theoretical computer science, for instance, the study of lenses, open systems, and rewriting. However, double categories come with a wide variety of equivalences, which makes it challenging to transport structure along equivalences. To deal with this challenge, we propose the univalence maxim: each notion of equivalence of categorical structures has a corresponding notion of univalent categorical structure which induces that notion of equivalence. We also prove corresponding univalence principles, which allow us to transport structure and properties along equivalences. In this way, the usually informal practice of reasoning modulo equivalence becomes grounded in an entirely formal logical principle. We apply this perspective to various double categorical structures, such as (pseudo) double categories and double bicategories. Concretely, we characterize and formalize their definitions in Coq UniMath up to chosen equivalences, which we achieve by establishing their univalence principles.

We prove a strictification theorem for cartesian closed bicategories. First, we adapt Power’s proof of coherence for bicategories with finite bilimits to show that every bicategory with bicategorical cartesian closed structure is biequivalent to a 2-category with 2-categorical cartesian closed structure. Then we show how to extend this result to a Mac Lane-style “all pasting diagrams commute” coherence theorem: precisely, we show that in the free cartesian closed bicategory on a graph, there is at most one 2-cell between any parallel pair of 1-cells. The argument we employ is reminiscent of that used by Čubrić, Dybjer, and Scott to show normalisation for the simply-typed lambda calculus (Čubrić et al., 1998). The main results first appeared in a conference paper (Fiore and Saville, 2020) but for reasons of space many details are omitted there; here we provide the full development.

We present two proofs of coherence for cartesian closed bicategories. Precisely, we show that in the free cartesian closed bicategory on a set of objects there is at most one structural 2-cell between any parallel pair of 1-cells. We thereby reduce the difficulty of constructing structure in arbitrary cartesian closed bicategories to the level of 1-dimensional category theory. Our first proof follows a traditional approach using the Yoneda lemma. For the second proof, we adapt Fiore’s categorical analysis of normalisation-by-evaluation for the simply-typed lambda calculus. Modulo the construction of suitable bicategorical structures, the argument is not significantly more complex than its 1-categorical counterpart. It also opens the way for further proofs of coherence using (adaptations of) tools from categorical semantics.

A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are developed, the latter in terms of (strict) indexed symmetric monoidal categories with comprehension. Various optional type formers are treated in a modular way. In particular, we will see that the historically much-debated multiplicative quantifiers and identity types arise naturally from categorical considerations. These new multiplicative connectives are further characterised by several identities relating them to the usual connectives from dependent type theory and linear logic. Finally, one important class of models, given by families with values in some symmetric monoidal category, is investigated in detail.

Given an algebraic theory which can be described by a (possibly symmetric) operad $𝑃$, we propose a definition of the weakening (or categorification) of the theory, in which equations that hold strictly for $𝑃$-algebras hold only up to coherent isomorphism. This generalizes the theories of monoidal categories and symmetric monoidal categories, and several related notions defined in the literature. Using this definition, we generalize the result that every monoidal category is monoidally equivalent to a strict monoidal category, and show that the “strictification” functor has an interesting universal property, being left adjoint to the forgetful functor from the category of strict $𝑃$-categories to the category of weak $𝑃$-categories. We further show that the categorification obtained is independent of our choice of presentation for $𝑃$, and extend some of our results to many-sorted theories, using multicategories.

We show how to solve the word problem for simply typed λβη-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for these results is 𝒫-category theory, a version of ordinary category theory where each hom-set is equipped with a partial equivalence relation. The part of 𝒫-category theory we develop here is constructive and thus permits extraction of programs from proofs. It is important to stress that in our method we make no use of traditional proof-theoretic or rewriting techniques. To show the robustness of our method, we give an extended treatment for more general λ-theories in the Appendix.