Ulrik Buchholtz

I'm a logician/computer scientist/mathematician who likes to work on homotopical and/or foundational matters, often related to homotopy type theory. Assistant professor at the School of Computer Science at the University of Nottingham.

Last Notes

2026-01-17 17:16:31 UTC

I haven't seen this announced here: My colleague Thorsten Altenkirch launched a new podcast #aboutlogic together with cohost @nprofile…yetk – I enjoyed the first three episodes with Thorsten, Deniz, and @nprofile…pm2x, respectively. Find it in your podcast app (RSS https://aboutlogic.podigee.io/feed/mp3) or watch on YouTube (https://www.youtube.com/@aboutlogic). #logic #mathematics #philosophy #computerscience

2025-12-25 14:53:01 UTC

- reply

@nprofile…8eua “What are they called in some other language?”
In Latin they are called “duris” and “mollis”(hard and soft), which survives into German as “Dur/Moll” (and similar in Danish “dur/mol” and other related languages). @nprofile…mdgu @nprofile…sn9y

2025-12-06 14:03:41 UTC

At the School of Computer Science at the University of Nottingham, we just opened applications for a limited number of PhD studentships. They are open to students of any nationality, but non-home students must be able to cover the additional cost of international tuition fees. Please see here for details on joining us at the Functional Programming Lab: https://people.cs.nott.ac.uk/pszgmh/phd-advert.html

2025-12-03 20:07:35 UTC

- reply

@nprofile…xjm9 Yes, from the title “Type Theory using Agda” I strongly suspect that the focus will be on learning to use type theory by working in Agda. Sergey Goncharov's Category Theory course and Sean Moss' course would give prerequisites for some meta-theory of type theory, which can then be followed up by Chapters 3 and 6 of @nprofile…9t3n and @nprofile…v38n 's book draft: https://www.danielgratzer.com/papers/type-theory-book.pdf @nprofile…w8t5 @nprofile…kxks

2025-11-20 17:19:56 UTC

- reply

@nprofile…rrqe @nprofile…8pq6 using univalence a lot, even transparently as we do, forces equal conventions for both (of course having both diagrammatic works too :))

2025-11-20 17:16:22 UTC

- reply

@nprofile…rrqe @nprofile…8pq6 in the book, both paths and functions (and thus equivalences) are composed in algebraic/applicative (rather than diagrammatic/sequential) order.

2025-11-20 16:54:48 UTC

- reply

@nprofile…8pq6 @nprofile…rrqe Thanks both for catching that; I've just pushed a fix. Chapter 7 isn't quite as polished as we'd like yet. We'd like to state some of these results more neatly for reference, which is why I'm in the process of adding Chapter 6 on category theory.

2025-11-10 10:49:04 UTC

It’s not every day you get to witness one of the largest cranes in the world gently lifting a bridge in place.
https://media.mathstodon.xyz/media_attachments/files/115/524/999/125/031/422/original/4fd76297950c0af1.jpeg
https://media.mathstodon.xyz/media_attachments/files/115/524/999/220/821/123/original/09a17c0f6a276132.jpeg

2025-10-18 14:25:33 UTC

- reply

@nprofile…rrqe Scandalous situation with the lack of good whiteboards! Instead of an iPad you could consider a writing tablet. I teach with an affordable Huion H1060p that I've had since the pandemic. I like writing on it, and it has the added benefit of giving legible recordings when used with the portable executable of Xournal++ on our lecture room Windows machines. (We have to record our lectures anyway.)

2025-10-12 10:14:50 UTC

- reply

@nprofile…6kk0 Another win for playing with fibered vs indexed!

2025-05-26 18:14:28 UTC

- reply

Section 4 is a walking meditation on Engelbartian themes, from Wittgenstein and Anscombe, via Turing and Dijkstra, to recent work on embodied augmentation: https://open.substack.com/pub/fortunebuchholtz/p/high-mood-a-series-on-our-augmented-6e2

2025-05-23 19:13:42 UTC

- reply

In Section 3, Fortune talks about the Freudian psychology of working with LLMs, Extreme Programming inventor Kent Beck’s “Tidy First”, Toyota's Set-Based Concurrent Engineering (not that kind of set!), and more, still through the Engelbartian lens: https://open.substack.com/pub/fortunebuchholtz/p/high-mood-a-series-on-our-augmented-775?r=7u437&utm_medium=ios

2025-05-22 08:07:40 UTC

My better half is writing a series on her substack on how to view the current attempts at augmented coding via LLMs through the lens of Doug Engelbart's framework of tools for collective intelligence amplification. The first two installments are there; expect the next ones to touch on using Toyota manufacturing methods to facilitate testing, Dijkstra, the philosophy of language, and more. I'm of course highly skeptical of LLM-assisted coding, but many workers and students are already doing it, so thinking about doing it better is needed. First installment here: https://fortunebuchholtz.substack.com/p/high-mood-a-series-on-our-augmented

2025-04-23 07:29:45 UTC

- reply

@nprofile…6kk0 Looking forward to it! Though I may nip out after the intro to watch the Colloquium in memoriam Thomas Streicher: https://www.mathematik.tu-darmstadt.de/fb/aktuelles/news/news_details_15104.en.jsp