Univalent categories, displayed categories, and fibrations.
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. 2013. https://homotopytypetheory.org/book
- Benedikt Ahrens, Chris Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, Volume 25, Special Issue 5, 2015. https://doi.org/10.1017/S0960129514000486
- Amélia Liao. Univalent Category Theory. Homotopy Type Theory Electronic Seminar Talks, 2022. https://www.uwo.ca/math/faculty/kapulkin/seminars/hottestfiles/Liao-2022-10-06-HoTTEST.pdf
- Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. Logical Methods in Computer Science, Volume 15, Issue 1, 2019. https://doi.org/10.23638/LMCS-15(1:20)2019
- Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, and Niels van der Weide. Bicategories in Univalent Foundations. Mathematical Structures in Computer Science, 31(10), 2021. https://doi.org/10.1017/S0960129522000032 https://arxiv.org/abs/1903.01152