Research papers

Published

• Double Categories of Relations Relative to Factorisation Systems, with Keisuke Hoshino. Appl Categor Struct 33, 11 (2025).
  https://doi.org/10.1007/s10485-025-09799-y
  arXiv:2310.19428

  Abstract

  We relativise double categories of relations to stable orthogonal factorisation systems. Furthermore, we present the characterisation of the relative double categories of relations in two ways. The first utilises a generalised comprehension scheme, and the second focuses on a specific class of vertical arrows defined solely double-categorically. We organise diverse classes of double categories of relations and correlate them with significant classes of factorisation systems. Our framework embraces double categories of spans and double categories of relations on regular categories, which we meticulously compare to existing work on the characterisations of bicategories and double categories of spans and relations.

Preprints on ArXiv

• Logical Aspects of Virtual Double Categories (2025) (master's thesis)
  arXiv:2501.17869 Updated version (2025/03/13)

• An Internal Logic of Virtual Double Categories (2024)
  arXiv:2410.06792 Updated version (2024/10/10)

  Abstract

  We present a type theory called fibrational virtual double type theory (FVDblTT) designed specifically for formal category theory, which is a succinct reformulation of New and Licata’s Virtual Equipment Type Theory (VETT). FVDblTT formalizes reasoning on isomorphisms that are commonly employed in category theory. Virtual double categories are one of the most successful frameworks for developing formal category theory, and FVDblTT has them as a theoretical foundation. We validate its worth as an internal language of virtual double categories by providing a syntax-semantics duality between virtual double categories and specifications in FVDblTT as a biadjunction.