aboutlogic #05 | Steve Awodey – Homotopy Type Theory, Logic & Philosophy

00:00:00: I'm not blaming the philosophers for that.

00:00:02: I'm just explaining sociologically why I don't spend much time on it.

00:00:08: But if I'm at a conference and having a glass of beer with somebody and they're interested, I'm glad to talk about it.

00:00:15: So we're having coffee now, but I'd be happy to talk more about it right now, too.

00:00:24: Welcome to About Logic.

00:00:26: And in this week's podcast, we have Steve Awade here, one of the fathers of homotopytheory.

00:00:32: And we will talk about the relations of philosophy and math, but also the main ideas between geometric thinking and logic and what all this has to do with computer science.

00:00:49: So welcome to the About Logic podcast.

00:00:53: Today we have Steve Audi from CMU, Carnegie Mellon University in Pittsburgh.

00:01:00: And I'm very happy.

00:01:01: And thank you very much, Steve, for agreeing.

00:01:05: I mean, we know each other for quite a while.

00:01:08: My pleasure.

00:01:09: It's

00:01:09: good to have you here.

00:01:12: So, how would you describe your interests?

00:01:17: I mean, I know you have written a book about category theory and you are very involved in this hot project.

00:01:25: So, how would you describe your, what drives you maybe?

00:01:32: Okay, well, thank you very much for... inviting me to this conversation.

00:01:36: Torsten and Dennis, nice to meet you.

00:01:41: I wasn't sure exactly what, I'm dodging your question for the moment and then I'll get back to it.

00:01:47: Then Torsten invited me to a podcast which he said was about logic and philosophy of mathematics maybe, something like that.

00:02:01: Initially I declined because I said I don't do philosophy anymore.

00:02:05: I'm not I'm.

00:02:06: I'm devoting all my time now to mathematics, so I don't know if I should say that For the public record here.

00:02:13: if my boss hears that maybe I'll suffer some repercussion, but but Torsten assured me that the discussion could be about anything we really want and that There's interest in all different topics and so on.

00:02:30: So maybe I start by saying that that's not to say that philosophy is off limits.

00:02:35: That's just to say that I no longer really spend a lot of time thinking about philosophy.

00:02:41: It's not what drives me.

00:02:43: I discovered at some point when I started doing hot that the mathematics takes up more of my energy and time and thought mental.

00:02:56: capacity, then the philosophy does.

00:03:01: And if I'm going to do a proper job of it, I need to make time for it and focus on it.

00:03:06: And so for the last, I'd say more than ten years or so, I've really been spending most of my time thinking about mathematics.

00:03:15: Just because I have a limited mental capacity, maybe I'm getting old or something like that and my brain is slowing down and I don't have time to think about philosophy anymore.

00:03:27: I would do it if I had infinitely much time.

00:03:31: but the mathematical problems somehow, it's not that I consider them more important or something like that, it's just they take more time and energy to do properly and so I don't have time left for everything.

00:03:45: So that's just as a preface.

00:03:48: So Like now, for example, last week I went to visit Jonathan Weinberger in Chapman University, and he's a new assistant professor in a program that's devoted to philosophy, physics, and mathematics.

00:04:06: And I give a talk that was a philosophy talk on maybe a motivation for hot coming from Fraga's early semantics.

00:04:18: of sense and reference and the morning star and the evening star and all that stuff that the philosophers like.

00:04:26: And I was trying to motivate hot by connecting up ideas from Martin Liff type theory and homotopy type theory with some of those old fashioned problems in the philosophy of language.

00:04:40: And I came away and I had some conversations with some philosophers there and I felt like, oh, this is fun after all.

00:04:47: Maybe I should do some more of this.

00:04:48: Maybe I should write this talk as a paper.

00:04:50: Maybe I should whatever.

00:04:54: And I resolved to maybe spend some more time on it.

00:04:58: And since I've left, it's been a week or a half.

00:05:01: Now I've been stuck on a problem involving a certain hyperdoctrine that turns out not to be a pie tribe.

00:05:08: And I find that much more fascinating.

00:05:10: And so I'm thinking a lot more about that.

00:05:13: It's a kind of mathematical semantics for homotopy type theory that was invented by Andrei Joyal.

00:05:19: And when I get given a choice between thinking about those two different problems, I find myself more fascinated by the latter, the mathematical one.

00:05:29: And that's just me, I guess.

00:05:30: It's just what I, you know, it's like, I know when you start doing formalizations, that's like a video game, you can't put it down.

00:05:40: And it's that kind of thing, the mathematics has a kind of compelling I don't know, fascination for me.

00:05:51: And the philosophy, I'm happy to talk about it.

00:05:55: And especially when somebody else is interested and engaged, then I'm interested in doing that.

00:06:01: But if you leave me alone, I'll start thinking about some mathematical problem, and then that'll be the end of that.

00:06:06: So that's to answer your question, Torsten, and maybe a long-winded answer.

00:06:10: But that's what I'm thinking about more.

00:06:13: Yeah, I'm thinking more about mathematical and specifically What I'm really interested in is mathematical descriptions of Martin Leuph type theory and homotopy type theory, which we can talk more about if you want.

00:06:30: It's a foundational system for constructive mathematics that is connected to homotopy theory and so on.

00:06:39: It also has a long history and philosophical aspects, but I'm interested in the mathematical semantics of that system.

00:06:46: And that's what I've been thinking about a lot lately.

00:06:50: But I wonder, is there such a clear demarcation between philosophy and mathematics?

00:06:57: And it seems to me that the sort of kind of mathematics you're thinking about is very much sort of influenced by, I would say, philosophical consideration.

00:07:10: I would like to sell it as philosophy.

00:07:12: If people would buy it in that package, I'd be happy to.

00:07:16: sell it to them.

00:07:18: And I think there's some legitimacy in that.

00:07:20: I mean, if you look at historically work in conceptually motivated mathematical logic, it has philosophical maybe motivations and implications and so on.

00:07:37: So the mathematical work too is a branch of exact philosophy.

00:07:43: Certainly there were historically philosophers who considered you know, mathematical logic to be an important part of philosophy.

00:07:56: And maybe that's a good way of reconciling my interest in pursuing mathematical semantics for homotopy type theory with philosophical motivations or whatever, is that it is philosophy.

00:08:15: I could just bang my fist on the table and say, it is philosophy.

00:08:20: Mathematical logic is a branch of philosophy.

00:08:24: I don't know if that's legit.

00:08:26: There's some remaining evidence of this culture in our conference system nowadays.

00:08:33: I mean, we put together logic and philosophy of mathematics into one track normally at philosophy conferences.

00:08:40: And I guess this is still from those times.

00:08:43: But nowadays, there's, of course, the problem that Mathematical logic is advancing and advancing.

00:08:50: And so the audience that can really understand the nuances and is interested in philosophy is not empty, but of course, a smaller cut than

00:09:00: safer.

00:09:02: And we see the same thing.

00:09:05: I agree with you.

00:09:06: And I see the same thing happening in the Association for Symbolic Logic.

00:09:10: Maybe that's an American association, but it has a European section, and it has a conference every year in the European Logic Colloquium and so on.

00:09:23: But if you look at the journal of the symbolic logic, most of the papers are mathematical, and then the papers that are more philosophical tend to go into the journal of whatever, the bulletin of symbolic logic or the review of symbolic logic.

00:09:42: I'm not speaking as an editor here, I'm just speaking from practice.

00:09:48: But so there is a split and at the meetings too, you know, sometimes there will be a philosophy section or something at one of the meetings, but there tends to be quite a split between the two.

00:10:02: But do you think it's important to explain these ideas?

00:10:07: I mean, mathematics sounds obvious, like we're going for more specialization and in the end nobody understands anymore what we're doing.

00:10:16: And isn't it important to, I mean, to explain, especially, I mean, you mentioned homo toky type theory.

00:10:24: And this, I mean, I think this, in my view, the name is maybe a bit misleading because it's just sort of the penultimate type theory.

00:10:38: And this is a very important discovery.

00:10:41: So shouldn't we work to spread?

00:10:44: Because there seem to be still many people not realizing this sort of fundamental revolution.

00:10:52: And you're very instrumental in bringing it along.

00:10:56: So I'm a bit sad by what you're saying.

00:10:59: It seemed to be given up on this very important aspect, at least.

00:11:06: Well, thanks for saying so.

00:11:07: I appreciate that.

00:11:09: I agree with you that it's an important advance in foundations of mathematics and logic and it has or should have, let me put it this way, it has a great deal of importance for philosophy too and it should have a large impact on philosophy of mathematics.

00:11:32: but I'm afraid that it hasn't and maybe I'm just too impatient.

00:11:36: I wrote a couple of papers even one, I started when we were at the Institute together, Torsten, I realized that the, I mean, it took a long time to really digest and metabolize univalence.

00:11:52: Yes.

00:11:53: Because it was, at first, it was so surprising and shocking and mysterious.

00:11:59: But as I came to understood it, I realized how important it was also for topics that philosophers care about.

00:12:06: And so I did try to reach out to the philosophers and I wrote a couple of papers and I gave a couple of talks.

00:12:12: But then it really didn't go anywhere and nobody didn't get much of a reception.

00:12:17: And so I didn't pursue that.

00:12:20: And maybe it's just being impatient or maybe it's moving on to other topics that I was more interested in.

00:12:28: I mean, one thing is you know if you try different things and one thing gets a good reception and another thing doesn't then you pursue the thing that's getting a good reception.

00:12:37: and what was working for me was the connections to homotopy theory and so I spent a lot of time working on working out the Stuff learning Quillen model categories proving stuff like that whereas the philosophical papers about the structure identity principle and the connection between Univalence and Invariance and structuralism Which is something the philosophers are very interested in I think they still write papers about it.

00:13:05: that didn't go anywhere and nobody read those papers and nobody You know invited me to come for a seminar or whatever.

00:13:13: I tried to talk to people about it and Didn't really go anywhere.

00:13:16: So I'm not blaming the philosophers for that.

00:13:19: I'm just explaining Sociologically why I don't spend much time on it.

00:13:25: But you know if somebody if I'm at a conference and having a glass of beer with somebody and they're interested I'm glad to talk about it.

00:13:32: So I'm.

00:13:33: we're having coffee now, but I'd be happy to talk more about it right now, too.

00:13:38: I see a great and as you suggested towards a deep connection between Univalence and the idea of invariance and structuralism in the philosophy of mathematics and that's I should say.

00:13:53: I've been interested in structuralism and philosophy of mathematics and so on from way back.

00:13:59: I wrote papers about category theory and structuralism and things like that when I was a grad student even and so the Univalence I think is a breakthrough in that respect.

00:14:11: and let me just say That's not my idea.

00:14:14: Univalence is Voivotsky's idea.

00:14:16: My idea was the homotopical interpretation of type theory, which makes Univalence possible.

00:14:22: But Voivotsky certainly is the one who came up with Univalence.

00:14:26: I don't want to suggest I'm taking any credit for that.

00:14:29: But it's a beautiful idea, and it has a big, I think, importance for philosophy.

00:14:38: For the audience, can you just summarize what Univalence is, if you don't mind?

00:14:42: Oh, sure.

00:14:43: Oh, sure.

00:14:44: So in everyday old-fashioned, Frager, Russell, Girdle, Carnop.

00:14:53: I should do the other order.

00:14:54: Frager, Russell, Carnop, Girdle.

00:14:57: Predicate logic.

00:15:00: There is an identity relation, as we know from the history of logic going way back.

00:15:07: Identity is a logical relation, but it's kind of trivial in that predicate logic that the students learn and that we all learned maybe as undergraduates.

00:15:18: Because either, if you give me two mathematical objects, either they're equal or they're not, and that's the end of the story.

00:15:26: But as Frege observed in the introduction to the Grif Schrift, there are deep problems that follow from the relation of equality.

00:15:36: And if you pursue that line of thought, what you see is equality is a much more subtle relation from a mathematical and logical point of view than we at first observe.

00:15:52: And one of the ideas coming from, well, let's go back a little bit to Martin-Lev type theory, is that the equality, or as Martin-Lev calls it, identity relation can be proof relevant.

00:16:09: The idea of proof relevance is a type theorist's way of saying that a relation is more than just honor off yes or no, it has some content.

00:16:23: It can have content.

00:16:25: Some relations don't have any content, but some do.

00:16:28: And one way of cashing that out is to say, well, you look at the meaning of the relation is all of the proofs of that relation.

00:16:36: That's a proof theoretic way of describing what's going on there.

00:16:41: But there are other ways of describing it too.

00:16:43: Paramartin Lyft thought of it as proof relevance.

00:16:47: So the meaning maybe of a proposition is the collection of all of its proofs.

00:16:54: That would be the propositions as types idea.

00:16:58: But in homotopy type theory, we have a refinement maybe of the propositions as types conception where every type has not only its own identity relation, which is not only yes or no, but a whole collection of proofs of identity, but an even richer structure.

00:17:23: And the richer structure comes from the fact that the identity relation, if you take seriously the idea that it's proof relevant, then there's an identity relation on identity proofs.

00:17:35: And that's proof relevant too, right?

00:17:39: And so For example, you might have a proof that two things are are Equal or identical and then you might have another one and they might be identical or not and If they are identical there might be other ways in which they can be identical.

00:17:56: and that structure Leads to a hierarchy or we say a tower of identity types which have a very rich structure.

00:18:04: for example reflexivity of identity, which we all know well.

00:18:08: Everything is equal to itself, as Frege already observed and Aristotle I'm sure.

00:18:15: The reflexivity of identity leads to an identity path on every object.

00:18:21: Now I'm using the homotopical term in that.

00:18:24: terminology.

00:18:25: And two identities compose, that's a transitivity of identity.

00:18:30: And identity is symmetric, so you can reverse an identity.

00:18:34: And this structure, it turns out, is the same as, or at least can be described as, the structure that occurs in a topological space if you look at the continuous paths between points of the space.

00:18:51: And that structure, which was discovered already by Ponca Ray and called a fundamental group of a space at a point.

00:19:00: If you look at all the continuous paths at a point, that forms a group.

00:19:06: That actually has a higher dimensional structure where you look at deformations, continuous deformations of the continuous paths as higher paths between the paths.

00:19:17: And those are like the higher identities between the identities.

00:19:21: And this structure is a what the homotopy theorist calls an infinity groupoid.

00:19:27: It's a category in which every arrow is invertible, but the category structure and the inversion structure only holds up to a higher dimension of structure, which itself is an infinity groupoid, and so on.

00:19:41: So this notion was introduced by Groton Dieck, the celebrated famous mathematician, maybe the greatest mathematician of the twentieth century, I don't know.

00:19:50: Those kinds of things are easy to throw around.

00:19:53: But he introduced this idea of an infinity groupoid as a way of classifying homotopy types of topological spaces.

00:20:01: Those are the idea of a space up to, regarded up to continuous deformation.

00:20:10: So this is a mathematical idea that has occurred naturally in the world, right?

00:20:18: Homotopy types of spaces and continuous deformations.

00:20:21: And then it pops up in infinite-dimensional algebra in the form of an infinity groupoid.

00:20:28: and now what we discovered is this happens in Martin-Liff's intentional type theory.

00:20:33: These infinity groupoids occur in the type theory.

00:20:37: We don't put them in.

00:20:39: We don't add any axioms.

00:20:41: We discovered that they're there.

00:20:43: So this is an amazing Coincidence of ideas.

00:20:46: it's one of those kinds of coincidences of ideas that doesn't happen very often and when it does happen you should take note I think and the philosophers could take note of this amazing occurrence that these infinity group oids occur in the foundations deep in the foundations of mathematics and that's the kind of connection between foundations and type theory and homotopy theory.

00:21:16: So, sorry,

00:21:17: go ahead.

00:21:17: To emphasize this, there's a connection between what one could call very abstract geometry, right?

00:21:25: I mean, the theory of spaces.

00:21:27: And type theory, which is something like very discreet in the sense of, I mean, people you learn about sets, but I mean, okay, we use types and there are some subtle differences.

00:21:37: But basically, these are very structures which are on the basis of mathematics.

00:21:42: And if you look at them, no close enough, then it emerges that this relation to homotopytheism, to abstract geometry exists.

00:21:53: I find this already absolutely, I mean, fascinating.

00:21:59: Yeah, I agree.

00:22:01: This fact, yeah.

00:22:02: Yeah, it's quite fascinating, I agree.

00:22:04: And maybe it should urge us to revise our idea about the foundations of mathematics being in the discrete, where we have this idea that maybe mathematics should be built up from elements and discrete bits and computation with finite sets and the arithmetic of the numbers is closely tied and that's the basis of mathematics.

00:22:35: But there's another kind of mathematics which deals with maybe continuous deformation and transformation in space and time and as you said geometry abstract geometry and it turns out maybe through this connection in type theory that we can get a glimpse of a way of understanding the fundamentals of mathematics in a more continuous way or a more spatial topological way.

00:23:07: that's not discrete.

00:23:08: I mean, there has always been in the history of mathematics this kind of tension or duality between the discrete and the continuous.

00:23:17: But in foundations, we usually fall on the side of the discrete, as you already said.

00:23:23: But it seems that there's also a continuous or geometric side of foundations that maybe has been overlooked.

00:23:32: and which now we can see coming up in this type theory that the basic types of type theory are not discrete sets.

00:23:44: They have an integrity as a continuous objects or mathematical objects which can be deformed, which can change, which can be stretched, and which have an internal structure which can be infinitely complex.

00:24:02: It's not just a discrete set of points.

00:24:05: There's a great quote from Frege.

00:24:08: I wish I could find it, but I'll just paraphrase it, and you can splice it in later if you want.

00:24:17: It's from the conclusion of the preface, or maybe the introduction to the Begrift Schrift, where Frege says, I believe that my grief shift will be of great use in those areas where precision in the proofs is of the greatest importance, for example, in the differential and integral calculus.

00:24:43: And indeed, we could imagine adding a concept with some geometric content.

00:24:55: to the Begrift Schrift and that would allow us to reason also about geometric objects in a similarly precise way and it would imbue the system with a geometric meaning.

00:25:10: And I think that's so close to what we are actually doing.

00:25:15: is we take the existing system of the Begrift Schrift which is a kind of logical system, and we add a little bit of geometric content at one point, but because the system is this tightly interconnected network of concepts, the geometric content flows through the entire system, and now it becomes a system for reasoning about geometric objects as well.

00:25:41: So it's very much, I think, in the spirit of Frege's conception there of what he was doing.

00:25:49: May I?

00:25:50: Yeah, please.

00:25:52: So maybe just one short question.

00:25:53: There is a lovely story how the discrete pops out of the continuous and maybe it's something.

00:25:59: Yeah.

00:26:01: I'm not sure whether I'm up to date, but the version I know still goes with the circle.

00:26:06: Yeah.

00:26:06: Still how you get the discrete out.

00:26:08: Would you like to tell our audience?

00:26:15: Well, I mean, in how

00:26:18: do we get arithmetic so to speak?

00:26:21: Yeah, in type theory there are, one can identify properties of types which are describable within the theory and one can reason about a type having a structure of a certain Level or a certain kind.

00:26:44: and there are some types which are merely propositions there yes or no.

00:26:49: and there are other types which are essentially discrete their sets of discrete points up to Homotopy and then there are other types that are group oids.

00:27:00: they have paths which are non-trivial and so on up.

00:27:03: There's a whole hierarchy of such types all the way up to types which don't have which have an infinite structure.

00:27:14: And so the discrete is a definable characteristic of some types which occur in type theory.

00:27:24: So you don't have to construct a discrete thing out of continuous things, but you can identify which things you have that you have constructed are discrete.

00:27:33: And one of the basic ways of getting discrete things is by an induction starting from some discrete things like the natural numbers are usually defined in type theory as an inductive type generated by a starting point and then a operation.

00:27:53: and if you take the free thing or the inductive thing generated by that that's the logician or the logic.

00:28:01: students will be familiar with piano's description of the natural numbers.

00:28:05: if you do that construction in type theory you will obtain something which is essentially discrete in the sense that I was just mentioning.

00:28:13: It will be a set of points, essentially.

00:28:18: So the discrete arises naturally within type theory.

00:28:23: It's just that not everything that arises is discrete.

00:28:27: For example, the universe of all types is not discrete.

00:28:31: That's maybe the most basic example of something that's not a zero type in the previous sense, in the sense of being discreet, because a type itself may have some structure, it may have some automorphisms, and so the universe of all types will contain points that have automorphisms.

00:28:51: And that just, it just is in the nature of things.

00:28:57: Yeah.

00:28:59: I'd like to tell a story, which So, I mean, Martin Hofmann was a good friend of mine, and he and Thomas Streicher, they were also thinking about types theory.

00:29:17: And in particular, exactly about this question is the equality type discrete, right?

00:29:22: Which I think Martin Lüft did not really answer.

00:29:27: I mean, I think he thought... given his laws equality type would be discreet.

00:29:33: And it was Martin and Thomas who proved the contrary using the group reading model.

00:29:40: And the group reading model shows that, as you say, that the type theory is not, that you can actually not prove that equality is discreet, that Martin left open this door.

00:29:56: to the type theory we have now.

00:29:58: But I don't think he was doing this intentionally.

00:30:00: I think it's an over-interpretation.

00:30:02: I think he was just doing it basically by accident.

00:30:04: I

00:30:05: think that's right.

00:30:06: I think that's a good point, yeah.

00:30:08: Yeah, but then we went together and we discussed this and we realized that the group we model still has got one level higher discrete structure.

00:30:19: So it's not really a very principled approach, but it's very sort of cut off here.

00:30:25: And we thought, oh, we should go to have infinity group weights.

00:30:29: And we started on a whiteboard writing down laws of infinity group weights.

00:30:34: And very quickly, it was absolutely impossible.

00:30:37: I mean, we tried to do this algebraically, which is the killer.

00:30:43: And we thought, OK, OK, forget about this, forget about this.

00:30:46: And years later, when Vladimir Borodsky started to post on the cockmailing list.

00:30:53: He posted a paper about the homotopy lambda calculus, and I didn't understand the word.

00:30:58: But I thought I wanted to find out more about this.

00:31:01: So I sent him an email and said, is this maybe what you're doing?

00:31:04: Is this maybe related to the group read model?

00:31:07: And he went back and says, yeah, actually, infinity group reads.

00:31:12: And I realized that he, because he comes from homotopy theory, For him, an infinity groupoid is a very natural structure.

00:31:22: There is a very straightforward description from this geometric perspective.

00:31:26: So in a way, I would say these things, they are not this or that, but here's our intuition, which intuition works better and the sort of algebraic approach, the sort of discrete approach.

00:31:42: We were not able to actually understand what an infinity groupoid is.

00:31:46: is, but because of Włowocki coming from it, had a different background, had this super ability to do this.

00:31:59: And I think this is an important combination in a way to combine these views.

00:32:08: Yeah,

00:32:09: yeah, that's a really good account of the.

00:32:16: The background of these ideas I think pair originally as you said left the possibility open that the identity types are not just discrete.

00:32:27: he in fact in one of his early systems he Declared them to be discrete and then he later realized that spoils the computational uses of the system and it also violates his philosophical scruples that motivated the system.

00:32:43: and so he dropped that condition and went back to the identity type which he did have a kind of let's say philosophical motivation for.

00:32:52: but he didn't really understand it because it was not evidently discreet and so it was hard to understand and the type theorists had difficulty comprehending what was happening there.

00:33:06: And it wasn't until the groupoid that we model that we realized that something subtle and interesting was going on.

00:33:15: It made sense, finally, of the non-discreet character of the identity types.

00:33:21: But then, as you said, we quickly realized, because every type has an identity type, that the identity type has an identity type and that's not discreet either.

00:33:32: Yeah, it shouldn't be.

00:33:33: Yeah, and if you know a little bit of mathematics or algebraic topology or category theory, then you say, oh, infinity groupoid.

00:33:40: Maybe it's an infinity groupoid.

00:33:42: But once you start to try to do it, it's hard.

00:33:45: And we tried to do it as well.

00:33:49: It's around CMU.

00:33:50: This was before Vladimir.

00:33:52: And we did manage to prove that every type is a globular infinity groupoid, which is one of the definitions of infinity groupoid, not the homotopical one, but a weak algebraic one.

00:34:05: And that was Peter Lumsdain's dissertation.

00:34:07: And then after that, we got in touch with Vladimir because we heard about his lectures at Stanford on the homotopy lambda calculus and so on.

00:34:16: And we invited him to visit and he came and visited.

00:34:18: I remember I picked him up at the hotel and the first thing He asked me, so what are your students?

00:34:26: What are you doing?

00:34:27: What have you been talking about?

00:34:29: And I said, well, we have this proof that every type is a weak infinity groupoid.

00:34:33: And he couldn't believe it.

00:34:34: He stopped.

00:34:34: He said, you have a proof of it?

00:34:37: Because for him, it was just an analogy, an intuition.

00:34:42: An intuition.

00:34:43: And I said, yeah, we've got a proof.

00:34:45: We prove that every type gives rise to a weak infinity groupoid.

00:34:48: And he was really, I think, excited.

00:34:52: excited about that idea because it confirmed his intuition of what was happening in the type theory.

00:34:58: So yeah, that was a really important breakthrough, but maybe we're kind of getting toward the end, I guess.

00:35:08: Maybe we should go on to Univalence.

00:35:11: as much as I like this idea of the homotopy theory and the interpretation of identity types as spaces and Infinity group oids, and according to Groten Dieck, those are just homotopy types of spaces.

00:35:27: There's still this breakthrough then that came from Vladimir after that, which was the Univalence idea.

00:35:35: And I think that's a really profound thing that the philosophers might be able to take an interest in, interest in.

00:35:43: So I can describe it kind of... Briefly, now that we've talked about infinity group voids and the fact that every identity, that every type has its tower of identity types, and that's an infinity group void, and it makes the type into a kind of infinite dimensional structure, we can ask about specific types, like, what about the type of all functions from one type to another?

00:36:13: that has an identity type too.

00:36:15: What is an identity between two functions?

00:36:18: And there we can kind of unpack that structure in terms of the the domain and range of the function.

00:36:27: We say if it takes identical elements to identical elements then well every function does that.

00:36:35: but if two functions blah blah blah.

00:36:37: So we can unpack the identity type on the function space.

00:36:43: What about the universe?

00:36:45: That's something in type theory.

00:36:46: What's the identity type on the universe?

00:36:49: Can we unpack that in terms of the types in the universe?

00:36:53: Well, in type theory, in Martin Love type theory, there's no such description.

00:37:00: The identity type is a primitive structure.

00:37:03: So all we know about it is it's an infinity groupoid.

00:37:07: We can prove that about the type theory.

00:37:09: But if the type that we're interested in is a universe of types, so it itself contains as terms types, then there's another possible description of a relation on those types.

00:37:26: And that's the equivalence of types.

00:37:29: That's a definable structure on the universe is equivalence of types.

00:37:34: Two types are equivalent.

00:37:39: in the sense of homotopy theory, if you can map back and forth and the composites of the maps in each case is homotopic to the identity on that type.

00:37:52: So it's like isomorphism of two objects.

00:37:55: Everybody knows what an isomorphism is between two sets.

00:37:59: But this is a generalization which replaces the identity relation on the sets by, well, Homotopy which is given by the identity types.

00:38:11: in the system, right?

00:38:13: The identity types are interpreted as paths or homotopies.

00:38:17: So it's it's the very natural internalization of the notion of isomorphism is equivalence of types.

00:38:25: and now if you have a universe and the objects in the universe are types then there Then a very natural relation on the universe is isomorphism of types or equivalence of types.

00:38:39: And what the Univalence Axiom says is that notion of equivalence of types agrees with the identity type on the universe.

00:38:47: So there's a kind of a priori first choice of what should be the right notion of identity for two types, and it's this generalization of isomorphism, its equivalence of types.

00:39:04: And what the Univalence principle or axiom or condition says is that's the right notion that is the identity type on the universe.

00:39:16: If you take

00:39:18: two

00:39:19: types and you take their Cartesian product, you might think the natural notion of identity on the Cartesian product is just pairs of identities.

00:39:29: If you take the notion of a universe and you say what's the natural notion of identity, the first, if you think about it, For a few minutes the first thing you'll come up with is well, it should be isomorphism.

00:39:39: Well in type three isomorphism is equivalence of types and that's what the Univalence axiom says is the natural notion of identity is the identity type and it has amazing consequences, but but it's not it's not Mind bending.

00:39:59: once you bend your mind into that place then it's the obvious thing.

00:40:06: I would go further.

00:40:07: I think it's the only choice.

00:40:12: For a number of reasons.

00:40:13: I mean, can you define another relation on types which behaves like an equality?

00:40:19: No, you can't.

00:40:21: And also, I would also now quote this Leibniz principle.

00:40:27: If you have two types and a type theory, unlike set theory, you cannot distinguish objects by their elements, because the element always belongs to a type.

00:40:40: So you cannot say, oh, the empty set is an element of this type, but it's not an element of this type, because you cannot talk about the empty set in isolation.

00:40:49: And because of this structural principle of type theory, you cannot distinguish isomorphic structures or isomorphic types.

00:40:58: Absolutely.

00:40:59: And by like that, the equality of indiscernible, they have to be equal.

00:41:06: So I would go further.

00:41:07: That's not just the natural choice of equality.

00:41:11: It's the only possible

00:41:12: choice.

00:41:12: It's the only choice.

00:41:13: Yeah.

00:41:14: But

00:41:14: for structuralist theory,

00:41:16: it's absolutely structuralism.

00:41:19: And there's

00:41:20: the big philosophical

00:41:23: moment.

00:41:23: It's absolutely structuralism.

00:41:25: It tells you that two types, which are isomorphic, are the same.

00:41:30: For all practical purposes in the sense of they have all the same properties, they satisfy all the same conditions.

00:41:37: And moreover, even richer than properties, they have all the same structures.

00:41:41: Any structure on one is also a structure on the other.

00:41:45: It's equal as morning star and evening star.

00:41:48: Exactly, yeah, exactly.

00:41:51: Let me tell you one little story with linguists.

00:41:55: We worked on equivalents of stories and we asked people about their opinion.

00:42:00: and of course epistemology and ontology are different things.

00:42:04: But there some people insisted that if you change the color of the cape of the little girl who goes into the woods, then it's a new story.

00:42:14: It's structurally very equivalent and we hope that people would say Romeo and Juliet and Avatar, that's the same story.

00:42:23: But people didn't agree.

00:42:26: I mean, of course, they were untrained, they were not mathematicians.

00:42:29: But there are different competing intuitions there.

00:42:32: So maybe the color of the cape is essential.

00:42:36: But whether this is maybe just an anecdote, not a proper contribution to the philosophy of math.

00:42:43: Yeah, that's a good point.

00:42:49: I don't want to stop anything if you want to develop it further.

00:42:52: But for me, one point we haven't talked so much about is logic is often claimed to be like the isolated case within the math community and sad theory.

00:43:02: It's sometimes said they aren't that linked to other fields of math in comparison to topology.

00:43:08: And I mean, your story is one of connecting worlds in very different sense, right?

00:43:13: We have this Deep results now in topology, biological methods you mentioned.

00:43:19: Have we connected people like the homotopy theorists with the logicians?

00:43:24: Is there a chance that we find a few moments to talk about that, how this viewpoint can create new math for the mathematician?

00:43:33: It's true that current logic is quite separate from much other mathematical research, but I think you can say the same thing about any area of mathematics.

00:43:48: That's just the nature of mathematics nowadays.

00:43:51: But what is exciting is when one finds a connection between one area and another, and that's something that has happened with homotopy type theories, we did find a connection between logic and topology and geometry and homotopy theory, which seems to be quite robust and that makes it interesting from a mathematical point of view and I guess from a philosophical point of view too is what we've been arguing that it should or discussing that it should be of interest to philosophers who like to study conceptual connections between different areas of mathematics or different areas of science and so forth.

00:44:37: I mean people who do history of mathematics are very interested in the development of the calculus in connection with physics and applications in physics.

00:44:47: So that's the sort of phenomenon that we have here.

00:44:50: Instead of looking at the connection between the differential calculus and the development of Riemannian geometry and the theory of manifolds and spacetime and so on, here we have a connection between mathematical logic and the foundations of mathematics and the theory of homotopy theory and the development of abstract homotopy theory and so on.

00:45:20: So from that kind of sociological point of view, I think it's quite fascinating, there's one of these instances where a bridge is found between two different areas of science or mathematics and ideas flow back and forth.

00:45:37: And then from a sociological point of view, one can look at what's happening and how the two fields interact and how ideas influence each other.

00:45:49: I don't know about a deeper, more explicitly philosophical point about the nature of mathematical objects or something like that.

00:46:00: I don't want to get into that.

00:46:03: just motivation for the Langlands program.

00:46:04: Yeah, I mean,

00:46:09: I mean, something

00:46:10: maybe.

00:46:11: So

00:46:11: what you what you just, what you didn't actually mention is our is the sort of synthetic use of our true homotopy type theory, right?

00:46:21: I mean, to, I mean, As we know, there are structures which are interesting for a mathematical point of view.

00:46:30: They are very popular as the infinity categories.

00:46:34: And they are very, very difficult to describe, analytical, in the language of set theory, almost impossible, basically.

00:46:42: And one idea, one sort of application of type theory is to use the language of type theory to synthetically talk about higher categories and that seems to be very attractive to non-logicians, right?

00:46:57: I mean, it's an implication of type theory outside of logic, right?

00:47:01: Yeah, I like that idea.

00:47:02: That's a good point.

00:47:03: Thank you, Torsten, for bringing that up.

00:47:06: There's a new kind of... Maybe one of the people who's urged this point is Emily Reel and you can look her up and find talks about her talking about infinity categories and infinite-dimensional mathematics and so forth being difficult to capture in traditional foundations of mathematics, but type theory and in particular homotopy type theory and related systems of type theory provide a way of dealing precisely with these kinds of infinity mathematics and that's quite a I think should be useful and exciting for mathematicians who are not just or not only logicians or type theorists, but who are interested in these higher, higher dimensional mathematical structures as well.

00:47:59: The type theory provides a way of reasoning rigorously and even formally using a computer about such infinite dimensional structures.

00:48:11: That's a good point, yeah.

00:48:12: which come up in physics, right, in quantum field theory.

00:48:16: If you listen to O. Schreiber...

00:48:18: I guess, yeah, I don't know anything

00:48:19: about... In quantum gravity, or what?

00:48:21: I don't know anything about that, but I

00:48:22: think... Or we'll have him at the podcast as well.

00:48:25: Oh, good idea, yeah, have Ours.

00:48:27: He'll tell you all about that, yeah.

00:48:30: And Emily Eriel, we should also...

00:48:32: Should have Emily too, yeah.

00:48:34: She has a lot to say about that.

00:48:35: Yeah,

00:48:37: there's so much more to ask about the sociology and the advanced institute of Princeton, how to write a book collaboratively about the other models, what's our cubicle types.

00:48:48: I mean, if you have the time, maybe we should have another episode.

00:48:52: Some other time, yeah.

00:48:55: I guess we should come to an end.

00:48:58: Yeah.

00:48:58: So

00:49:02: thank you so much.

00:49:02: It was super interesting.

00:49:04: Well, thank you for your interest.

00:49:06: Thank you for your interest.

00:49:07: And it was a pleasure talking to both of you.

00:49:10: I mean, just a very tiny remark.

00:49:13: I mean, it's you might need to wait longer.

00:49:16: But when I was a student, I found this hot, so interesting that it was like the starting point of my first edited volume.

00:49:23: This is where I met Thorsten reflections on the foundations of mathematics, where we compared set theory with other approaches.

00:49:34: And so I think you influenced many people, and it will take a while

00:49:39: before we

00:49:40: get tenure.

00:49:42: I mean, the first ones already got, right?

00:49:44: There was a huge amount of projects, so many postdocs in the area, and a lot of them found permanent positions now.

00:49:52: So I don't think it's over yet.

00:49:55: I think we've got a foothold or toehold in the scientific community.

00:50:04: I'll plug a book too.

00:50:05: I don't have it here.

00:50:05: I wish I could show the book.

00:50:07: Yeah, but I would like to plug

00:50:08: a

00:50:09: plug a book and that's Egbert Reich as new Introduction to homotopy type theory, which has just been published by Cambridge University Press.

00:50:18: I got one in the mail because I gave a blurb to put on the back cover.

00:50:23: So they sent me one for free.

00:50:25: So and I just saw it.

00:50:26: It's just beautiful.

00:50:27: I'm very happy and any students who are interested in learning homotopy type theory.

00:50:32: Of course, the Hot Book is the Bible of homotopy type theory, but Egbert Reica's book is a textbook for homotopy type theory from which you can actually learn it.

00:50:42: So go ahead and look at that.

00:50:44: I think it's even free online, but anyway, go ahead and buy it.

00:50:48: Egbert could use the money.

00:50:49: Yeah,

00:50:49: it's better if Egbert deserves the money, certainly.

00:50:53: Yeah.

00:50:54: And I mean, it contains more things, right?

00:50:55: The Hot Book.

00:50:56: is maybe even outdated for such a fast

00:51:00: way.

00:51:00: I wouldn't go that far, but

00:51:02: maybe it doesn't feature all of the newer developments.

00:51:05: Maybe that's a

00:51:06: good

00:51:07: way to put it.

00:51:10: Okay.

00:51:10: And again, thank you.

00:51:12: Thank you.

00:51:12: Thanks very much.

00:51:14: And you all should subscribe now and comment and do whatever these algorithms want to see, even if Torsten studies algorithms.

00:51:23: I guess it's fair to say that.

00:51:25: No,

00:51:27: the YouTube algorithm has its own rules and I guess our audience knows that better than we do.

00:51:32: So thanks for tuning in.