I am a postdoc at the Department of Mathematics at Stockholm University. My main research interests are in Homotopy Type Theory, in particular its semantics using (higher) category theory. I am also interested in type theory in general and pure category theory.
Papers
Publications
- 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
- Normalization and coherence for ∞-type theories. 2022. arXiv:2212.11764
- Homotopy type theory as internal languages of diagrams of ∞-logoses. 2022. arXiv:2212.02444
- ∞-type theories (joint with Hoang Kim Nguyen). 2022. arXiv:2205.00798
- A General Framework for the Semantics of Type Theory. 2019. arXiv:1904.04097
- 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
- ホモトピー型理論 ホモトピー型理論についての日本語文書。 ほぼほぼ工事中。
- 「正しい」圏論
- 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
- 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 Student Paper Award at International Conference on Homotopy Type Theory (HoTT 2019), August 12–17, 2019, Pittsburgh, USA.
Activities
- Part of organizers of Workshop on Homotopy Type Theory/ Univalent Foundations 2023
Contact
See my profile at the university site.