I do type theory and category theory, I mean ∞-ones. I am currently a 特任助教 at School of Informatics, Nagoya University. My research interests are homotopy type theory, category theory, type theory, logic, and computer science.

Papers

Publications

• A General Framework for the Semantics of Type Theory. Mathematical Structures in Computer Science, 2023. doi:10.1017/S0960129523000208 arXiv:1904.04097
• Homotopy type theory as internal languages of diagrams of ∞-logoses. 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), 2023. doi:10.4230/LIPIcs.FSCD.2023.5 This is a short version of arXiv:2212.02444.
• On Church’s Thesis in Cubical Assemblies (joint with Andrew Swan). Mathematical Structures in Computer Science, 2022. doi:10.1017/S0960129522000068
• The universal exponentiable arrow. Journal of Pure and Applied Algebra, Volume 226, Issue 7, 2022. doi:10.1016/j.jpaa.2021.106991
• Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing. 24th International Conference on Types for Proofs and Programs (TYPES 2018), 2019. doi:10.4230/LIPICS.TYPES.2018.7
• Fibred Fibration Categories. 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2017. doi:10.1109/LICS.2017.8005084 arXiv:1602.08206

Preprints

• An elementary definition of opetopic sets. 2025. arXiv:2504.14935
• Higher inductive types in (∞,1)-categories. 2024. arXiv:2410.17615
• Normalization and coherence for ∞-type theories. 2022. arXiv:2212.11764
• Homotopy type theory as internal languages of diagrams of ∞-logoses. 2022. arXiv:2212.02444 This is an extended version of the FSCD 2023 paper.
• ∞-type theories (joint with Hoang Kim Nguyen). 2022. arXiv:2205.00798
• Homotopies for Free! 2017. arXiv:1701.07937

PhD Thesis

Abstract and Concrete Type Theories. Institute for Logic, Language and Computation, University of Amsterdam, 9 July, 2021. abstract pdf UvA DARE

Other documents

• Synthetic topos theory. Under construction.
• ホモトピー型理論 ホモトピー型理論についての日本語文書。 書きかけ。
• 「正しい」圏論
• A characterization of open modalities in homotopy type theory
• A universal property of the (∞, 1)-category of presentable (∞, 1)-categories Notes for the talk presented at PSSL 106.
• トポスと高階論理
• Grothendieck ファイブレーション
• ホモトピー型理論入門
• Functor Categories of a Locally Cartesian Closed Category

Talks

• Homotopy Type TheoryとCubical Type Theory. 東北大学コンピュータサイエンス研究会講演会, 2025年3月21日, 仙台. slides
• ホモトピー型理論とUnivalent Foundations入門. ロジックウィンタースクールIII, 2025年2月17–21日, 和光. slides
• An elementary definition of opetopic sets.
  • Kyoto Category Theory Meeting, February 12, 2025, Kyoto. slides
  • CSCAT 2025, March 10, 2025, Kumamoto. slides
• Higher inductive types in (∞,1)-categories. Workshop on Categorical Structures and Computer Science (2024 Edition), November 1, 2024, Kyoto.
• Homotopy type theory as internal languages of diagrams of ∞-logoses. 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), July 4, 2023, Roma. slides
• Towards modular proof of normalization for type theories. EuroProofNet WG6 meeting, April 24–25, 2023, Vienna. slides
• Normalization and coherence for ∞-type theories. Invited talk at The 8th KTGU Mathematics Workshop for Young Researchers, January 30, 2023, Kyoto.
• Internal languages of diagrams of ∞-toposes. Invited talk at Workshop on Homotopy Type Theory/ Univalent Foundations, July 31, 2022, Haifa. notes
• Normalization for initial space-valued models of type theories. Invited talk at EuroProofNet WG6 kick-off meeting: Syntax and Semantics of Type Theories, May 21, 2022, Stockholm. slides
• Introduction to Homotopy Type Theory and Univalent Foundations of Mathematics. Logic Summer School, December, 2021, Australian National University.
• ∞-type theories and internal language conjecture. Homotopy Type Theory Electronic Seminar Talks, December 2, 2021, Online. slides video
• ∞-type theories. Workshop on Homotopy Type Theory/ Univalent Foundations, July 5, 2020, Online. abstract video
• Abstract type theories. HoTTEST Conference 2020, June 17, 2020, Online. slides video
• Cubical Assembly Models of Homotopy Type Theory. Invited talk at HoTT-UF, June 13, 2019, Oslo, Norway.
• A General Framework for the Semantics of Type Theory.
  • International Conference on Homotopy Type Theory (HoTT 2019), August 16, 2019, Pittsburgh, USA. slides
  • Category Theory 2019, July 9, 2019, Edinburgh, Scotland. slides
  • 25th International Conference on Types for Proofs and Programs (TYPES 2019), June 11, 2019, Oslo, Norway.
• Cubical Assemblies and the Independence of the Propositional Resizing Axiom.
  • Workshop on Homotopy Type Theory/ Univalent Foundations, July 7-8, 2018, Oxford, United Kingdom. slides
  • 24th International Conference on Types for Proofs and Programs (TYPES 2018), June 18-21, 2018, Braga, Portugal. slides
• Fibred Fibration Categories. Workshop on Homotopy Type Theory / Univalent Foundations, June 25–26, 2016, Porto, Portugal. slides

Awards

• Best Paper Award by Junior Researchers at FSCD 2023, July 3–6, 2023, Roma, Italy.
• Best Student Paper Award at HoTT 2019, August 12–17, 2019, Pittsburgh, USA.

Activities

• Part of organizers of Workshop on Homotopy Type Theory/ Univalent Foundations 2023

SNS accounts

• ORCID: 0000-0003-4930-1384
• GitHub: uemurax
• Mastodon: @tuemura@mathtod.online
• Twitter: t_uemura669101
• Kaggle: taichiuemura