Homepage of Jonas Frey
I am special faculty in the Homotopy Type Theory research group at Carnegie Mellon University in Pittsburgh.
Below you can find my publications and preprints, and some slides and recordings of talks. Please let me know if you find dead or incorrect links.
News
From June 10 to 14, 2024, I will be co-teaching a course on Categorical Semantics and Synthetic Topology with Reid Barton at the Summer School in Logic and Formal Epistemology at Carnegie Mellon University. Interested students are invited to apply before February 14.
I was on the local committee of the Homotopy Type Theory 2023 conference, which took place at Carnegie Mellon University in Pittsburgh between May 22 and May 25, 2023.
I was invited speaker at the Workshop on Doctrines & Fibrations which took place at the Department of Mathematics “Tullio Levi-Civita” in Padova from May 29 to June 1, 2023.
Publications
Preprint: Uniform Preorders and Partial Combinatory Algebras (2024)
Preprint: Duality for Clans: an Extension of Gabriel-Ulmer Duality (2023)
Constructing Coproducts in locally Cartesian closed ∞-Categories (with Nima Rasekh), Homotopy, Homology and Applications (2023)
Categories of partial equivalence relations as localizations, Journal of Pure and Applied Algebra (2023)
Triposes as a generalization of localic geometric morphisms (with Thomas Streicher), Mathematical Structures in Computer Science (2021)
Characterizing partitioned assemblies and realizability toposes, Journal of Pure and Applied Algebra (2019)
Impredicative Encodings of (Higher) Inductive Types (with Steve Awodey and Sam Speight), Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (2018), Lean code
Ordered combinatory algebras and realizability (with Walter Ferrer Santos, Mauricio Guillermo, Octavio Malherbe and Alexandre Miquel), Mathematical Structures in Computer Science (2017)
Classical realizability in the CPS target language, Electronic Notes in Theoretical Computer Science (2016)
Realizability toposes from specifications, Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (2015)
Triposes, q-toposes and toposes, Annals of Pure and Applied Logic (2015)
Unpublished Notes
A 2-categorical analysis of the tripos-to-topos construction. A complete rewrite of this, which is much shorter, and unfortunately doesn't contain any string diagrams, was published under the title "Triposes, q-toposes, and toposes", see above.
Toposes for Time Complexity Classes (with Jakob Grue Simonsen, presented at DICE 2016)
Confluence and strong normalization for the CPS target language (presented at HOR 2016)
Notes on 2-categorical limits (notes of a seminar talk in February 2010 at Paris 7 University)
Computability and Krivine realizability (based on a conversation with J.-L. Krivine in November 2015)
Some Slides and Videos
Partial equivalence relations, localizations, and equipments, Workshop on Doctrines and Fibrations, May 2023, Padova, Italy, Video
Basic Combinatory Objects, Uniform Preorders and Partial Combinatory Algebras, Category Theory Octoberfest 2022, Video
An Introduction to Cohesive Homotopy Type Theory, HoTT special session at the ASL 2022 North American Annual Meeting
Characterizing clan-algebraic categories, Homotopy Type Theory Electronic Seminar Talks series, February 2022, Video
Coproducts in ∞-LCCCs with subobject classifier, HoTT/UF 2021, July 2021, Video Conference, Video
A refinement of Gabriel-Ulmer duality, HoTT/UF 2020, July 2020, Video Conference
A language for closed cartesian bicategories, CT 2019, July 2019, Edinburgh, Scotland
Modelling homotopy type theory in cartesian cubical sets, CT 2017, Vancouver, Canada
Classical realizability in the CPS target language, Realizability in Uruguay 2016, July 2016, Piriapolis, Uruguay
Realizability toposes as homotopy categories, Topos à l'IHES, November 2015, Bures-sur-Yvette, France
Realizability toposes from specifications, TLCA 2015, July 2015, Warsaw, Poland
Enriched triposes and enriched Pitts functors, PSSL 96, October 2014, Palermo, Italy
Characterizing realizability toposes, CT 2014, June 2014, Cambridge, England
Moens’ theorem and fibered toposes, ScotCats 9: Fibrations in Computation Workshop, June 2014, Glasgow, Scotland
A fibrational analysis of realizability toposes, Slides of my PhD defense, June 2013, Paris, France
Indexed preorders, uniform preorders, and PCAs, Réalisabilité à Chambéry #5, June 2012, Chambéry, France
Multiform preorders and partial combinatory algebras, Logic and interactions 2012, February 2012, Marseilles, France
A double categorical analysis of the tripos-to-topos construction, CT 2010, June 2010, Genoa, Italy
My PhD Thesis
A fibrational study of realizability toposes, supervised by Paul-André Melliès at Paris 7 University (now Université Paris Cité)
My Master's Thesis
A Universal Characterisation of the Tripos-to-Topos Construction, supervised by Thomas Streicher at Darmstadt University