Journal Articles

  • Double Categories of Relations Relative to Factorisation Systems

    Keisuke Hoshino, Hayato Nasu double category
    Applied Categorical Structures, 33(2), 11, 2025 arXiv
    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.

    Cite 
    @article{hoshino2025double,
  author = {Hoshino, Keisuke and Nasu, Hayato},
  title = {Double Categories of Relations Relative to Factorisation Systems},
  journal = {Applied Categorical Structures},
  volume = {33},
  number = {2},
  pages = {11},
  year = {2025},
  doi = {10.1007/s10485-025-09799-y}
}

Preprints

  • On the decomposition of a strong epimorphism into regular epimorphisms

    Yuto Kawase, Hayato Nasu algebraic theorytype theory
    arXiv preprint, 2026 arXiv
    Abstract

    Strong epimorphisms and regular epimorphisms are two important classes of morphisms, and they do not coincide in general. Yet, in a locally presentable category, it is known that any strong epimorphism can be decomposed into a transfinite composite of regular epimorphisms. In this paper, we provide two syntactic methods to determine how many regular epimorphisms are needed in such a decomposition, using partial Horn theory and generalized algebraic theory. We start by discussing a general problem of decomposing a morphism into a transfinite composite of morphisms in a given class, which also covers the decomposition of an adjoint functor into monadic functors.

    Cite 
    @article{kawase2026decomposition,
  author = {Kawase, Yuto and Nasu, Hayato},
  title = {On the decomposition of a strong epimorphism into regular epimorphisms},
  journal = {arXiv preprint arXiv:2604.05744},
  year = {2026}
}

  • An Internal Logic of Virtual Double Categories

    Hayato Nasu double categorytype theory
    arXiv preprint, 2024 PDF arXiv
    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.

    Cite 
    @article{nasu2024internal,
  author = {Nasu, Hayato},
  title = {An Internal Logic of Virtual Double Categories},
  journal = {arXiv preprint arXiv:2410.06792},
  year = {2024}
}

Theses

  • Logical Aspects of Virtual Double Categories

    Hayato Nasu
    Kyoto University — Master's Thesis, 2025 PDF arXiv
    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.

    This is the version updated after the thesis defence (not every error is corrected). The originally submitted version is also available.

    Cite 
    @mastersthesis{nasu2025logical,
  author = {Nasu, Hayato},
  title = {Logical Aspects of Virtual Double Categories},
  school = {Kyoto University},
  address = {Kyoto},
  year = {2025}
}