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

2025-11-25 10:30:49 UTC

- 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 UTC

- 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 UTC

- 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 UTC

- 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 UTC

- 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 UTC

- 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-02-23 10:57:54 UTC

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 (anders.mortberg@math.su.se) and Peter LeFanu Lumsdaine (p.l.lumsdaine@math.su.se) if you have any questions about the position.