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