Homepage of Jonas Frey
I am a postdoc in the Homotopoy 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
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.
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.
Publications
Triposes, q-toposes and toposes, Annals of Pure and Applied Logic 166.2 (2015): 232-259.
Realizability toposes from specifications, Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015: 196-210.
Classical realizability in the CPS target language, Electronic Notes in Theoretical Computer Science 325 (2016): 111-126.
Ordered combinatory algebras and realizability (with Walter Ferrer Santos, Mauricio Guillermo, Octavio Malherbe and Alexandre Miquel), Mathematical Structures in Computer Science 27.3 (2017): 428-458.
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. ACM, 2018, Lean code
Characterizing partitioned assemblies and realizability toposes, Journal of Pure and Applied Algebra 223.5 (2019): 2000-2014.
Triposes as a generalization of localic geometric morphisms (with Thomas Streicher), Mathematical Structures in Computer Science, 2021
Categories of partial equivalence relations as localizations, Journal of Pure and Applied Algebra, 2022
Constructing Coproducts in locally Cartesian closed ∞-Categories (with Nima Rasekh), accepted in Homotopy, Homology and Applications
Notes, Preprints
Duality for Clans: a Refinement of Gabriel-Ulmer Duality (2023)
A 2-categorical analysis of the tripos-to-topos construction. A complete rewrite of this, which is much shorter, 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