We adapt Fiore, Plotkin, and Turi’s treatment of abstract syntax with binding, substitution, and holes to account for languages with second-class sorts. These situations include programming calculi such as the Call-by-Value lambda-calculus (CBV) and Levy’s Call-by-Push-Value (CBPV). Prohibiting second-class sorts from appearing in variable contexts changes the characterisation of the abstract syntax from monoids in monoidal categories to actions in actegories. We reproduce much of the development through bicategorical arguments. We apply the resulting theory by proving substitution lemmata for varieties of CBV.

Orthogonality is a notion based on the duality between programs and their environments used to determine when they can be safely combined. For instance, it is a powerful tool to establish termination properties in classical formal systems. It was given a general treatment with the concept of orthogonality category, of which numerous models of linear logic are instances, by Hyland and Schalk. This paper considers the subclass of focused orthogonalities. We develop a theory of fixpoint constructions in focused orthogonality categories. Central results are lifting theorems for initial algebras and final coalgebras. These crucially hinge on the insight that focused orthogonality categories are relational fibrations. The theory provides an axiomatic categorical framework for models of linear logic with least and greatest fixpoints of types. We further investigate domain-theoretic settings, showing how to lift bifree algebras, used to solve mixed-variance recursive type equations, to focused orthogonality categories.

We develop a constructive theory of finite multisets in Homotopy Type Theory, defining them as free commutative monoids. After recalling basic structural properties of the free commutative-monoid construction, we formalise and establish the categorical universal property of two, necessarily equivalent, algebraic presentations of free commutative monoids using 1-HITs. These presentations correspond to two different equational theories invariably including commutation axioms. In this setting, we prove important structural combinatorial properties of finite multisets. These properties are established in full generality without assuming decidable equality on the carrier set. As an application, we present a constructive formalisation of the relational model of classical linear logic and its differential structure. This leads to constructively establishing that free commutative monoids are conical refinement monoids. Thereon we obtain a characterisation of the equality type of finite multisets and a new presentation of the free commutative-monoid construction as a set-quotient of the list construction. These developments crucially rely on the commutation relation of creation/annihilation operators associated with the free commutative-monoid construction seen as a combinatorial Fock space.