Tom de Jong

This paper, by @IgorArrieta , @ayberkt and myself has just appeared in Mathematical Structures in Computer Science.

The patch topology in univalent foundations
Igor Arrieta, Martin Escardo and Ayberk Tosun

Stone locales together with continuous maps form a coreflective subcategory of spectral […]

On my way to Bochum to teach a course on Categorical Realizability at the European Summer School in Logic, Language and Information 😄 #esslli2025 #esslli

@joey I don't think so by recent results of @aws, see https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper40.pdf (and the slides and video linked on the TYPES 2025 website).

This short expository paper has now been published (https://doi.org/10.4230/LIPIcs.TYPES.2024.1) along with the other papers of the TYPES 2024 post-proceedings 🎉

#typetheory

Thanks to the organizers, you can now find the recording of my TYPES talk on "Examples and counter-examples of injective types in univalent mathematics" with @MartinEscardo on YouTube: https://www.youtube.com/watch?v=u8MD9iu9NHA

Slides […]

Two small wins yesterday

I have a Word template of a form that I need to complete. Using Word is not fun, especially because the template is relatively complicated, so that, as a Linux user, I'm forced to use a virtual Windows desktop.

Small win #1: I found a LaTeX template emulating the Word […]

I am happy to announce that my colleague Paul Blain Levy has won the Alonzo Church Award.

https://siglog.org/winner-of-the-2025-alonzo-church-award/

A meme featuring Bernie Sanders standing outdoors in a winter coat, speaking directly to the camera. The caption reads, “I am once again asking PhD students to make a damn website."

This is your yearly reminder that anyone who publishes CS papers should have a personal website that lists their current position, research interests, publications, and email address.

If you don't, it's basically impossible for me to invite you to a PC […]

[Original post on discuss.systems]

TYPES talk done! Time to enjoy the rest of the conference 😄 I talked about injective types in univalent mathematics which is joint work with @MartinEscardo. You can find my slides here https://tdejong.com/talks/TYPES-2025.pdf.

#TYPES2025 #typetheory #HoTT

Taking "algebraically" seriously in the definition of algebraically injective type.

In this thread, I want to discuss recent developments regarding the notion of algebraically injective type that I discussed in the following paper:

Injective types in univalent mathematics […]

On combinatorial aspects of fat Delta The category fat Delta, introduced by J. Kock, is a modification of the simplex category where the degeneracies behave weakly. The objective of this note is to provide tools for working with fat Delta. In particular, we identify three types of morphisms: degenerated, standard and vertical faces, and establish six relations between these classes. We then show that fat Delta is generated by these morphisms and relations.

Happy to see the second paper of our PhD student @Stiephen Pradal on the arXiv today! 😄
https://arxiv.org/abs/2506.01717

He continues the study of the fat Delta category — a modification of the simplex category introduced by Joachim Kock — and gives a presentation by generators and relations.

🚨 #ESSLLI2025 - Last chance for early bird registration (May 31)!
👉 Logic
👉 Language
👉 Information
Really interesting courses and the Ruhr area is much more interesting than it is known for! ✨
#nlproc #logic #linguistics #summerschool
https://2025.esslli.eu/registration.html

On the first of several trains to CIRM for this nice workshop on semantics of programming languages 😄 https://conferences.cirm-math.fr/3518.html

Short summaries of (1) and (2):

(1) We describe how two-level type theory can be used to represent a type theory by turning structural extensions into axiomatic extensions, using Riehl and Shulman’s simplicial type theory as an example. This talk explains the motivation behind work in progress […]

The abstracts for TYPES 2025 are now available at
https://msp.cis.strath.ac.uk/types2025/accepted.html 🎉

I'm involved in two abstracts:

(1) "Representing type theories in two-level type theory" with @Nicolai_Kraus (https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper42.pdf);

(2) […]

✨European Summer School for Logic, Language and Information 2025✨ in Bochum, Germany:
- 47 courses & workshops
- 4 exciting evening lectures
- social events
- explore the Ruhr area
Early bird registration deadline: May 31!
#esslli2025 #esslli #logic #linguistics #compSci #nlproc #summerSchool […]

If you're interested in learning how proof assistants and proof checkers work, and what their underlying formalisms are, consider applying to the International School on Logical Frameworks and Proof Systems Interoperability, which will take place on 8–11 September 2025 in Orsay. France. There […]

Euclidean interval objects in categories with finite products Based on the intuitive notion of convexity, we formulate a universal property defining interval objects in a category with finite products. Interval objects are structures corresponding to closed intervals of the real line, but their definition does not assume a pre-existing notion of real number. The universal property characterises such structures up to isomorphism, supports the definition of functions between intervals, and provides a means of verifying identities between functions. In the category of sets, the universal property characterises closed intervals of real numbers with nonempty interior. In the the category of topological spaces, we obtain intervals with the Euclidean topology. We also prove that every elementary topos with natural numbers object contains an interval object; furthermore, we characterise interval objects as intervals of real numbers in the Cauchy completion of the rational numbers within the Dedekind reals.

To close the thread, here is the arXiv version of the paper we submitted for publication yesterday:

Euclidean interval objects in categories with finite products.
http://arxiv.org/abs/2504.21551

12/12

The recordings and slides of the contributed and invited talks from the Workshop on Homotopy Type Theory/Univalent Foundations (HoTT/UF) are all up at https://hott-uf.github.io/2025/

Thanks again to all our speakers!

An approximate solution to the problem of squaring a circle. The outer square has the side 2√2. The red square is supposed to have size π.

A while ago I received a phone call from a man who lives in a small Slovenian town. He claimed to have squared the circle, finally after 10 years of efforts. He wanted to come to talk to me about it in Ljubljana. I asked that he first send me his construction […]

[Original post on mathstodon.xyz]

I've had mixed experiences with LICS and I sympathize with anyone who submitted good work but still didn't make the cut (for whatever reason).
I think allowing subreviewers to participate in the discussion was a good move by this year's PC and I hope future editions also adopt this policy […]

Here is a new reasoning principle which I have not encountered before.

Majority Decision Principle:

Given propositions p₁, p₂, p₃ and q, suppose
(1) pᵢ ⇒ ¬q ∨ ¬¬q, for i = 1, 2, 3
(2) pᵢ ⇒ ¬pⱼ, for i ≠ j
Then ¬q ∨ ¬¬q.

The principle is classically valid, but not intuitionistically provable […]

Evan Cavallo (@ecavallo@mathstodon.xyz) 241 Posts, 62 Following, 184 Followers · Postdoc at Göteborgs universitet. Types + Cubes

I'm happy to report that my expository note (https://arxiv.org/abs/2408.11501), which has previously been kindly mentioned on here by @ecavallo and @jonmsterling, has been accepted to the TYPES 2024 post-proceedings 🙂

#typetheory #formalization

@christianp Not at all, thank you for looking into it!

Search and @-resolution appear to be not working on #mathstodon. Am I the only one with this issue?

The great virtue proof assistants, more than verifying correctness, is the ability to organize mathematical knowledge so that it is recorded and can be inspected to any level of detail by just following links.

Before I used proof assistants, I recorded my thoughts in paper notebooks, like […]

The slides and recordings of the talks at the Heyting Day in celebration of Jaap van Oosten's retirement are now available here:
https://www.knaw.nl/en/heyting-day-2025

Besides the Heyting lecture by the guest of honour, we had three wonderful talks by Sebastiaan Terwijn, Andy Pitts and […]

I am very proud of our PhD student @Stiephen Pradal whose first paper appeared on the arXiv today! 🎉
https://arxiv.org/abs/2503.10963

In this paper we study the fat Delta category, a modification of the simplex category introduced by Joachim Kock. A full abstract can be found in the reply to […]

Many thanks to everyone who attended and made this an amazing day of #logic, #computabilitytheory and #categorytheory!

Recordings and slides will be available on the website sometime next week (hopefully)!

Welcome to ESSLLI 2025 ESSLLI 2025

36th European Summer School in Logic, Language and Information
https://2025.esslli.eu/

Registration is now open for students!

Boosts are appreciated.

#logic #computerscience