Coherence for bicategorical cartesian closed structure

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.

An interpretation of dependent type theory in a model category of locally cartesian closed categories

Locally cartesian closed (lcc) categories are natural categorical models of extensional dependent type theory. This paper introduces the “gros” semantics in the category of lcc categories: Instead of constructing an interpretation in a given individual lcc category, we show that also the category of all lcc categories can be endowed with the structure of a model of dependent type theory. The original interpretation in an individual lcc category can then be recovered by slicing. As in the original interpretation, we face the issue of coherence: Categorical structure is usually preserved by functors only up to isomorphism, whereas syntactic substitution commutes strictly with all type-theoretic structures. Our solution involves a suitable presentation of the higher category of lcc categories as model category. To that end, we construct a model category of lcc sketches, from which we obtain by the formalism of algebraically (co)fibrant objects model categories of strict lcc categories and then algebraically cofibrant strict lcc categories. The latter is our model of dependent type theory.

Categorical Nonstandard Analysis

In the present paper, we propose a new axiomatic approach to nonstandard analysis and its application to the general theory of spatial structures in terms of category theory. Our framework is based on the idea of internal set theory, while we make use of an endofunctor U on a topos of sets S together with a natural transformation υ, instead of the terms as “standard”, “internal”, or “external”. Moreover, we propose a general notion of a space called U-space, and the category USpace whose objects are U-spaces and morphisms are functions called U-spatial morphisms. The category USpace, which is shown to be Cartesian closed, gives a unified viewpoint toward topological and coarse geometric structure. It will also be useful to further study symmetries/asymmetries of the systems with infinite degrees of freedom, such as quantum fields.

Categorical and algebraic aspects of the intuitionistic modal logic IEL― and its predicate extensions

The system of intuitionistic modal logic $\textbf{IEL}^{-}$ was proposed by S. Artemov and T. Protopopescu as the intuitionistic version of belief logic (S. Artemov and T. Protopopescu. Intuitionistic epistemic logic. The Review of Symbolic Logic, 9, 266–298, 2016). We construct the modal lambda calculus, which is Curry–Howard isomorphic to $\textbf{IEL}^{-}$ as the type-theoretical representation of applicative computation widely known in functional programming.We also provide a categorical interpretation of this modal lambda calculus considering coalgebras associated with a monoidal functor on a Cartesian closed category. Finally, we study Heyting algebras and locales with corresponding operators. Such operators are used in point-free topology as well. We study complete Kripke–Joyal-style semantics for predicate extensions of $\textbf{IEL}^{-}$ and related logics using Dedekind–MacNeille completions and modal cover systems introduced by Goldblatt (R. Goldblatt. Cover semantics for quantified lax logic. Journal of Logic and Computation, 21, 1035–1063, 2011). The paper extends the conference paper published in the LFCS’20 volume (D. Rogozin. Modal type theory based on the intuitionistic modal logic IEL. In International Symposium on Logical Foundations of Computer Science, pp. 236–248. Springer, 2020).

Dynamic game semantics

The present work achieves a mathematical, in particular syntax-independent, formulation of dynamics and intensionality of computation in terms of games and strategies. Specifically, we give game semantics of a higher-order programming language that distinguishes programmes with the same value yet different algorithms (or intensionality) and the hiding operation on strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to a cartesian closed bicategory, and our game semantics forms an instance of a bicategorical generalisation of the standard interpretation of functional programming languages in cartesian closed categories. This work is intended to be a step towards a mathematical foundation of intensional and dynamic aspects of logic and computation; it should be applicable to a wide range of logics and computations.

A Study on Cubic H-Relations in a Topological Universe Viewpoint

We introduce the concrete category CRel P ( H ) [resp. CRel R ( H ) ] of cubic H-relational spaces and P-preserving [resp. R-preserving] mappings between them and study it in a topological universe viewpoint. In addition, we prove that it is Cartesian closed over Set . Next, we introduce the subcategory CRel P , R ( H ) [resp. CRel R , R ( H ) ] of CRel P ( H ) [resp. CRel R ( H ) ] and investigate it in the sense of a topological universe. In particular, we obtain exponential objects in CRel P , R ( H ) [resp. CRel R , R ( H ) ] quite different from those in CRel P ( H ) [resp. CRel R ( H ) ].

Cofree coalgebras and differential linear logic

We prove that the semantics of intuitionistic linear logic in vector spaces which uses cofree coalgebras is also a model of differential linear logic, and that the Cartesian closed category of cofree coalgebras is a model of the simply typed differential λ-calculus.