Tom de Jong

@de-jong-tom.mathstodon.xyz.ap.brid.gy

Postdoc at Radboud University, previously at University of Nottingham, working on type theory. PhD from University of Birmingham. Mathematician, computer […]

🌉 bridged from ⁂ https://mathstodon.xyz/@de_Jong_Tom, follow @ap.brid.gy to interact

@de-jong-tom.mathstodon.xyz.ap.brid.gy Oct 5, 2026, 6:01 AM

[1] André Joyal. Notes on clans and tribes. arXiv:1710.10238, 2017. [2] Michael Shulman. All (∞,1)-toposes have strict univalent universes. arXiv:1904.07004, 2019. [3] Benno van den Berg and Ieke Moerdijk. Exact completion of path categories and algebraic set theory: Part I: Exact completion of […]

@de-jong-tom.mathstodon.xyz.ap.brid.gy Oct 5, 2026, 6:01 AM

We propose a new approach to the semantics of identity types in intensional Martin-Löf type theory. The setting is quite general, assuming only a category with finite limits and an exponentiable interval. It therefore applies to many different cases such as clans [1], model categories [2], path […]

@de-jong-tom.mathstodon.xyz.ap.brid.gy Oct 5, 2026, 6:00 AM

This week the #HoTTEST seminar presents:

Steve Awodey

Path types in Algebraic Type Theory

The talk is at 11:30am EST (15:30 UTC) on Thursday, October 8. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a […]

@de-jong-tom.mathstodon.xyz.ap.brid.gy Oct 1, 2026, 2:48 PM

During those 8 years I maintained strong ties to the Netherlands, largely because my partner continued to live there. As a result, I've long felt that I was living two lives. This was rich and fun, but also (increasingly) exhausting. I feel very fortunate that I was able to "go home" while […]

@de-jong-tom.mathstodon.xyz.ap.brid.gy Oct 1, 2026, 2:47 PM

Eight years ago, I moved to the UK to do a PhD within the Theory (Computer Science) group of the University of Birmingham, supervised by @MartinEscardo and co-supervised by Benedikt Ahrens. After my PhD, I moved to Nottingham's Functional Programming (FP) Lab to work with @Nicolai_Kraus. I […]

@de-jong-tom.mathstodon.xyz.ap.brid.gy Oct 1, 2026, 2:47 PM

I've started my new job! As of today, I'm a postdoc in the Software Science group of the Institute of Computing and Information Sciences at Radboud University in the Netherlands. This position is (largely) funded by a personal 3-year Veni fellowship from the Dutch research organization NWO. I'm […]

@de-jong-tom.mathstodon.xyz.ap.brid.gy Sep 19, 2026, 7:21 AM

The slides for my course in homotopy type theory / univalent foundations at the Proof and Computation autumn school are available at:
https://tdejong.com/talks/PC-2026-1.pdf
https://tdejong.com/talks/PC-2026-2.pdf
https://tdejong.com/talks/PC-2026-3.pdf

As always it was a great pleasure to be a […]

@de-jong-tom.mathstodon.xyz.ap.brid.gy Sep 18, 2026, 12:12 PM

[LLMs]

I'm not big on legalese but nevertheless I found this court document [1, found via [2]], and the quotes from people in the tech industry, quite interesting.

Example: "Microsoft has observed that “threaten[ing] the economic foundations of its essential […]

[Original post on mathstodon.xyz]

May contain graphic violence

@de-jong-tom.mathstodon.xyz.ap.brid.gy Sep 9, 2026, 3:01 PM

RE: https://mathstodon.xyz/@de_Jong_Tom/115932662984124108

And now this paper with @MartinEscardo on injective types is published in the Annals of Pure and Applied Logic 🙂️ https://doi.org/10.1016/j.apal.2026.103829

@de-jong-tom.mathstodon.xyz.ap.brid.gy Aug 13, 2026, 9:09 AM

Who came up with the "type check" vs "vibe check" joke? The students in my HoTT course liked it, and I also like it a lot (and it's actually useful in some explanations). But I would like to remember who came up with it, so that I can give them credit in the future.

@de-jong-tom.mathstodon.xyz.ap.brid.gy Aug 9, 2026, 4:23 PM

Made to Prague for #ESSLLI! The hotel room TV remote is interesting 😄

A remote with a lambda on the bottom left.

@de-jong-tom.mathstodon.xyz.ap.brid.gy Aug 3, 2026, 2:50 PM

Just learnt that our paper "A study of Kock's fat Delta" (https://arxiv.org/abs/2503.10963) with Nicolai Kraus (@Nicolai_Kraus), Simona Paoli and Stiéphen Pradal (@Stiephen) was accepted for publication in the Journal of Pure and Applied Algebra (JPAA).

I'm quite happy about this, but I'm […]

mathstodon.xyzOriginal post on mathstodon.xyz

@de-jong-tom.mathstodon.xyz.ap.brid.gy Jul 23, 2026, 6:27 AM

One of the joys of using #Typesetter (a minimal editor for #typst) is that I find it improves after each update which is not usually the case for many other pieces of software 🥲️

@de-jong-tom.mathstodon.xyz.ap.brid.gy Jul 14, 2026, 6:46 PM

@jeanas You can't (I think).

@de-jong-tom.mathstodon.xyz.ap.brid.gy Jul 10, 2026, 2:53 PM

The teaching materials (first version) for my course "Introduction on Homotopy Type Theory / Univalent Foundations" at ESSLLI 2026 are now available at https://github.com/tomdjong/ESSLLI-2026/

I really enjoyed putting this together and naturally I (re)learnt a thing or two myself in the […]

mathstodon.xyzOriginal post on mathstodon.xyz

@de-jong-tom.mathstodon.xyz.ap.brid.gy Jun 22, 2026, 8:50 AM

This week I'm very much looking forward to the "Formal proof and synthetic mathematics" workshop co-organized by @matematiflo! https://matematiflo.github.io/ProofWorkshop2026/

Can't say the same about the weather forecast...

@de-jong-tom.mathstodon.xyz.ap.brid.gy Jun 4, 2026, 6:50 AM

The 37th European Summer School in Logic, Language and Information (ESSLLI), taking place from August 3rd to August 14th, 2026 at the Faculty of Civil Engineering, Czech Technical University, Prague, Czechia.
https://2026.esslli.eu/

= Overview =
The European Summer School in Logic, Language and […]

mathstodon.xyzOriginal post on mathstodon.xyz

@de-jong-tom.mathstodon.xyz.ap.brid.gy Jun 4, 2026, 6:44 AM

RE: https://mathstodon.xyz/@de_Jong_Tom/116435680670519184

The early-bird registration deadline for the European Summer School in Logic, Language and Information (ESSLLI) has been extended to 15 June.
https://2026.esslli.eu/registration/registration.html

[More details in the reply to this post.]

Tom de Jong@de-jong-tom.mathstodon.xyz.ap.brid.gyApr 20, 2026, 6:44 AM

The 37th European Summer School in Logic, Language and Information (ESSLLI 2026) will take place on 3-14 August in Prague. https://2026.esslli.eu I'm excited that I'll be teaching an introductory course on univalent foundations / homotopy type theory! @stringdiagram and @jaklt will also be […]

mathstodon.xyzOriginal post on mathstodon.xyz

@de-jong-tom.mathstodon.xyz.ap.brid.gy Jun 3, 2026, 1:43 PM

Does anybody know how to typeset pullback/pushout corners in typst/fletcher?
The code provided at https://github.com/Jollywatt/typst-fletcher/issues/50#issuecomment-2851846670 does not quite work for me and even when it does, it requires experimenting with degrees which is bad.

#typst […]

mathstodon.xyzOriginal post on mathstodon.xyz

@de-jong-tom.mathstodon.xyz.ap.brid.gy Jun 1, 2026, 3:41 PM

RE: https://mathstodon.xyz/@iblech/116675413147766207

I didn't know of this collection of notes by (the late) Thomas Streicher. Thanks for sharing them!
https://www2.mathematik.tu-darmstadt.de/~streicher/mixed.pdf

mathstodon.xyz

Older posts