← Feed

Posts

• Post #3002045

  The Budapest type theory group is hiring a postdoc to work on higher observational type theory. http://lists.seas.upenn.edu/pipermail/types-announce/2026/012535.html

• Post #3002044

  I added a definition of the effective topos to Wikipedia. I think it's incomprehensible for a newcomer (as it was to me two years ago), but since I ran out of time, pedagogy will have to wait for later or someone else. https://en.wikipedia.org/wiki/Effective_topos#Definition

• Post #3002043

  Here's a question I've meant to ask for a long time: https://mathoverflow.net/q/511737/

• Post #3002042

  The setoid model translation takes a model of type theory and returns a new model which validates function extensionality and propositional extensionality for SProp. Has anyone already worked out something like this for unique choice? I guess something like replacing functions with functional relations should work, right? I'm asking because I understand unique choice to be the reason why the definition of the effective topos is so complicated and doesn't just use plain setoids (s...

• Post #3002041

  I have in my mind two conflicting definitions of “f : X → Y has the Baire property (BP)”. (X and Y are topological spaces which I'm happy to assume Polish.) The first is that the preimage of an open subset has the BP (coincides with an open modulo a meager, and open can be replaced with Borel here). The second is that f is “Baire-measurable”, i.e., measurable with respect to the σ-algebras of BP subsets: the preimage of a BP has the BP. Did I dream up that these are equivalent? It comes...

• Post #1763209

  In French mathematics, families are tied into tribes living on separated spaces.

• Post #1763208

  Breaking mathematical news: recent events have formally disproved the claim that adults are adults, refuting a nearly 350 years old conjecture of Leibniz. This is the first fully automated contribution to mathematics by autonomous geopolitical agents.

• Post #1763206

  I just created a Wikipedia page about cubical type theory. For now this is a stub with just keyword-dropping and reference-dropping. Help to augment it is very welcome, we really need a readable first introduction to cubical type theory written down somewhere. https://en.wikipedia.org/wiki/Cubical_type_theory

• Post #1763205

  I also proposed to merge “Homotopy type theory” and “Univalent foundations”. Opinions are welcome on which name to retain… https://en.wikipedia.org/wiki/Wikipedia:Articles_for_deletion/Homotopy_type_theory

• Post #1763204

  I'm taking a descriptive set theory course. I'm the only one from the type theory group (which is in the CS department), the others are master's students in the math department. In today's exercise session, one of them wrote on the board “{F ∈ ℱ(X) | F ∩ U}” and said that F ∩ U was a shorthand notation for “F intersects U”. Others started to laugh. He said that after all it makes sense because you can convert a set to a boolean through the function that maps the e...

• Post #822909

  I just signed the “No free view? No review!" pledge to refuse reviewing papers for closed-access venues, and I encourage all researchers to do the same. https://nofreeviewnoreview.org