Logical Aspects of Virtual Double Categories
Hayato Nasu
TL;DR
This work develops a double-categorical approach to categorical logic by using virtual double categories as semantic environments for predicate logic and by presenting an internal language, FVDblTT, for virtual double categories. It constructs a 2-functor $\mathbbm{Bil}$ from cartesian fibrations to cartesian fibrational virtual double categories and characterizes elementary existential fibrations as a pullback along a forgetful 2-functor, while identifying Frobenius cartesian equipments as a natural image of this construction. In Chapter 3, it introduces FVDblTT and proves a biadjunction between cartesian-fibrational virtual double categories and specifications for the type theory, with a counit that is pointwise equivalent, thereby formalizing an internal-language viewpoint for virtual double categories. Together, these results illustrate how semantics and syntax can be integrated within a unified double-categorical framework, subsuming existing models of categorical logic and enabling a robust method for reasoning about predicate logic through both semantic and syntactic lenses. The work thereby advances a principled, structurally rich bridge between logical semantics and syntactic presentations in higher-dimensional category theory.
Abstract
This thesis deals with two main topics: virtual double categories as semantics environments for predicate logic, and a syntactic presentation of virtual double categories as a type theory. One significant principle of categorical logic is bringing together the semantics and the syntax of logical systems in a common categorical framework. This thesis is intended to propose a double-categorical method for categorical logic in line with this principle. On the semantic side, we investigate virtual double categories as a model of predicate logic and illustrate that this framework subsumes the existing frameworks properly. On the syntactic side, we develop a type theory called FVDblTT that is designed as an internal language for virtual double categories.