## Preprints

- Awodey, Gambino, Hazratpour, Kripke-Joyal forcing for type theory and uniform fibrations
- Anel, The elementary ∞-topos of truncated coherent spaces
- Anel, Biedermann, Finster and Joyal, Higher Sheaves and Left-Exact Localizations of ∞-Topoi
- Swan, On the Nielsen-Schreier Theorem in Homotopy Type Theory
- Swan, A class of higher inductive types in Zermelo-Fraenkel set theory
- Anel, Subramaniam, Small object arguments, plus-construction, and left-exact localizations
- Frey, Categories of partial equivalence relations as localizations

## Publications

- Frey, J., & Streicher, T. (2021). Triposes as a generalization of localic geometric morphisms.
*Mathematical Structures in Computer Science,*1-10. doi:10.1017/S0960129520000304 - Awodey, S. (2021). Sheaf representations and duality in logic. In:
*Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics*, Claudia Casadio and Philip J. Scott (eds.), Springer-Verlag.

## Slides

- Awodey, S. (2021) Univalence in infinity topoi. Slides from the conference Category Theory 2021 held at the University of Genoa, August 2021.
- Frey, J. (2021) A refinement of Gabriel-Ulmer duality. Slides from the conference Category Theory 2021 held at the University of Genoa, August 2021.
- Swan, A.W. (2021) Some remarks on locally representable algebraic weak factorisation systems. Slides from the conference Category Theory 2021 held at the University of Genoa, August 2021. Video of the talk.
- Frey, J. (2021) Coproducts in infinity-LCCCs with subobject classifier. Slides from the workshop HoTT/UF 2021 held at Buenos Aires, July 2021. Video of the talk.
- Swan, A.W. (2021) The Nielsen-Schreier theorem in homotopy type theory. Slides from the workshop HoTT/UF 2021 held at Buenos Aires, July 2021. Video of the talk.
- Awodey, S. (2021) Polynomial functors and natural models of type theory. Slides from the Workshop on Polynomial Functors held at the Topos Institute, March 2021.
- Awodey, S. (2019) Quillen model structures on cubical sets. Slides from the conference Homotopy Type Theory 2019 held at CMU, July 2019.

*Sponsorship*

*The CMU HoTT Group gratefully acknowledges the support of the Air Force Office of Scientific Research through MURI grants FA9550-15-1-0053** and FA9550-21-1-0009, as well as award number FA9550-20-1-0305**. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the United States Air Force.*