nLab Fredrik Forsberg

• webpage

Selected writings

On quotient types and higher inductive types:

• Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, Fredrik Forsberg, Quotient inductive-inductive types, Foundations of Software Science and Computation Structures (FoSSaCS 2018), Lecture Notes in Computer Science 10803 (2018) [doi:10.1007/978-3-319-89366-2_16, arXiv:1612.02346]

On ordinals in dependent type theory and marked extensional well-founded orders:

• Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu, Set-Theoretic and Type-Theoretic Ordinals Coincide [arXiv:2301.10696]

On ordinal exponentiation in dependent type theory, see:

• Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu, Ordinal Exponentiation in Homotopy Type Theory (arXiv:2501.14542)

Related entries

• inductive-inductive type

category: people