Hayato Nasu 奈須隼大

I am a master's student at RIMS, Kyoto University, Japan.

I am a member of the Computer Science Group.

Research Interests

I am interested in the following topics:

• Categorical Logic – topos theory, hyperdoctrines, categorical semantics of type theory
• Category Theory – toposes, double categories, higher categories
• Type Theory – homotopy type theory, structural set theory

Preprints on ArXiv

• 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.

• Double Categories of Relations Relative to Factorisation Systems, with Keisuke Hoshino (2023)
  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.

Talks

• A Formal Theory of Anticolimits given at the workshop on Computer Science and Categorical Structures, on October 31 2024. Slides

• Double categories of Relations Relative to Factorization Systems given at CT2024, on June 25 2024. Slides

• (Hyper)doctrines as virtual double categories CSCAT2024 at the University of Chiba, on March 14 2024. Slides

• Structural Set Theory -- Towards SEFAR -- the Mathematical Foundations seminar for Young Generation 2023, on December 08 2023. Slides

• Double categories of Relations Relative to Factorisation Systems given at the Thursday Seminar at RIMS, Kyoto University, on November 16 2023. Slides

Friends and colleagues

• Keisuke Hoshino
• Yuto Kawase
• Kengo Hirata
• Ryuya Hora
• Takahiro Sanada
• Yuki Maehara

Notes

• A note on SEAR 2023.12.08 under construction

For other notes written in Japanese: Japanese page