Intuitive Type Theory

The Sokal MathsBet is a whitehat decentralized betting club run by mathematicians, which was founded twelve years ago in London. While one might expect more sensible gambling choices from the members of a maths club – anything from ferret bingo to guessing the winner of the Eurovision song contest, the swamp football world championship, or the Cooper's Hill Cheese-Rolling and Wake challenge – the Sokal MathsBet's activity concerns solely science-abuse predictions. The rules of the club are simple: every month, members should place their bets regarding a newly published book or long paper. Only members who have not yet read the work can play. The book to be discussed is chosen by the member who made the best prediction the month before. The bet concerns the positioning of the chosen work on the Sokal discourse continuum defined by the two extremes of scientific abuse catalogued in Impostures Intellectuelles: "at one end, one finds extrapolations of scientific concepts, beyond their domain of validity, that are erroneous but for subtle reasons. At the other end, one finds numerous texts that are full of scientific words but entirely devoid of meaning (Sokal & Bricmont 1997)". After the bets have been placed, to decide who won, the work must be examined. All members of the club should now read (parts of) the book. In addition, the member who made the worst previous prediction has to review and present it to their peers. Each mathematician then secretly evaluates the book, and the final score is determined by calculating the mean of the registered values. Although the club is rather heterogeneous, with members working across fields such as topology, category theory, type theory, model theory, and institution theory, the votes have always been close. It seems that everyone agrees with the computed mean score: they can all spot abuse, be it a consequence of incompetence and self-deception, or intended fraud – rather unusual for a book club. Expectedly, each member has devised their own method of evaluation. Some rely more on their intuition, developed over many years of marking exams and assignments, while others have defined minutious points systems that they follow strictly:

[12 points] "using scientific ideas totally out of context, without giving the slightest justification (note that we are not against extrapolating concepts from one field to another, but only against extrapolations made without argument)";

[12 points] "throwing around scientific jargon in front of their non-scientist readers without any regard for its relevance or even its meaning (the goal is, no doubt, to impress and, above all, to intimidate the non-scientist reader)";

[11 points] "manipulating phrases and sentences that are, in fact, meaningless"

April's bet results were however surprising. The club chose to sokalize Astrolinguistics: Design of a Linguistic System for Interstellar Communication Based on Logic published by the Dutch mathematician Alexander Ollongren in 2013. This was an unlikely, one-of-a-kind event: the members of the club have unanimously decided to break the rules and discuss a book that was both quite old and written by a mathematician (Ollongren 2013). Kavvos, one of the club founding members, first suggested the more recent Extraterrestrial Languages, a history of communications with extraterrestrial intelligence (Oberhaus 2024). He had just confiscated it in class from a giggling, distracted compsci student, and was surprised to find, hidden deep in the bibliography list, some type-theory references. However, the club quickly realized that Oberhaus's book was a too low hanging fruit and decided instead to bring to trial the work responsible for generating these peculiar logical references: Ollongren's Astrolinguistics, which no one had read or even heard of before. The book presents "a meta-language that would allow extraterrestrial recipients to decipher natural language texts via applied higher-­order logic" – Lincos 2.0, lingua cosmica based on the Calculus of Inductive Constructions (CIC). The language is essentially a second-­generation version of the first (and only other) formally defined language designed exclusively for the purpose of alien communication: Lincos, "a language for cosmic intercourse", defined by another Dutch mathematician (Freudenthal 1960). Hans Freudenthal's symbolic system, which was built up from numerals into a complex language that tried not just to capture concepts used in the physical sciences, but some abstract concepts such as love and death as well, started in fact as merely a didactic exercise showcasing how to teach mathematics while amusing your students – a skill now almost extinct among the members of our club. The truth is, no one really expected Lincos 2.0 to be sound, even if Roq was flashed before our eyes right from the abstract. We wondered if this could be considered proof that the allegations against the members of our club were in fact true. Paraphrasing Sokal and Bricmont (1997), the club has officially dismissed these accusations and labeled the recent cautiousness and unexpected result as a normal part of the sieving process: "We are sometimes accused of being arrogant scientists, but our view of maths' role is in fact rather modest. Wouldn't it be nice if Gödel's theorem did have immediate and deep implications for the study of society? Or if the axiom of choice could be used to study poetry? Or if topology had something to do with the human psyche?"

Our club's May Queen is Eric Schmid's Transcendental Mathematics (Schmid 2025). It is always difficult to predict how far a young researcher's work will land on the Sokal discourse continuum, but the prospects for "Transcendental Mathematics" seem dire, if we take into consideration the clues left this year by other members of the Fellowship of the Neorationalism. Reza Negarestani's talk Synthetic A Priori After Type Theory, which he gave at Schmid's book launch in March, and Peter Wolfendale's newest book, The Revenge of Reason, act as warnings of potential scientific concepts and terminology abuse. Their quest to align to the analytic practice by basing their discourse on rigorous mathematical concepts is failing and seems more likely to continue in the continental tradition of fashionable nonsense. Through their recent quasi-scientific reading and instrumentation of intuitionistic type theory, they gave birth to an alternate type theory – the so-called intuitive type theory, based on vibe reasoning. However, we are not yet crying out that the king is naked: sometimes, their clothes are just old, borrowed, or (cherry) picked up from the unwanted/unread pile in a charity shop; sometimes, the clothes don't quite fit, and sometimes they are full of holes. Their work is nowhere in the vicinity of Lacan on the Sokal continuum, but not that close to Badiou's Mathematics of the Transcendental either.

Badiou noted that he hoped he said "nothing imprecise in mathematics, but also nothing that is mathematically proffered" in his Theory of the Subject. Sadly, he did say a lot of such things. However, in the notes collected in Mathematics of the Transcendental, the proffered statements are true. The theorems and proofs, albeit standard, are correct (many of them borrowed from books such as Robert Goldblatt's Topos: The Categorial Analysis of Logic, and Michael Fourman and Dana Scott's Sheaves and Logic – hello, Michael!). What some mathematicians complained about was the imaginative terminology he used to express/reproduce them. He essentially rebaptised existing, already well-defined concepts with terms having a greater chance to appear in a philosophy book. For example, he wrote "the transcendental of a situation is phenomenally complete" when he meant that "the subobjects of 1 in a localic topos form a complete lattice", effectively denying any dialogue with category theorists, who although could perform the expected mental alpha-substitutions, chose rather not to do so. Nevertheless, his greatest sin was not the use of unorthodox terminology, or the rather trivial comparisons he sometimes made, but that he completely missed the main idea behind category theory, limiting it to the definition of possible universes. Upon my word, where are the functors, natural transformations, or adjunctions? Moreover, for him "objects are without any determinate interior". Why restrict your transcendentals in such a way? He should have known that he was (unnecessarily) limiting his theory to a special kind of topos – for example, the statement above on the subobjects of 1 holds for any Grothendieck topos, not just for localic ones. We stop here this trial, but we refer the curious reader to Colin McLarty's review in Notre Dame Philosophical Reviews for more details on Badiou's transcendental mathematics sins.

"You do not know anything until you know why you know it", the epigraph in Sokal's Beyond the Hoax (Sokal 2010), taken from Clovis Andersen's The Principles of Private Detection, sums well our type-theory transplantation problem at hand. Badiou thought that "philosophy must enter into logic via mathematics, and not into mathematics via logic". Although he didn't always practice what he preached, as he entered category and topos theory precisely via logic, he was right. What we require from philosophers is that they have a good understanding of the mathematics they intend to apply, and that they always explain the concepts they use in terms that can be understood by their expected philosophy readers. If they can't do that, we are left to wonder why and who are they writing for. There is nothing shameful in being ignorant of (homotopy) type theory. This is a difficult topic, even for mathematicians. What we can't tolerate is claiming to present profound judgments on such difficult topics without relying on a higher understanding than that assumed at the level of science popularization. Neither Wolfendale or Negarastani seem to possess such an understanding.

In his essay surveying transcendental logic from The Revenge of Reason, Wolfendale shows that he diligently did the required reading, citing appropriately relevant mathematical works from logic, type theory and computer science (Wolfendale 2026). 10 points to Gryffindor! This is not, however, convincing proof of his grasping. He does not get into details, sticking to wikipedia-level explanations, but makes no gross mathematical mistakes. At least until he starts writing about coalgebras and exception handling. What follows is a purely speculative research promise that would probably fit better in Negarestani's Cyclonopedia (Negarestani 2008). Starting from the obvious observation that "state transition systems can be interpreted as coalgebra" and sprinkling some perfectly sound concepts such as Heyting algebras, co-Cartesian co-closed categories, and bisimulation in his report, he concocts a co-intuitionistic freestyle soup regarding a co-intuitionistic predicate calculus used "to model something like the inheritance tree of object-oriented class hierarchies", and a dual of the Curry-Howard correspondence which would be "concerned with computation not from the perspective of languages (e.g., lambda calculus) but from the perspective of machines (e.g., Turing machines)." I'll spare you the details – there aren't many, anyway. Wolfendale's desideratum is endearing. He remains "convinced that the challenge posed by Kant's notion of transcendental logic requires that we philosophers wade into this deep mathematical sea" (Wolfendale 2026). The issue is not so much that he adventures in uncharted coalgebraic waters with a bit too much confidence, but that his plan seems suicidal, given that he openly admits that not even he is sure he can actually swim ("stray into mathematical waters somewhat outside of my depth").

If Wolfendale may pass the exam with his good intentions and references from the essential reading list, Negarestani's terribly confusing talk Synthetic A Priori After Type Theory (Negarestani 2026), in which he tries to extend Per Martin-Löf's remarks on analytic and synthetic judgements in type theory to homotopy type theory (HoTT), is a mathematical death sentence. The most relevant, well explained, and least imprecise part of his talk is the section in which he solely delivers a choppelganger of Martin-Lof's talk Analytic and Synthetic Judgements in Type Theory (Martin-Löf 1994). Do not expect, however, an effort similar to Bentzen's recent revisiting of Martin-Löf's text in which he tries to clarify and correct some of his assumptions, omissions, or conclusions (Bentzen 2024). Negarestani adds nothing of value to Martin-Löf's ideas in that section, and through numerous imprecise statements he shows that he does not fully understand the main concepts he mentions. He gives no examples and no complete and clear explanations from which a virgin listener could understand the main point of Martin-Löf's interpretation/comparison. If you haven't read Martin-Löf's text yet, it's recommended you just do that instead.

It does seem that since he published Intelligence and Spirit (Negarestani 2018), Negarestani learned the difference between a type and a term of a certain type. In his book he denotes both the type and a term of that type with the same letter alpha, thus giving rise to a cascade of misunderstandings. It is not clear if his present confusion about the existence of a type versus the existence of a term of a type stems from that unfortunate denotation. Although it is safe to say alpha exists when it is clear that it is an existential judgement, as in "from A:alpha, one may infer alpha exists” (i.e., there is a term of type alpha), by saying "so the existential punchline is that when Per Martin-Löf says that A inhabits the type alpha, from there we can infer that alpha exists", Negarestani shows confusion between "alpha exists" and "an alpha exists", which seems to persist throughout the rest of the talk when discussing the existence of an object: "He wants to say that if we have made a term for an alpha type, then obviously, if we can create an existential, a particular existential dictum for alpha, for A, this means that we are supposed to create or construct – let's say not create – construct, a witness for the existence of alpha, of the object alpha. This is revolutionary. This is the whole idea that Kant has always been talking about. That, when we say that x exists, what do we mean? Really, genuinely, what do we mean when we say x exists? In philosophy or in logic, and I know that these are not fully in correspondence, these two statements in philosophy and logic, but nevertheless, as Per Martin-Löf wants to say that yes, there is a fundamental equivalence between such statements. Because if you say x exists as a certain sort of object, you should be able to construct a witness of such object of objectivity. In other words, an existence judgment is warranted by the availability of a witness, a construction of an object of the relevant type. This ties existence to construction in a way that maps naturally onto Kant's insistence that mathematics proceeds by construction. The existential judgment is synthetic in the sense that it is evidence, it is not secured solely by meaning, it requires a construction be provided" (Negarestani 2026). First of all, this is simply mathematical constructivism – it is not pertaining only to Martin-Löf intuitionistic type theory. Secondly, we have no idea what he means with the last sentence because "meaning" was not defined (as in denotational semantics, for instance). Thirdly, no, there is no fundamental equivalence between the statements mentioned – this is something that holds/applies to intuitionistic theories. And lastly, one more time, just in case it was not clear by now: we are always certain of the existence of a type. The type exists, even if there is no term of that type (provided it is well formed, i.e. written according to the grammar of types).

Throughout his talk, Negarestani launches with ease many imprecise statements that make the reader doubt his understanding of notions such as definitional identity, model theory, and semantics. We mention just a few:

|- By saying "definitional identity is not merely a claim that two expressions denote the same thing, but rather it is an equality born out of judgment that is governed by the computational and definitional rules of the system itself", he seems to suggest that definitional identities are something we infer through combinations of rules, which is really not the case – this would apply to propositional identities.

|- When he says "Martin-Lof remarks that intuitionistically, truth is defined as the existence of a proof or construction of the proposition. This is not a mere terminological shift. It relocates the notion of truth from a semantic relation to a constructive one", there is in fact no relocation here because there is no previously defined notion of truth. And in any case, why should we oppose the semantic relation to constructivism? More questions about his understanding of model theory arise with equivocal statements such as "Lambek is quite model theoretic" or "the Lambek component is often introduced through model theoretic or semantic consideration". It is by no means clear the intended meaning (pun intended) of this statement, or what is the connection to the Curry-Howard-Lambek correspondence. Perhaps via combinatory logic, which led to Lambek's contribution to the correspondence? Most likely not.

|- Since he claims that "It is tempting to assimilate the constructivist character of type theory to Kant's distinction between phenomena and noumena...", we should remind Negarestani that not all type theories, only some, are constructivist in nature.

|- Negarestani believes that "type theory's meta theory or model theory does not play the same role. It is a semantic perspective on the system, not a metaphysical behind the scenes reality". But we should note that there is no single meta-theory or model theory for type theory. Some meta-theories can be viewed as model theories, but there's no need to discuss that here. And of course that any meta-theory gives some semantic perspective on the system – that's what meta-theories do! – and cannot be the "behind the scenes reality" – because it's a theory.

|- By stating that "categorical semantics can also be read as a disciplined theory of translation. It specifies which transformations preserve compositional structure and inferential rule, thereby providing criteria for when two presentations count as the same for the purpose of reasoning and justification", he strangely mashes up naive ideas from category theory. The first and last statements fit well together, explaining how different presentations can be 'identified' through categorical semantics, while the second one belongs to a different story altogether.

The main problem of his talk is however its inability to clearly extend Martin-Löf's idea to HoTT. The jump from the discussion of Martin-Löf's text is abrupt: Negarestani does not even say how the Curry-Howard correspondence is extended to accommodate HoTT (for the curious reader: types correspond to spaces, terms correspond to paths between spaces, type equality corresponds to homotopy equivalence between spaces). He just says that "homotopy type theory inherits this trinitarian background but also pushes it further by internalizing identity and equivalence as first class objects of reasoning". Here we should add that internalization is not specific to HoTT, but rather to the Martin-Löf type theory, through identity types – the J rule. In fact, not many things are explained about HoTT in Negarestani's talk, which is quite puzzling, since HoTT is not, by any means, neither a well known, nor an easy theory, and his talk was meant to be about... HoTT. One of the few things he mentions about HoTT is that

"the formal stress that homotopy type theory places on transport across equivalences does resonate with the project of world making, not as a celebration of arbitrariness, but as a study of the condition under which redescription remains objectively accountable". But we could easily say this about univalence, or more generally, about category theory. But then again, what does this have to do with arbitrariness or with objectively accountable redescription, whatever that means?

If it is clear that a text will make just as much sense to a reader as Derrida's infamous seminar talk about cows before he was told that he should pronounce that recurring term as 'chaos', why bother writing it? There are no shortcuts: you need to do the work. If you want to talk about HoTT and the Curry-Howard correspondence, you need to at least study Homotopy Type Theory: Univalent Foundations of Mathematics (The Univalent Foundations Program 2013) – only after Per Martin-Löf's Intuitionistic Type Theory (Martin-Löf 1984) – and a gentle presentation such as Philip Wadler's excellent nugget Propositions as Types (Wadler 2015) or the Lectures on the Curry-Howard Isomorphism (Sørensen & Urzyczyn 2006). Nonetheless, in all honesty, this short mandatory reading list on its own is nowhere close to being enough. We just hope Schmid read it before writing his book.