What Can Category Theory Do For Philosophy?

December 6, 2012

What Can Category Theory Do For Philosophy?

Posted by David Corfield

$MathML-enabled post (click for more details).$

I’m thinking of organising a meeting next Summer, perhaps in July, here in Canterbury to address the question in the title.

What feels like an age ago, I wrote that I wasn’t looking for (higher) category theory to be the tool to spark off an analytic philosophy Mark II. I meant by this that I wasn’t looking for a rerun of the transformation in philosophy brought about by Frege’s logic as taken up by Russell, Carnap, etc. Rather, I looked on the reconceptualisation of the basic notions of mathematics brought about by category theory largely as a sign that we should never forget that we are historically situated beings, aiming for something of enduring value, but in the full expectation that our successors will see what we achieve as limited in many respects.

I’m still sympathetic to that point of view, but clearly it shouldn’t stand in the way of work that actively uses the formalisms provided by (higher) category theory to allow progress to be made on what are counted as philosophical issues. It has seemed to me for a while somewhat arbitrary which formalisations of which subject matters fall under the remit of philosophy. Search for a probabilistic logic and you’re in, rethink basic geometric concepts and you’re not.

Anyhow, here are some topics which might be treated at such a meeting:

Categorical logic & type theory (especially of the intensional dependent variety)
Modal logic
Physics & structuralism
Other metaphysics, e.g., identity, space, quantity
Probability theory, stochastic mechanics & machine learning
Other: biology, natural language, Arrow’s theorem,…

I’d be interested to hear any thoughts on such a meeting and about anything else you might like to see. I’m maintaining a page at my personal wiki to gather some ideas. If you’d rather not write to a public blog, you can contact me via here.

Posted at December 6, 2012 9:46 AM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2576

34 Comments & 0 Trackbacks

Re: What Can Category Theory Do For Philosophy?

This might fall under #3, but category theory has also been applied to philosophy of science more broadly. I’m thinking in particular of the work of James Weatherall and Hans Halvorson, the latter of whom is currently applying category theory to the problem of theory individuation.

Also, for what it’s worth, I think holding such a meeting would be a valuable thing.

Posted by: John Dougherty on December 6, 2012 5:10 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

Yes, I recently read Halvorson’s What Scientific Theories Could Not Be. We catch a glimpse at the end of the paper of the Awodey-Forssell approach to theory-model duality.

From the Schreiber perspective, of course, it’s not surprising that category theory provides the right tools to think about how best to consider physical theories. Universal constructions are everywhere.

Posted by: David Corfield on December 7, 2012 9:24 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

Hi David,

sorry for the immensely slow reaction here. Only now do I see your post here, and understand where our discussion on the nForum came from, on your side.

Now I am looking through Halvorson’s article that you pointed to above.

There are several points where I don’t follow the argument given there. This may well be my fault, but let me tell you about some of my puzzlement.

Right on the first page I see that “scientific theory” is identified with a theory as in logic. (I’ll provide some $n$ Lab links for eventually interested bystanders, to make this more self-contained.) Even though – I understand – the author’s whole point is to argue that this is not a good approach, that one should instead consider the models of such theories, I find that a dubious starting point.

Clearly, not every theory-as-in-logic is a “scientific theory”! I would think. Not only is soemthing like “the theory of groups” not a “scientific theory”, but worse, there are lots of random theories-as-in-logic that formally qualify as “theories” in this sense, but which are not theories of anything that we would care to give a name, be it mathematics or be it the sciences.

And, I should hasten to say in view of Halvorson’s main point, just as clearly is not every collection of models-as-in-logic a collection of models of some scientific theory.

Or so it seems to me.

To me it seems that the main problem with even getting started with such a kind of discssion is that one needs to figure out what a formal meaning of “physical theory” might be in the first place. Maybe one needs a “theory-in-the-sense of logic of theories-in-the-sense-of-physics”.

We had had related discussion here every now and then. As you know, there are people who made an attempt in this direction, proposing that a “physical theory” in the formal sense is a topos equipped with an object called the “phase space object” subject to some conditions. Given that, they proposed a way to interpret the idea of “physical observable” etc. in these axioms.

I am not sure if I find these proposals fully convincing, but I do appreciate that at least they do see the need to make some proposal in this direction at all. Something like this seems to be necessary to make any progress with the kind of question that the above article wants to address.

Or so it seems to me.

Of course we could settle for something less ambitious, but closer to actual practice in physics. Instead of trying to formalize what “physical theory” means in full generality, we could decide that since we already know that the best kind of physical theories – in the sense of fundamental accuracy – are not random theories about things that look like physical observables, but are quantum field theories, that therefore a formalization of “physical theory” just needs to be a formalization that allows to specify points in the moduli space of quantum field theories. This is a question where at least we have recently seen a whole lot of progress in, and where I wouldn’t be surprised to see a satisfactory and useful fully formal conceptualization of soon.

That would be my criticism of the very starting point of the above article. But I have further puzzlements also when reading on.

For instance on p. 3 it says that

a model of the general theory of relativity is a four dimensional Lorentzian manifold

and again on p. 5, more pronounced:

we identify the theory of general relativity with the class of general relativistic spacetimes (i.e. four-dimensional manifolds with a Lorentzian metric),

I am not sure what to make of this statement. Taken at face value it is clearly wrong: from the collection of (and let it be the category of) Lorentzian manifolds, one can certainly not recover in any meaningful sense Einstein’s equations of general relativity, and certainly not the additional field content that must be invoked in order to obtain suitable energy-momentum tensors such as to make any Lorentzian manifold a solution…

The standard way to say what the “theory of general relativity” is, is to state Einstein’s equations, or else state the Einstein-Hilbert(-Maxwell-Yang-Mills) action functional of which these characterize the critical points. And that feels more like specifying a “theory”, if we think of an equation as being the “theory” of which its solutions are “models”.

And for all of this to qualify as a discussion of “theory of physics” in the first place, we have to assume that we intentionally restrict to just the approximate notion of classical field theories anyway. Because the true quantum field theory induced by an action functional is not fixed by the collection of its critical points anyway.

If I think about these mattes, what I can come up with is an indication, at the horizon, of a theory-as-in-logic of a Lagrangian-quantum-field-theory-as-in-physics, as follows in the next paragraph. But notice that even so, this is a rather different perspective than that of the above article: in what I say next a theory-as-in-physics is a model-as-in-logic of the theory-as-in-logic of physical theories. For each such we can consider its covariant phase space of classical solutions, which would be the collection of what the above article apparently calls the collection of models of the theory-as-in physics. Beware, though, that model-in-theoretical-physics in the standard sense is something different alltogether. It is rather a model in my sense here, of the theory-of-physical-theories (to the extent that we can identify this).

So this would be the axiomatization of the theory-of-theories-of-physics as I seem to see it faintly on the horizon:

the ambient logical framework is natural deduction realizing homotopy type theory.

In there, we first of all add the axioms for cohesive homotopy type theory.

This allows to axiomatize the following, in turn:

the group $\mathbb{G} := \mathbb{A}^1 / \mathbb{Z}$
the differential cohomology coefficient types $\mathbf{B}\mathbb{G}_{\mathrm{conn}}$

Then: an extended prequantum field theory of dimension $n$ with moduli stack of fields any type $\mathbf{Fields}$ is a function

$\mathbf{L} : \mathbf{Fields} \to \mathbf{B}^n\mathbb{G}_{conn} \,.$

Period.

As I said, that’s what I can currently see on the horizon. I am not claiming that this is fully the last answer. But it sure does seem to go in a sensible direction.

You know what I am alluding to here. Other readers may find exposition of how the above relates to quantum field theory in our recent exposition A higher stacky perspctive on Chern-Simons theory .

Posted by: Urs Schreiber on December 28, 2012 4:30 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

Thanks for this, Urs.

Clearly, not every theory-as-in-logic is a “scientific theory”!

This seems so clear that perhaps we should interpret the remark to be about necessary conditions of being a scientific theory, rather than sufficient ones. As far as I’m aware, nobody has tried to delimit amongst whatever they take to be all possible theories, those which might be termed ‘scientific’. In particular, I haven’t seen a search for

“theory-in-the-sense-of-logic of theories-in-the-sense-of-physics”.

Perhaps it’s best to see this work as pointing to the possibility of resolving, by means of the novel tools provided by category theory, a problem philosophers of science have considered for many years. This problem is that it’s not straightforward to say of two theories whether they’re the same or not. Now, to the extent we treat theories in terms of their categories of models, we can propose that an equivalence between such categories implies equivalence of theories.

Perhaps it strikes you as odd to be interested in this sort of issue (especially since the resources to resolve the issue about equivalence of theories-in-the-sense-of-logic have been available for many decades already, though Awodey-Forssell have a new reconstruction result). So why turn to category theory for such a simple task at a time when wonderful connections are being made between cohesive homotopy type theory and physics?

Perhaps something to say is that the kind of question you’re pursuing is ‘philosophical’ more in the sense of what Michael Friedman calls ‘meta-scientific’ (Newton, Helmholtz, Lie, Poincaré,Einstein,…), than work of the kind ‘let’s make sense of a revolution after the event’ (Kant, Carnap,…).

Posted by: David Corfield on December 29, 2012 2:43 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

It’s maybe worth noting that there are three category theory events already scheduled for July: (1) a workshop at Macquarie, 2–5 July, (2) the major conference, Category Theory 2013, also at Macquarie, 7–13 July, and (3) the Samuel Eilenberg Centenary Conference in Warsaw, 22–26 July.

Posted by: Tom Leinster on December 7, 2012 4:24 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

Ah, that’s useful to know.

Posted by: David Corfield on December 9, 2012 8:21 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

One question I’d like to know the answer to is why the Structuralism promoted by Category Theory is different from Philosophical Structuralism, it’s “the belief that phenomena of human life are not intelligible except through their interrelations. These relations constitute a structure, and behind local variations in the surface phenomena there are constant laws of abstract culture”.

Perhaps, it’s because this movement was in Continental Philosophy, and motivated by developments in linguistics, rather than mathematics. I understand that there was (still is?) a sharp divide between Continental Philosophy and the Analytic Anglo-American tradition.

It somehow doesn’t surprise me, that there was a rerun of the analytic debate: presumably seeing its universalising tendencies in mathematics, they saw it as a revival of their hopes, of what they thought of as the universalising tendancies of the Hilbertian Formalist School/Vienna Circle.

Is the hope to import Continental methods into the Anglo-American philosophical community via subversive means? Or at least bridging the gap, a bit.

Posted by: mozibur ullah on December 9, 2012 12:50 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

[Typo fixed]

It would be interesting to explore possible connections with Continental uses of the term ‘structuralism’ I read a fair bit of Levi-Strauss in my youth. André Weil worked with him. References can be found in Morava’s own development.

I was intending more Anglophone notions of structuralism, from that of the philosophy of mathematics to the structural realism of some philosophers of science.

The extraordinary thing is how little attention is paid to category theory, especially in the case of the latter, but even in that of the former. I’ve been heartened recently coming across the section ‘Category theory in the philosophy of science’ on James Weatherall’s site.

Posted by: David Corfield on December 9, 2012 9:00 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

Steve Awodey argues that category theory provides a framework for philosophical structuralism.

Posted by: Bas Spitters on December 9, 2012 7:55 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

I expect you’re aware of your friend Colin McLarty’s excellent article Exploring categorical structuralism. I think many readers here would enjoy it too.

Posted by: Tom Leinster on December 9, 2012 11:56 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

Yes, both very good articles. It’s worth noting that neither Colin nor Steve are your typical analytic philosopher who would be after some definitive metaphysical account of what mathematics is about. Colin has interests in the historical emergence of new kinds of mathematical thinking, in particular, in the hands of people such as Emmy Noether and Grothendieck. Steve has done historical work on Carnap, and I would say works more as a mathematical logician, than a philosophical one.

It seems to me only sensible to avoid definitive metaphysics. Sure, if you’re good enough, like Russell, you can help with the emergence of a new way of thinking about mathematics. But you should surely take it as inevitable that it will only be a very partial view which will be superseded.

Collingwood made a similar point in the 1930s about the metaphysician who decrees that physics is the science of matter, as though there were some independent way of knowing what matter is other than through physics. What could you have achieved other than, at best, an account of what are the current presuppositions of physics? And, as Collingwood noted, generally it is to give as timeless truths the presuppositions of an earlier generation, quite possibly those delivered to you during your early education in physics before you turned to philosophy.

All this in not to say there isn’t useful work to be done teasing out current conceptions and the tensions between them. And there’s useful work to be done in bridging disciplines. Had philosophers of science looked into category theory earlier, who knows what sparks might have been generated.

Posted by: David Corfield on December 10, 2012 9:18 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

At the heart of classical structuralism lies the observation that in the practice of modern sciences like mathematics, physics and linguistics knowledge claims are made less on objects but on intrinsic relations and interdependencies. From this perspective structuralism is an epistemological hypothesis on the sciences which attempts to provide a mental hygiene for the individuals sciences by purging theories from statements that are not structurally invariant.

As such there is nothing particularly ‘continental’ about the hypothesis that is compatible with whatever your favorite philosophy happens to be e.g. Carnap articulated it in the most explicit form in ‘Der logische Aufbau der Welt’ of 1928 within an empiricist-operational approach to science whereas Roman Jakobson tied it to Husserlian phenomenology and, of course, a platonist structural realism also conveniently accomodates it.

‘Parisian’ structuralism, whose main inspiration and paradigm was the work of Levi-Strauss, added the supplementary ‘semiotic’ hypothesis that human institutions and forms of expression are sign systems and as such should be studied by the techniques of structuralist linguistics thereby giving scientific foundations to the humanities. It is fair to say that as a research program this has largely failed (Personally, I would probably exempt Levi-Strauss here) and was replaced by the end of the 1960s by more fashionable forms of poststructuralist philosophy.

In my view, the above epistemological structuralism is the mere diagnosis of the state of affairs in advanced sciences that practising scientists better take into account in the way they do science and philosophers of science better pay attention to. To the extent that category theory is the congenial language of this structuralism at work it can facilitate scientists and philosophers their respective tasks.

Hence epistemological structuralism is very much alive and should be on the research agenda continental or not. The main obstacle to revive semiotic structuralism is the decline of structuralist linguistics which as a research paradigm has been replaced in contemporary linguistics by Chomskian generative grammar. In my view, semiotic transcendentalism i.e. the hypothesis that (at least knowable) reality has the structure of language has still much to recommend itself but it faces the challenge to give a structuralist account of generative grammar or a viable structuralist alternative.

Let me close with a recommendation of Louis Hjelmslev’s ‘Prolegomena to a theory of language’ (2nd ed. 1961). The thought of the Danish linguist and son of the mathematician Johannes Hjelmslev is in many ways the intellectual culmination of structuralist linguistics inspired by de Saussure and its epistemology. Being quite familiar with the works of Russell, Hilbert, Carnap and Tarski Hjelmslev tried to lay axiomatic foundations of linguistic structuralism in a topological ‘prelogic’ which has many points of contact with the work of Lawvere on axiomatic cohesion and repays the reading even nowadays for a philosopher of mathematics, who will find there definitions of cohesion, variable, class, intensive/extensive ‘quantity’, form, substance etc.

Posted by: thomas holder on December 13, 2012 4:53 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

The SEP entry on Structural Realism says ‘certainly, the structuralist faces a challenge in articulating her views to contemporary philosophers schooled in modern logic and set theory, which retains the classical framework of individual objects, and where a structure is just a particular set’. Perhaps this (set theory) is the same reason why philosophers aren’t talking to category theorists. If categorical foundations and topoi (as generalised set theories) become more widely desseminated and understood, it may help to push the two communities together a bit more.

I know that Badiou, a continental philosopher is interested in both Set and Category Theory, calling the first ‘the very site of ontology’. What he means by that I do not know; (but Scruton says that ‘the jargon of set theory is waved like a magician’s wand, to give authority to bursts of all but unintelligible metaphysics’). From what I hear, he’s meant to be in vogue in certain American and European campuses.

Posted by: mozibur ullah on December 20, 2012 1:53 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

I’ve never found Scruton to be a very good philosophical guide, myself. He’s always seemed more interested in polemic and scoring points on his political opponents than in reaching genuine understanding.

I found Badiou (in Number and Numbers) hard going, but worthwhile. He’s a very old-fashioned set-theoretic realist, very much in the tradition of Cantor. His idea, basically, is that the ontology of science (does/should?) consist of re-presentations of the ontology of mathematics, and he makes use of set theory since that’s the most plausible way of forming an ontology for all of mathematics. This is a very Quinean idea, except that he thinks that the linguistic turn was a fruitful mistake – weak systems have too many models, which makes them inadequate for use in ontology, on his view.

To a type theorist like myself, this is a very stimulating argument: Badiou basically completely rejects the inductive constructions that underpin type theory. Instead, he prefers viewing numbers in a sort of Dedekind/Frege impredicative style, where the induction principle tells you what numbers are. This is, incidentally, almost a categorical structuralist view of number, even though Badiou is explicitly a realist who rejects the ontology of structuralism.

It’s very interesting to see a philosopher identify the extraordinary significance of the Dedekind/Frege program of formalizing number. I have the impression that he regards the failure of this program in much the same way that Cantor regarded the absolute infinite: he sees its inexpressibility as a limitation of finitary syntax, rather than an indication of its nonexistence. (However, I remain fascinated by this program because it seems barely possible that it could be salvaged using the theory of parametricity for System F, which offers a differing account of impredicativity than set theory does.)

Posted by: Neel Krishnaswami on January 2, 2013 1:57 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

I’m confused. Isn’t the induction principle precisely the characterizing property of an inductive construction?

Posted by: Mike Shulman on January 3, 2013 1:13 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

Hm. There used to be a freely available English translation of Dedekind’s What Are the Numbers, and What Should they Be? online, but I can’t find it anymore.

Anyway, as I understood it, the way Dedekind tried to define the natural numbers was to (1) state the induction principle for the natural numbers, and (2) say that a set of pre-numbers is any set that can be a model for the induction principle, and (3) argue that if you “abstracted away” all the features not shared by all the sets of pre-numbers, you were left with a unique set of natural numbers.

I found his uniqueness property extremely surprising – in ZF, you can prove the categoricity of the natural numbers, but you certainly can’t prove that all models of the natural numbers are actually equal! In his argument, Dedekind relied on the ability to treat abstraction as an operation. This is not really sensible in modern mathematical formalism, but I found it strongly reminiscent of the way data abstraction works in type theory.

I’ve thought for a while that it ought to be possible to use type theory to resuscitate this old intuition. I don’t want to claim too much, yet, but in a recent paper with Nick Benton, we showed that if you (a) extend System F with equation types, then (b) all inhabitants of the existential datatype corresponding to the signature of the Peano axioms are equal. So in a sense Dedekind’s argument is indeed a valid proof. One limitation of this approach is that while it works for induction principles, I don’t see how to extend it to allow large eliminations (i.e., the definition of sets or types by recursion on a number).

Posted by: Neel Krishnaswami on January 3, 2013 9:34 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

I had no idea that Dedekind had invented the univalence axiom! (-: In univalent type theory, the type of all models of the induction principle for natural numbers is contractible, i.e. has a unique inhabitant. You just prove that they are all uniquely isomorphic, and then invoke univalence.

But I don’t quite see how this answers my confusion about what you said Badiou is trying to say?

Posted by: Mike Shulman on January 4, 2013 11:38 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

That’s very funny! To perhaps take your joke a little more seriously than I ought :), I think univalence is stronger than what Dedekind had in mind – unless I misunderstand it (entirely possible, btw), univalence would let you prove the equality of the set of natural numbers with the rationals, since there’s an isomorphism between them.

I’m pretty sure Dedekind didn’t want to go that far, though. Bearing in mind that formal logic and set theory didn’t yet exist when he wrote this paper, I got the impression that he wanted to say something like (consistent) theories with a categoricity property have unique models. Nowadays, we satisfy ourselves with categoricity – that the models are unique up to isomorphism, but Dedekind’s idea seemed to be that if the only things you did with particular models were the common operations, you could “abstract away” the differences between the isomorphic models and treat them as if they were the same. (This is what reminded me of data abstraction in type theory.) Note that unlike with univalence, you couldn’t identify the rationals and the naturals, since they don’t have the same signature.

What makes this relevant to Badiou is that in proving categoricity for the natural numbers, Dedekind made free use of higher-order logic and impredicative definitions. And in fact, Frege defined the natural numbers with impredicative quantification, and of course the type of the Church encoding of the naturals in System F is just the pure second-order version of the induction rule. This approach is sort of the opposite of the usual route, where you explain how to construct the inductive type and then use that to justify the induction principle. Instead, you end up saying, sort of, “I have the universe, and now by asserting an induction principle I can pick out just the bits that satisfy the properties I am interested in.”

Badiou likes the impredicative approach, because he sort of wants to say that mathematical objects give us the ontology we can make scientific theories out of. Since any fixed set of inductive set-formers is inherently incomplete, this is an obstacle to his goal. Impredicative, higher-order constructions are less obviously defective. (Of course, there’s this whole debate about whether second order logic is logic, which simply puts me to sleep, so I have no opinion there.)

Badiou is pretty clearly conversant in modern set theory but I don’t get the impression he knows much, if any, category theory. He also has a bunch of strained stuff in his book about the politics of numbers, but I found the pure philosophy-of-math stuff pretty interesting. I don’t get the impression that a set theorist would find his ontology all that radical (though they might be bemused by the importance he ascribes to the surreals), but to a type theorist like me it was an interestingly different perspective.

Posted by: Neel Krishnaswami on January 5, 2013 7:17 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

“Theories with a categoricity property have unique models” sounds to me exactly like univalence. Just as always in type theory, the way that univalence makes things “equal” depends on what type at which they are compared. The natural numbers and the rational numbers are equal as sets, but once you equip them with the structure for some signature, then if the signatures are different, you can’t compare them, while even if the signatures are the same, they might be unequal structures. A set (or type) doesn’t “have” any signature until you give it a structure.

For instance, consider the signature consisting of a single nullary operation and a single unary operation. The type of structures in this signature is $NatSig \coloneqq \sum_{A:Type} A \times (A\to A)$ One inhabitant of this type is $(\mathbb{N},0,S)$ . And if you form the subset type $\sum_{A:NatSig} hasInductionPrinciple(A)$ then by categoricity and univalence, this type will be contractible, and in particular any two elements of it will be equal.

The rational numbers could be made into an element of $NatSig$ in an obvious way such as $(\mathbb{Q},0,\lambda x.x+1)$ , but this would not be equal to $(\mathbb{N},0,S)$ as elements of $NatSig$ , because even though $\mathbb{Q}$ is bijective (hence equal) to $\mathbb{N}$ , the bijection does not respect the additional structure. On the other hand, by fixing a bijection $\mathbb{N} \leftrightarrow \mathbb{Q}$ we could transport $0$ and $S$ from $\mathbb{N}$ to $\mathbb{Q}$ , and then we would get an element of $NatSig$ whose first component is $\mathbb{Q}$ and which is equal to $(\mathbb{N},0,S)$ .

It’s really precisely about data abstraction.

This approach [impredicative definitions] is sort of the opposite of the usual route, where you explain how to construct the inductive type and then use that to justify the induction principle.

Huh, that’s weird. I’ve never thought of the impredicative encoding of an inductive type as somehow “opposed” to or “opposite” to the inductive presentation; to me they are just two sides of the same coin. The introduction and elimination rules determine each other, so it doesn’t really matter which one you start with.

Posted by: Mike Shulman on January 7, 2013 6:00 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

You gave a rich response, so I broke my reply into three reasonably independent pieces.

I don’t quite understand what you mean by “a type doesn’t have a signature until you give it a structure”. Your $\mathrm{NatSig}$ type can be read as a tuple of a (small) type, plus two operations on it (the intended zero and successor operations).
I can see that $(\mathbb{N}, 0, s)$ is not equal to $(\mathbb{Q}, 0, \lambda x.\,x+1)$ at type $\mathrm{NatSig}$ since there isn’t a structure-respecting isomorphism. That’s just beautiful, and thanks for such a clear explanation! I think it’s fair to say that univalence really does seem like an explanation of abstraction in the sense of the old logicians.

However, I’m still reluctant to identify univalence with data abstraction in the sense of computer science, exactly since you cannot use $\mathbb{Q}$ , $0$ , and $\lambda x.\,x+1$ and the appropriate proofs to give an element of: $\sum_{A:\mathrm{Type}} A \times (A \to A) \times \mathrm{PeanoAxioms}(A)$ Existential types (aka weak sums) in System F do permit exactly this kind of data representation, since you cannot construct elements of the unknown type $A$ except by applying the two operations in the signature.

This is all a little puzzling. I’m guessing the difference is that sigma-types have projective eliminations, and so if $e : \sum_{A:\mathrm{Type}} A \times (A \to A)$ and $e = \left(X, i, f\right)$ , then you know that $\pi_1(e) = X$ , allowing you to cook up arbitrary elements of $X$ to feed to the operations?

But there doesn’t seem to be any obvious reason you couldn’t add existential types (weak sums) to a dependent type theory with univalence.
By impredicative encoding, I meant something like the Church encodings in impredicative type theory. You can construct an element of NatSig, with the appropriate induction principle, using the type
$\mathrm{ChurchNat} \triangleq \Pi A:\mathrm{Type}.\;A \to (A \to A) \to A$

What makes this work is that unlike in MLTT, there is no size distinction on $\mathrm{Type}$ – you are free to instantiate $A$ with $\mathrm{ChurchNat}$ , for example. (This has a bit of the flavor of Frege’s definition of the natural numbers in terms of the ancestral.)

In Martin-Loef type theory, universe checking will prevent you from doing this, which means you need to equip your type theory with some inductive type mechanism to define things like the natural numbers. (This is clearly necessary since MLTT without natural numbers or W-types has a model in finite sets, and so obviously cannot define the natural numbers.)

Posted by: Neel Krishnaswami on January 8, 2013 9:11 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

This was intended as a direct reply to your statement that “you couldn’t identify the rationals and the naturals, since they don’t have the same signature”. The rationals and the naturals by themselves are just sets (types); they don’t have any signature (or equivalently, they have the empty signature). If you equip the naturals with zero and successor and the rationals with some other structure, then you get two structures with different signatures, but you could also equip the naturals and rationals with two structures having the same signature, in either an equivalent way or an inequivalent way, as I described.
How exactly do you plan to prove that $(\mathbb{Q},0,\lambda x.x+1)$ satisfies the Peano axioms?
Yes, that’s what I meant by “impredicative encoding”. I was trying to say that I don’t think it makes much difference whether you define an inductive type using an impredicative encoding (in which case what you specify is the eliminators), or give a basic rule of type-formation for inductive types (in which case what you specify is the constructors); the notion of “inductive type” that you get out at the end is the same. I mean, certainly there are all sorts of differences between the two constructions, but it doesn’t seem to me that preferring an impredicative encoding amounts to rejecting inductive types; it’s just about choosing one property or another as the definition, like whether you use open sets or closed sets when defining a topological space.

Posted by: Mike Shulman on January 8, 2013 6:17 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

Ah, I was just confused because both the “bare set” and the sigma-type containing signature are types, and I got confused which one you were referring to.
You do this using Reynolds’ technique of “relational parametricity”, which is the same technique needed to prove the induction principle for the Church encoding of the natural numbers. In categorical terms, $\beta\eta$ -equality suffices to show that the Church naturals form a weak natural numbers object, and you need stronger reasoning principles to show the universal property, which is what parametricity supplies.

The basic idea is that in addition to the standard interpretation of types, we also give a second semantics of types, in which types are interpreted as relations, and type constructors as operators on relations.

The relational interpretation of functions will be something like $(f,g) \in [A \to B]\;\rho$ , if for every $(x,y) \in [A]\;\rho$ , we have $(f\,x, g\,y) \in [B]\;\rho$ , and
the relational interpretation of universal quantification will be something like $(f, g) \in [\forall \alpha.\;A]$ if for every relation $R$ , we have $(f, g) \in [A]\;(\rho, R/\alpha)$ , and
the relational interpretation of existential quantification will be something like $(f, g) \in [\exists \alpha.\;A]$ if there is a relation $R$ , such that $(f, g) \in [A]\;(\rho, R/\alpha)$ .

Then, you prove that every typeable term is related to itself in the relational interpretation, and this lets us conclude that the program language respects data abstraction. (I’m glossing over an awful lot of details, which I intend to blog about in the coming weeks, since I’m just finishing a paper submission about parametricity and dependent types. In the meantime, let me suggest Rosolini’s Reflexive Graphs and Parametric Polymorphism, which as a categorically-minded presentation may be more accessible to you. Or if he’s handy, just ask Bob Harper sometime.)

So if you implement the natural number signature using $(\mathbb{Q}, 0, +)$ , then you can interpret it with a relation consisting of the subset of the rationals corresponding to the usual natural numbers. And since every operation in the signature preserves this relation, we can conclude that using the operations in the Peano signature, we can never construct an element of $\mathbb{Q}$ that is outside of this set.

In a related way, you can show that for any “definable endofunctor” $F$ (i.e., a term $F : \mathrm{Type} \to \mathrm{Type}$ with a term $\mathrm{map} : \forall \alpha, \beta:\mathrm{Type}.\; (\alpha \to \beta) \to (F(\alpha) \to F(\beta))$ which preserves identities and composition), the type $\mu \alpha.\; F(\alpha) \triangleq \forall \alpha:\mathrm{Type}.\;(F(\alpha) \to \alpha) \to \alpha$ is the initial algebra corresponding to the inductive data type. (Similarly, you can code coinductive types as $\exists \alpha. \alpha \times (\alpha \to F(\alpha))$ .)

This all sounds innocuous, rather like a simple “categorification” of the Knaster-Tarski theorem, but it’s a strongly anti-classical type-formation principle. Note that $F(\alpha) \triangleq (\alpha \to 2) \to 2$ is functorial, and so parametricity implies that $\mu \alpha.\;(\alpha \to 2) \to 2$ is a well-defined inductive type. This is flatly incompatible with a set-theoretic reading of types, since no set can be isomorphic with its powerset, let alone its double powerset. (This is why dependent type theories tend to restrict inductive types to strict positivity, so that they don’t have to give up the possibility of a classical reading.)

Personally, I like anti-classical axioms, but also think it’s wise to keep clear when they are and aren’t needed.

Finally, on a pragmatic note, it’s as yet unclear how to make Church-encoded natural numbers play nicely with large eliminations. This may simply be a matter of not enough thought devoted to the issue (not many people have worked on the combination of parametricity and dependent types), but it may also touch upon deeper foundational issues. At any rate, computing with types — i.e., large eliminations — is one of the principle attractions of type theory, at least for me.

Posted by: Neel Krishnaswami on January 10, 2013 10:37 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

I know a bit about parametricity; in fact, I’m in the process of writing a paper and a blog post about it from the categorical/homotopy perspective. But I don’t understand what you’re saying about it. There can’t possibly be an inhabitant of $PeanoAxioms(\mathbb{Q},0,+1)$ , since that would be inconsistent with the set-theoretic model. It sounds like you’re saying that the relational model contains a different object whose underlying type is $\mathbb{Q}$ (but which is not the interpretation of “ $\mathbb{Q}$ ” in the relational model) and which… has some property or other. It seems to me that it can’t satisfy the property $PeanoAxioms$ internally to the relational model either, since then it would be isomorphic therein to the NNO — but their underlying types are not isomorphic, so they can’t be relationally isomorphic. What exactly are you saying about this object?

Posted by: Mike Shulman on January 10, 2013 11:01 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

Yes, there’s no interpretation of $\mathrm{PeanoAxioms}(\mathbb{Q})$ . But that’s not the relation we need to use!

So, suppose we have the existential type $\exists \alpha. \mathrm{Peano}(\alpha)$ , and we want to show that we can use the rational numbers to inhabit this type. What we’ll do is show that the terms $\mathrm{pack}(\mathbb{Q}, 0, +1, properties\ldots)$ is related to itself at the type $\exists \alpha. \mathrm{Peano}(\alpha)$ .

To do this, we can choose the relation:

$Q = \{(q, q') \in \mathbb{Q} \times \mathbb{Q} \;|\; q = q' = +1^k(0)\}$

Now, note that (0, 0) is in the relation $Q$ , and +1 is also related to itself in the relational action $Q \to Q$ . The iteration function (which realizes the induction principle), and is defined as: $\begin{array}{lcl} iter & : & \forall \alpha. \alpha \to (\alpha \to \alpha) \to \mathbb{Q} \to \alpha \\ iter & = & \lambda \alpha, i, f, n.\; \mathrm{if}\;n = 0 \;\mathrm{then}\;i \;\mathrm{else}\; f(iter\;\alpha\;i\;f\;(n-1)) \end{array}$ also lies in the interpretation of $\forall \alpha. \alpha \to (\alpha \to \alpha) \to Q \to \alpha$ — I am abusing notation here, but I hope you see what I mean. (As an aside, note that here we need to use the fact that we only pass arguments in $Q$ to $iter$ to guarantee the termination of this function.)

These facts then let you prove that the Peano axioms are satisfied by the implementation. I (currently) believe this requires us to organize the treatment of equality quite differently than the inductive definition Martin-Loef gives, since we may need to do quite nontrivial proofs (though they can be made proof-irrelevant) to show equality. I have thought the rules we need will end up looking something like Abadi-Plotkin logic.

However, if there’s a connection with univalence, then that’s incredibly exciting; I await your post with bated breath!

Posted by: Neel Krishnaswami on January 11, 2013 10:29 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

What is your definition of $Peano(\alpha)$ , and what do you mean by the Peano axioms being “satisfied?”

Posted by: Mike Shulman on January 11, 2013 6:34 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

The signature I used in my paper with Nick Benton is: $\begin{array}{ll} \exists \alpha:\mathrm{Type}. & z : \alpha \\ & s : \alpha \to \alpha \\ & iter : \forall \beta.\; \beta \to (\beta \to \beta) \to \alpha \to \beta. \\ & \forall \beta, i:\beta, f:\beta \to \beta.\; iter\;\beta\;i\;f\;z = i \;\times \\ & \forall \beta, i:\beta, f:\beta \to \beta, x:\alpha.\; iter\;\beta\;i\;f\;(s\;x) = f(iter\;\beta\;i\;f\;x) \end{array}$ We can show that there’s an isomorphism between this type and the Church naturals, and of course the Church naturals can be shown (again by parametricity) to contain just the natural numbers.

The guiding idea is that the relational interpretation of an equality type $e = e' : X$ is that this type is inhabited when $(e, e')$ lies in the relational interpretation of $X$ (eliding issues of free variables and substitutions).

Be warned that we haven’t worked out the proof theory of equality yet, and so the type theory appeals to the model as a semantic side-condition on equality introduction. That’s why my comments about the relation between the equality type and Abadi-Plotkin logic were prefaced with “I believe” and “I think” rather than “we have shown”!

Right now, we just inhabit equality types with a dummy reflexivity value when the equality should hold, but ultimately, equality proofs should contain evidence that the two terms are related by the relational interpretation of the type. However, we’re as yet some distance from making that work. For instance, under this approach it’s rather delicate to show even that the equality proposition lets you prove transitivity.

We’ll get there eventually, but I certainly hope you folks in Princeton can smooth the road for me. Setting the foundational issues aside, I find the purely technical work on HTT on equality types with nontrivial inhabitants very compelling.

Posted by: Neel Krishnaswami on January 11, 2013 8:07 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

But that type is not the Peano axioms; it doesn’t include induction. So of course you can inhabit it by any weak natural numbers object, which includes $\mathbb{Q}$ .

Posted by: Mike Shulman on January 12, 2013 6:55 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

Oh, wait, no, I’m even more confused: how does $\mathbb{Q}$ inhabit that type? E.g. if $\beta$ is $\mathbb{N}$ , with the usual $0$ and $s$ , then what is $iter(\mathbb{N},0,s)(-1) :\mathbb{N}$ ? Wouldn’t it have to be a natural number whose successor is $0$ ?

Posted by: Mike Shulman on January 12, 2013 7:00 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

Two terms $pack(X, x)$ and $pack(Y, y)$ will be in the relational interpretation of $\exists \alpha.A$ , if there is a relation $R \subseteq X \times Y$ , such that $(x, y) \in [A](R/\alpha)$ , where $[A]$ is the relational interpretation of $A$ .

So, in this case, we want to show that $pack(\mathbb{Q}, 0, +1, \lambda \beta, i, f.\; refl, \lambda \beta, i, f, x.\; refl)$ is related to itself at the type $\exists \alpha. \ldots\mathrm{stuff above}\ldots$ .

Note that the definition above leaves us free to choose the relation $R$ . So we can choose: $R = \{ (q, q) \in \mathbb{Q} \times \mathbb{Q} \;|\; q = +1^{k}(0) \}$

Now, here’s the really critical idea: not all of the elements of $Q$ are in this relation. The idea is that since we have an abstract type, the only way programs which use the existential package can construct elements of the existential type is by using the operations in the interface. And we’ve arranged things so those operations only let us construct $0$ and its successors from $\mathbb{Q}$ .

So type abstraction keeps clients from being able to construct all the elements of the implementation type, which is the key to maintaining invariants on data structures. In this case, it’s simply not possible to apply -1 to iter, since it cannot be constructed by applications of $z$ and $s$ .

This can be established by showing that:

$(0, 0) \in R$ ,
$(+1, +1) \in R \to R$ , and
$(iter, iter) \in [\forall \beta.\;\beta \to (\beta \to \beta) \to \alpha \to \beta](R/\alpha)$
$(\lambda \alpha, i, f.\;refl, \lambda \alpha, i, f.\;refl) \in [\forall \beta., i:beta, f:\beta \to \beta.\; iter\;\beta\;i\;f\;z = i](R/\alpha)$ .
$(\lambda \alpha, i, f.\;refl, \lambda \alpha, i, f, x.\;refl) \in [\forall \beta., i:beta, f:\beta \to \beta, x:\alpha.\; iter\;\beta\;i\;f\;(s\;x) = f(iter\;\beta\;i\;f\;x)](R/\alpha)$ .

Effectively, our choice of relation lets us state an invariant on our data structure, and then our proof obligation is to show that the implementation we give respects the invariant. If that’s true, then we know that no program can break the invariant, since all the terms of the language respect the relational interpretation.

This is essentially what makes it possible to (a) derive the rest of the Peano axioms from the given interface, and (b) show that all elements of this type are related to one another. (In some sense, it shouldn’t be all that surprising that the subset of rational numbers generated by 0 and +1 forms a natural numbers object. What is suprising is that parametricity lets us show, once and for all, that there are no way to get out.)

Posted by: Neel Krishnaswami on January 12, 2013 11:32 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

Why does “ $\lambda \beta,i,f.refl$ ” inhabit the type $\forall \beta. \beta \to (\beta\to\beta) \to \mathbb{Q}\to\beta$ ? I can’t think of a function from $\mathbb{Q}$ to $\beta$ called “ $refl$ ”.

Posted by: Mike Shulman on January 13, 2013 5:27 AM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

This is a typo. The term should be

$pack(\mathbb{Q}, 0, +1, iter, (\lambda \alpha, i, f.\; refl), (\lambda \alpha, i, f, x.\;refl)$

Where $iter$ is the function defined here.

That is, there should be three components for zero, successor and iteration, and two for the equational proofs. The 5 numbered points list the properties that must be (and are) satisfied by each of the components.

(Sorry for the delay in my response; I had a deadline come up this weekend.)

Posted by: Neel Krishnaswami on January 15, 2013 2:05 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

(For those reading along, the link should be this.)

That “function” iter diverges on any input that isn’t a natural number! What kind of type theory are you using? You said something like “we need to use the fact that we only pass arguments in $Q$ to $iter$ to guarantee the termination of this function” which I gather is supposed to explain this. But in the relational model that I’m familiar with, the terms are terms in the underlying type theory with the additional property of preserving the relations. So if the underlying type theory is consistent, then your $iter$ isn’t well-defined there, and hence doesn’t either exist in the relational model.

Posted by: Mike Shulman on January 15, 2013 8:25 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

To be more precise, I intend $iter$ to be the function which diverges on any input which is not a rational number generated by 0 and +1 (the “subset” of natural numbers in $\mathbb{Q}$ ).

These lambda-terms is not drawn from a type theory at all; I’m using a realizability model. That is, I’m starting with an untyped version of the lambda calculus, and then defining types inductively as families of relations on the untyped terms. The type system itself only comes at the end, when you prove that every well-typed term is related to itself in the relational interpretation. This is basically the approach used to prove the consistency of implementations of extensional type theories like Nuprl.

As a result, $(iter, iter)$ is in the relational interpretation of $[\forall \beta.\; \beta \to (\beta \to \beta) \to \alpha \to \beta]\;(Q/\alpha)$ . This is a semantic (i.e., without a well-typed proof term) proof that $iter$ has the right behavior, and so serves as a justification for adding a type rule for it as an axiom to the type theory.

Adding axioms is of course a violation of type-theoretic hygiene, but as a first step I’m looking for models which support the kinds of properties I want – once I know that it’s possible, I can use it to guide the design of a suitable type theory.

Posted by: Neel Krishnaswami on January 17, 2013 12:35 PM | Permalink | Reply to this

Re: What Can Category Theory Do For Philosophy?

$MathML-enabled post (click for more details).$

Ah, okay. Did you say that earlier? Back in your original comment that started this discussion, you wrote

Existential types (aka weak sums) in System F do permit exactly this kind of data representation [emphasis added]

which led me to believe you were working in a type theory (such as System F).

I have to say it seems a bit dodgy to me to (1) consider the rational numbers as equipped with the subset of natural numbers, (2) require all operations to respect that subset, and furthermore (3) allow operations which are only defined on that subset, and then still somehow think of this object as “the rational numbers”. Really, it’s just the natural numbers, with some extra stuff hanging around that is explicitly ignored by everything. Isn’t it?

Posted by: Mike Shulman on January 18, 2013 2:46 PM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

December 6, 2012