## Jonathan Weinberger

Dr Jonathan Weinberger (he/him/his)

Assistant professor in computer science @ Fowler School of Engineering, Chapman University

Address:

Fowler School of Engineering

Chapman University

1 University Dr

Orange, CA 92866

Email: jweinberger at chapman dot edu

Office hours: Tuesdays 3--5 PM & Thursdays 2:15--4:15 PM (Swenson Hall, 3rd floor, huddle spaces)

Google scholar, ORCID, Academia.edu, ResearchGate, nLab, GitHub, Math Genealogy

Current and recent events:

Formalization project on synthetic ∞-category theory: Contributions by Fredrik Bakke, Nikolai Kudasov, Emily Riehl and myself to a formalization of the ∞-categorical Yoneda lemma in Nikolai Kudasov's new Rzk proof assistant. See also sHoTT.

Check out the Women in Logic network and event series

Education:

Dr. rer. nat in Mathematics, advised by Prof. Dr. Thomas Streicher at Logic group, Dept. of Mathematics, TU Darmstadt, Germany

Dissertation A Synthetic Perspective on (∞ ,1)-Category Theory: Fibrational and Semantic Aspects, defended on Dec 9, 2021

MSc. Mathematics (Specialization: Category Theory, Categorical Logic, Algebraic Homotopy Theory, Synthetic Differential Geometry; Minor: Computer Science), TU Darmstadt, partial coursework at GU Frankfurt, Germany, 2016

BSc. Mathematics (Minor: Philosophy), TU Darmstadt, Germany , 2014

Academic employment:

since August 2024: Assistant professor in computer science at the Fowler School of Engineering, Chapman University, Orange, CA, USA

July 2022–August 2024: Postdoctoral fellow at the Dept. of Mathematics, Johns Hopkins University, Baltimore, MD, USA

Advisor: Prof. Emily Riehl, PhDMar–May 2022: Postdoctoral fellow at Max Planck Institute for Mathematics, Bonn, Germany

Advisor: Dr. Viktoriya OzornovaOct 2021–Feb 2022: Postdoctoral Researcher at Theory of Computation Group, School of Computer Science, University of Birmingham, UK.

Advisor: Dr. Benedikt AhrensOct 2016–Sep 2021: Doctoral student and teaching assistant at Logic group, Dept. of Mathematics, TU Darmstadt, Germany. This also included teaching duties, cf. below.

Advisor: Prof. Dr. Thomas Streicher

## Research interests

(Higher) category theory

(Homotopy) type theory

Connections between logic and homotopy theory

Proof assistants and formalization of mathematics

Theory of programming languages

Foundations of AI & machine learning

## Publications

M. Anel, J. Weinberger (2024): Smooth and proper maps with respect to a fibration. arXiv:2402.00331, pp 1–12. Accepted for publication in Mathematical Structures in Computer Science (Special Edition on Homotopy Type Theory)

J. Weinberger (2024): Two-sided cartesian fibrations of synthetic (∞, 1)-categories. arXiv:2204.00938, doi:10.1007/s40062-024-00348-3, Journal of Homotopy and Related Structures 19(2)

M. Capucci, B. Gavranović, A. Malik, F. Rios, J. Weinberger (2024): On a fibrational construction for optics, lenses, and Dialectica categories. arXiv:2403.16388. pp 1–18. Accepted at the 40th Conference on Mathematical Foundations of Programming Semantics (MFPS) 2024

J. Weinberger (2024): Internal sums for synthetic fibered (∞,1)-categories. arXiv:2205.00386, doi:10.1016/j.jpaa.2024.107659, Journal of Pure and Applied Algebra, vol 228, issue 9, 107659, pp 1–52, 2024

N. Kudasov, E. Riehl, J. Weinberger (2024): Formalizing the ∞-Categorical Yoneda Lemma. In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024). Association for Computing Machinery, New York, NY, USA, 274–290. arXiv:2309.08340, doi:10.1145/3636501.3636945

U. Buchholtz, J. Weinberger (2023): Synthetic fibered (∞,1)-category theory. arXiv:2105.01724, doi:0.21136/HS.2023.04, Higher Structures 7(1): 74–165, 2023

T. Streicher, J. Weinberger (2021): Simplicial sets inside cubical sets. arXiv:1911.09594, Theory and Applications of Categories, Vol. 37, 2021, No. 10, pp 276–286.

## Preprints

D. Trotta, J. Weinberger, V. de Paiva (2024): Skolem, Gödel, and Hilbert fibrations. arXiv:2407.15765. pp 1–35. Submitted

D. Gratzer, J. Weinberger, U. Buchholtz (2024): Directed univalence in simplicial homotopy type theory. arXiv:2407.09146. pp 1–28. Submitted

J. Weinberger (2024): Generalized Chevalley conditions in simplicial homotopy type theory. arXiv:2403.08190. pp 1–19. Submitted

J. Weinberger (2022): Strict stability of extension types. arXiv:2203.07194, pp 1–16. Submitted

## PhD thesis

A Synthetic Perspective on (∞,1)-Category Theory: Fibrational and Semantic Aspects. tuprints, dnb, summary, arXiv:2202.13132, xxi+177 pp

Slides from defense (Dec 9, 2021): pdf

## Reviews

Philip Hackney and Martina Rovelli: Induced model structures for higher categories, Zbl 7594302, PDF (zbMATH)

Evan Cavallo and Robert Harper: Internal parametricity for cubical type theory, Zbl 07471665, PDF (zbMATH)

Valery Isaev: Model structures on categories of models of type theories, Zbl 06965096, PDF (zbMATH)

## Research talks

Directed univalence in simplicial homotopy type theory (Seminar of trimester program "Prospects of Formal Mathematics," Hausdorff Institute for Mathematics, Bonn, July 24)

Formalization of ∞-category theory (Logic and Semantics Seminar, Aarhus University, Aarhus, June 24)

The dependent Gödel fibration (ItaCa Fest 2024, June 24, video)

Formalization of ∞-category theory (OCIE/MPP Seminar, Chapman University, Orange, CA, Mary 24, video)

Synthetic Foundations & Formalization of ∞-Category Theory (Topology Seminar, University of Virginia, Charlottesville, VA)

Formalizing the ∞-categorical Yoneda lemma (CPP 2024, IET, London, UK, Jan 24, video)

Formalizing the ∞-categorical Yoneda lemma (BUGCAT, Binghamton University, NY, Nov 23)

Formalizing the ∞-categorical Yoneda lemma (Slides, abstract) (Abstract Homotopy Theory Seminar, Max Planck Institute for Mathematics, Bonn, Germany, Aug 23)

Formalizing the ∞-categorical Yoneda lemma (Topology Seminar, NTNU, Trondheim, Norway, Aug 23, invited)

The dependent Gödel fibration (CT 23, UCLouvain, Louvain-la-Neuve, Jul 23)

Internal sums for synthetic fibered (∞,1)-categories (Homotopy Type Theory 2023, Carnegie Mellon University, Pittsburgh, PA, May 23)

Synthetic fibered (∞,1)-category theory (San Diego Category Theory and Type Theory Seminar, University of San Diego, San Diego, CA, Feb 23, video, invited)

Generalized Dialectica constructions via Skolemization (HoTT Seminar, Carnegie Mellon University, Pittsburgh, PA, Nov 22)

Dialectica constructions and lenses (Doktorandentreff AG Logik, TU Darmstadt, Germany, Oct 22)

Dialectica constructions and lenses (Berkeley Seminar, Topos Institute, California, CA, Sep 22, video)

A type theory for (∞,1)-categories (Berkeley Seminar, Topos Institute, California, CA, Sep 22, video)

Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability (HoTT/UF 2022, Haifa/Internet, Jul 22, video)

Synthetic (∞,1)-category theory in simplicial homotopy type theory (Uni Regensburg, SFB Higher Invariants Seminar, Jul 22, invited)

Synthetic Tait Computability for Simplicial Type Theory (TYPES 2022, Nantes/Internet, June 22, video)

Simplicial homotopy type theory (MSRI HC Pt 2, Cuernavaca, Morelos, Mexico, June 22)

Synthetic fibered (∞,1)-category theory (JMRA, March 22, video)

Synthetic fibered (∞,1)-category theory (Logic and higher structures, CIRM, Marseille, Feb 22, video)

Synthetic fibered (∞,1)-category theory (HoTTEST Event for Junior Researchers 2022, Western University, London, ON, online, Jan 22, video)

Synthetic fibered (∞,1)-category theory (Topology Seminar, EPFL, Lausanne, Nov 21, invited)

Synthetic fibered (∞,1)-category theory (Theoretical Computer Science Seminar, University of Birmingham, online, Nov 21)

Internal sums for synthetic fibered (∞, 1)-categories (CaTCat: Open House on Category Theory 2021, celebrating F. Marmolejos 60th Birthday. Ciudad de México, online, Nov 21)

Synthetic fibered (∞,1)-category theory (Novemberfest 2021, uOttawa, online, Nov 21) (video)

A Yoneda Lemma for synthetic fibered ∞‑categories (CMU HoTT Graduate Student Workshop 2021, Carnegie Mellon University, online, Feb 21, invited)

A Yoneda Lemma for synthetic fibered ∞-categories (Doktorandentreff AG Logik, TU Darmstadt, online, Dec 20)

A synthetic language for fibered higher categories (Doktorandentreff AG Logik, TU Darmstadt, online, Nov 20)

Cocartesian Fibrations in Simplicial Type Theory (correction Feb 19, 21) (Pittsburgh's HoTT Seminar, online, Sep 20)

Modalities and Fibrations for Synthetic (∞,1)-Categories (New York City Category Theory Seminar, The Graduate Center of The City University of New York, New York, NY, Oct 19, invited) (video)

Modalities and Fibrations for Synthetic (∞,1)-Categories (HoTT Seminar, Carnegie Mellon University, Pittsburgh, PA, Oct 19)

Modalities and Fibrations for Synthetic (∞,1)-Categories (Category Theory Seminar, Johns Hopkins University, Baltimore, MD, Sep 19, invited)

Type-theoretic Modalities for Synthetic (∞,1)-Categories (Homotopy Type Theory 2019, Pittsburgh, PA, Aug 19)

Type-theoretic Modalities for Synthetic (∞,1)-Categories (TYPES 2019, Oslo, Jun 19)

Fibrations, Modalities, and Universes for Synthetic (∞,1)-Categories (CAS, Oslo, Jun 19)

Universes in a Type Theory for Synthetic ∞-Category Theory (CAS, Oslo, Dec 18)

Universes in a Type Theory for Synthetic ∞-Category Theory (EUTYPES 2018, Aarhus, Oct 18)

Simplicial Sets inside Cubical Sets (PSSL, Amsterdam, Oct 18)

(Truncated) Simplicial Models of Type Theory (Workshop on HoTT/UF, FLoC, Oxford, Jul 18)

Fibrations in Type Theory with Shapes (PSSL, Santiago de Compostela, Jan 18)

Interpreting Cubical Type Theory in Appropriate Presheaf Toposes (Working group "Logique de la Programmation", Aix-Marseille Université, Luminy, Sep 17)

Interpreting Cubical Type Theory in Appropriate Presheaf Toposes (PSSL, Leeds, Sep 17)

Interpreting Cubical Type Theory in Appropriate Presheaf Toposes (Workshop on HoTT/UF, FSCD, Oxford, Sep 17)

## Expository talks

Topological Hochschild Homology et al (Prismatic Cohomology Seminar, Johns Hopkins University, Baltimore, MD, Spring 23)

Invertible TFTs and bordism spectra (TQFT Reading Group, Johns Hopkins University, Baltimore, MD, Spring 23)

Goodwillie calculus and the n-excisive modality in an ∞-topos (Goodwillie Calculus Reading Group, Johns Hopkins University, Baltimore, MD, Fall 22)

Homotopy type theory and synthetic homotopy theory (Intro to HoTT mini-series, Topology Seminar, MPIM Bonn, March 22)

Lurie's Adjoint Functor Theorem for (∞,1)-Categories (Mini-workshop ∞-Categories, Darmstadt, Feb 19)

What is...a Higher Category? (What is...? Seminar, Darmstadt, Nov 18) (expository)

Proof of Model-Independence of ∞-Category Theory in an ∞-Cosmos (MIT Talbot 2018: Model-Independent Theory of ∞-Categories, Government Camp, OR, May 18)

## Research program memberships

AMS Math Research Community on Applied Category Theory (22-23)

SLMath (ex-MSRI) Program Higher Categories and Categorification Pt. 2 (June 22)

## Research visits

Aarhus University, Logic and Semantics group (Aarhus, Denmark, 1 week, June 2024)

Carnegie Mellon University HoTT group (Pittsburgh, PA, 2 weeks, Nov–Dec 22)

Department of Mathematics, University of Pennsylvania (Philadelphia, PA, 1 week, Oct 22)

AMS MRC Applied Category Theory Collaboration Travel (Quinlan Community Center, Cupertino, CA, 1 week, Sep 22)

SFB 1085 Higher Invariants (University of Regensburg, 1 week, Jul 22)

AMS MRC on Applied Category Theory (Java Center, NY, 1 week, May 22)

Categorical Logic group, Carnegie Mellon University (Pittsburgh, PA, 1 week, Sep 19)

Category Theory group, Johns Hopkins University (Baltimore, MD, 1 week, Sep 19)

## Teaching experience

Assistant professor at Chapman University

### Fall 24

### Instructor at Johns Hopkin University

### Spring 24

### Fall 23

### Spring 23

### Fall 22

### Teaching assistant and organizer at TU Darmstadt

### Summer term 21

Logic for Computer Science II: Propositional and Predicate Logic (Prof Dr. Martin Otto, TA with Ulrik Buchholtz, PhD)

### Winter term 20/21

Mathematics I for Computer Science and Business Informatics (Prof. Dr. Thomas Streicher, TA with Ulrik Buchholtz, PhD, and Miriam Buck, MSc.)

Logic for Computer Science I: Automata, Formal Languages, and Decidability (Prof Dr. Martin Otto, TA with Ulrik Buchholtz, PhD)

### Summer term 20

### Winter term 19/20

### Summer term 19

### Winter term 18/19

### Summer term 18

### Winter term 17/18

### Summer term 17

Categorical Logic (Prof. Dr. Thomas Streicher) (3rd year+ course)

Topology (Dr. René Bartsch) (3rd year+ course)

### Winter term 16/17

Category Theory (Prof. Dr. Thomas Streicher) (3rd year+ course)

Introduction to Mathematical Logic (Prof. Dr. Martin Otto, TA with Julian Bitterlich, MSc.) (3rd year+ course)

### Student tutor for problem sessions at TU Darmstadt

### Summer term 12

### Winter term 11/12

Manifolds (3rd year+ course) (Prof. Dr. Karsten Große-Brauckmann)

Algebra (3rd year+ course) (Rings, fields, and Galois theory) (Prof. Dr. Jan-Hendrik Bruinier)

### Summer term 11

## Workshops organized

## Conference & workshop visits

Topos Institute / Chapman University Workshop (Chapman University, CA, May 24)

Certified Proofs and Programs (CPP) 2024 (IET, London, UK, Jan 24)

International Conference on Category Theory 2023 (UCLouvaine, Louvain-la-Neuve, Jul 23)

School and Workshop on Univalent Mathematics (Birmingham, Dec 17)

Categories in Homotopy Theory and Rewriting (Luminy, Sep 17)

Young Researchers in Homotopy Theory and Categorical Structures (Bonn, Feb 17)

Étale and Motivic Homotopy Theory - Prep. lecture series (Heidelberg, Mar 14)

What Can Category Theory Do For Philosophy? (Kent, UK, Jul 13)

Discrete, Tropical, and Algebraic Geometry (Frankfurt, May 11)