The Univalence Principle

Benedikt Ahrens, Delft University of Technology, The Netherlands Paige Randall North, Utrecht University, The Netherlands Michael Shulman, University of San Diego, California Dimitris Tsementzis, Princeton University, New Jersey, and Rutgers University, New Brunswick, New Jersey.

1. Introduction 2. Introduction to two-level homotopy type theory and univalent foundations 1. Theory of Diagram Structures 3. Categories: An extended example 4. Diagram signatures in Two-Level Type Theory 5. Indiscernibility and univalence for diagram structures 6. The univalence principle for diagram structures 2. Examples of Diagram Structures 7. Structured sets 8. Structured 1-categories 9. Higher categories 10. Strict categorical structures 11. Graphs and Petri nets 12. Enhanced categories and higher categories 13. Unnatural transformations and nonfunctorial operations 3. Theory of Functorial Structures 14. Functorial signatures 15. Levelwise equivalences of structures 16. Indiscernibility and univalence 17. Equivalence of structures and the univalence principle 18. Examples of functorial structures 19. Conclusion