Anders Mörtberg

Associate professor (docent) in computational mathematics at Stockholm University.

I'm interested in HoTT/UF, cubical stuff, constructive mathematics, logic and type theory, category theoretical foundations, functional programming, computer formalization of mathematics and computer science, and much more.

Webpage: https://staff.math.su.se/anders.mortberg/

Last Notes

2026-01-26 10:00:01 GMT

- reply

@nprofile…xuzd I hate this "feature" as well. I recently had to add some random underscores is various filenames to avoid some confusing hyperlinks... I believe we will switch to Canvas next year, but I don't know if that is any better...

2025-11-25 10:30:49 GMT

- reply

@nprofile…w8t5 @nprofile…rrqe I have no clue, it was a long time ago... I seem to recall that he was heavily using align-regexp to make definitions look nicer at least

2025-11-25 10:25:51 GMT

- reply

@nprofile…w8t5 @nprofile…rrqe I learned Agda in 2008/2009 in some lectures with Ulf Norell at Chalmers. He was heavily using some emacs macros that automatically refactored the code in addition to all the Agda interaction features, making me very confused and amazed 😃

2025-11-25 10:22:16 GMT

- reply

@nprofile…w8t5 @nprofile…rrqe I think some really good video lectures showing how to interact with Agda would be very helpful for newcomers (with some type of subtitles showing what keys are being pressed)... Maybe this already exists?

2025-11-10 21:35:11 GMT

- reply

@nprofile…rrqe @nprofile…w8t5 I read somewhere recently that the space of people getting a Fields medal for the work in their PhD is contractible (with JP Serre being the center of contraction). Not sure if this is true, but Serre's PhD work was of course very influential (and published in the Annals...)

2025-10-29 21:02:05 GMT

- reply

@nprofile…dand @nprofile…ujwf One idea was that II should be a formal analogue to the real interval [0,1] which forms a De Morgan algebra, not a Boolean algebra. I discussed this in some more detail on page 7 and remark 9 in https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/cubical-methods-in-homotopy-type-theory-and-univalent-foundations/ECB3FE6B4A0B19AED2D3A2D785C38AF9

2025-10-29 08:16:57 GMT

- reply

@nprofile…43uy @nprofile…w8t5 @nprofile…7mkg Peter Lumsdaine also gave a nice talk about setoids and univalent categories at the Palmgren memorial conference in 2020: https://logic.math.su.se/palmgren-memorial/slides/Lumsdaine-slides-Palmgren-memorial-conference.pdf

2025-10-06 07:26:50 GMT

- reply

@nprofile…6kk0 Yikes! Protip: always make sure you have at least one day without any meetings each week. Don't tell my colleagues, but my strategy is to fix a weekly research day for the semester and whenever someone tries to book something on that day I say that I'm too busy :-) Next level (that I haven't yet managed to achieve) is to have one completely empty week per semester to focus exclusively on research...

2025-03-19 09:19:07 GMT

We are hiring PhD students in Computational Mathematics and Mathematics at Stockholm University:
https://su.varbi.com/what:job/jobID:807359/where:4/
https://su.varbi.com/what:job/jobID:803014/where:4/
**Application deadline: April 22**
Please help spread the word to students who are interested in doing a PhD on type theory, HoTT, computer formalization of CS and math, constructive mathematics, etc. Note that PhD students here are employed with a salary and that the position comes with benefits. There are also no tuition fees.
If you are a student interested in doing a PhD with me you are welcome to apply to both positions above, just make sure you apply to the one in Computational Mathematics as that is the division I formally belong to. Please also specify clearly that you want me as an advisor in your application (e.g. in your cover letter).
Please don't hesitate to contact me on [email protected] if you have any questions.

2025-02-23 10:57:54 GMT

We are hiring an Assistant Professor in Mathematics with focus on Mathematical Logic in the Department of Mathematics at Stockholm University. The position is tenure track and the candidate will be part of the long standing tradition of logic research in Stockholm. Applicants from all areas of logic and related areas are very welcome to apply. Women and other underrepresented groups are strongly encouraged to apply.
Application deadline: April 15, 2025, 11:59 PM CEST
The Logic group in Stockholm currently consists of professor emeritus Per Martin-Löf and associate professors Peter LeFanu Lumsdaine and Anders Mörtberg with PhD students and postdocs. The Department is a vibrant place for logic research with a weekly seminar (https://logic.math.su.se/seminar/), advanced courses in logic, and close collaborations with other research groups in Sweden and internationally.
More information about the position and how to apply: https://su.varbi.com/en/what:job/jobID:796743/where:4/
Feel free to contact Anders Mörtberg ([email protected]) and Peter LeFanu Lumsdaine ([email protected]) if you have any questions about the position.