aboutlogic #24 | Why Didn't Homotopy Type Theory Take Over the World?

So why didn't homotopytypes take over the world? Why not yet if maybe you're just hosting. Be patient! Hello, yes welcome to the latest installment of About Logic. very happy to have Ulrich Buchholz here today who's actually a colleague at Nottingham and I know him quite along time And i think he is a good person To talk about philosophy of logic.

But I leave it to Dennis, who asks the first question. Yeah sure i'm happy to do so. and yeah a lot of appraisal from the beginning. you're doing so much And You are one of these mathematicians Who Are for me philosophers even if they might disagree or computer scientist by affiliation. So let Me invite you.

um you strived A couple Of topics right. your master was in topology? Then he went To stanford Doing working with one of the greats, with Heffermann on constructive themes and prove theory hot. Could you give us like a rough idea? how are these topics connected? or is it just I finished this thing now something completely new?

Oh yes thank you very much for having me. yeah so i have been interested in mathematics uh for long time and studied mathematics as thought i would be an algebraic topologist when i was in Copenhagen. I got the scholarship to go to Stanford for my PhD and started working with a topologist there. And had a little bit of crisis or faith thinking, well what does it all mean?

There are lots things you have take on faith. You don't no longer study everything from basic steps upwards and cross all tees and dot all eyes use black boxes get into frontier very quickly. Well, actually what does it all mean? I would like to study some foundations as well. And i had become aware of proof-assistance at the time.

that was playing around with rock and... ...I just heard a little bit about this. beginnings have some homotopy type theory wasn't quite called out at the times but.. ..i'd seen maybe an early blog post by Vladimir Ravotsky. So changed advisors to Solverferman And I basically said, I would like to learn everything there is about foundations of mathematics.

How things hang together? Or how do we trust proofs? What are these different foundational systems doing?". He gave me a problem in ordinal analysis and proof theory. that's what I worked on for my thesis but it was unfolding program. maybe you can come back. Related questions, predictivity and constructivity.

What rests on what? as modified Hilbert program these sorts of things? But I had this...I always liked topology And then when I was at Stanford Then homotopy type theory really became a field. This is great now! Now i know both logic and Homotopy Theory. So this Is what Im going to do. There are many questions about Open Questions About Homotopy Type Theory.

Some Of Them Are Still Open. Like, what is the expressive limits of homotopy type theory? How does it fit together with the mathematics we used to do in set theory. What kinds of foundational systems are there for a homotopy type theory? so I've been working on areas related to that but also more technical about... ...what does it mean if you have homotopic types as your basic ingredients and foundations?

And then trying to get at this expressivity question, what is it actually? What are the limits of what you can do in univalent foundations and homotopy type theory. So maybe let's stay slightly chronologically as your suggested for our audience who have only heard one guest doing proof theories so far.

Where does he? idea of ordinal analysis was like the main goals there? Right! It goes back I guess to Genson proof of consistency, of piano arithmetic using induction in primitive recursive arithmetic up to an ordinal epsilon naught. So it's related to Hilbert's program. so probably you've talked a little bit about Hilbert' s program.

the idea is try and secure ideal mathematics through concrete mathematics or computational finitistic If we not strictly finitist, but we allow some constructive methods. Can we secure classical ideal method via constructive methods? Maybe using some infinitary constructive principles. for instance wealth will founded recursion and induction up to some ordinal or other well-founded structure.

And that's exactly what you then do. An ordinal is an extensional, transitive well-founded order. So it's something like you start with the natural numbers as ordinal number. so we have first zero one two and so on And then gather all of them up. You still have something that isn't ordered. sequence from zero to omega now?

Now you can keep counting if one more Omega plus One Omega Plus Two and Then you have Omega plus Omega which be in ordinal arithmetic, well omega times two and not two times omega because two times Omega would just be omega again. We should have a premise on ordinal and cardinal arithmetics. Yes Could you say it's the generalization of like the natural numbers to include infinite numbers?

Right but order is important here. Yeah its orders are distinct from cardinality Exactly. And then these ordnance you can keep going and make more complicated. It's a way of playing the game, name it largest number for professional mathematicians. The interesting thing is when you go down to order your always stop after finding that amount... That right!

If pick as decreasing sequence eventually give up reach at bottom Right. So we have these complicated ordinals and can use them to measure the strength, that logical strength or consistency of foundational systems for mathematics. And then this strengths are themselves well-ordered. It looks like at least further natural system.

That's another open question. We could come up with artificial systems But most of the ones we come up with naturally are assigned such an ordinal and there different ways of assigning an ordnance to a system, they all agree. And then systems become well-ordered by consistency strength. Okay? You went on this order... I mean now you mentioned epsilon zero as like.

where was your work living? is it Now, just constructive ones or? Not quite the largest one. So after Piano Ritz-Muzik there's. you can take a little bit of step into impredicativity. You can go up that we could talk about predicativity A bit. so Vefermann is One Of The Names Associated To This. Veferman Schütte Ordinal Which Is One Analysis Of Predictivity According to Suggested by Kaiser And That's Gamma Naught.

And that's also the ordinal of predicative type theory, basic margin of predictive type theory with a hierarchy of universes. So it is sort of an natural closing point for predicative mathematics. but you can take some small steps into in predictivity not just going to full hark of propositional resizing or power sets and so on.

But allow maybe one generalized inductive definition. What words? Can we explain the word predicate versus impredicate? Yeah. Thorsten is really in his... This will be a rigorous episode, we will not go to higher categories! We really need this one. So yeah? No no..this could be whole episode. going back to Frank Herré and Havanweil There are two ideas which I think related but not quite the same.

One is the vicious circle principle that you should not define a mathematical entity by reference to collection of it itself as member. so box-off Russell's paradox and stuff like that. In Russell's Paradox, you're defining a set by reference to quantification over the collection of all sets And one diagnosis of that inconsistency is.

well You should not do anything like that. so this avoid the vicious circle principle. and Slightly different idea I think maybe more due to him and vile Is this idea? That some mathematical collections are open ended. We can keep adding to them. One of them might be the power set of their natural numbers.

because how do we talk about subsets? We talked about them via their propositional functions, the predicates. And you can always extend a language and come up with new predicates. so maybe the collection of subsets or natural numbers is an open-ended unbounded collections sort of idea potential infinity but not at that level in natural number some higher levels Different foundation systems from these two points of view avoiding vicious circles and having invariance under Extending the domain of discourse with this open-ended conditions.

You want to have statements that are stable? Under adding new elements. That's there, that's how man vials. idea of Predictivity. so to me always I mean okay. There is just two notions off predicative right. one form proof theory And then the one in type theory. Okay, so coming back to what I was looking at.

So in type theory we have generalized inductive definitions where you might have a quantifier over previously defined inductive set. A basic example is the Broward trees. Three constructors, you have this zero tree. You can add a new root below the trees or just get a successor tree. but it could also take an accountably branching family of trees and put in your route under all them.

so I'm gesturing even which is what we see on video not here at the audience because imagine if they had a countable collection with these well-founded trees. then there's a new node underneath every one. So this constructor, there you have this countable branching. It's not a finitary inductive definition but it somehow seems constructively acceptable that we should be able to do this inducted definition although you can imagine its intention with vials invariance principle for predictivity because as you grow the number of functions from natural numbers the inputs of this constructor, which is then in a negative position.

So you have to be careful that you don't upset some theorems that we've had at previous stage. but yes from point-of-view type theory it seems like a predictively innocuous step to go. generalize inductive definitions. so improved theory. start by doing just one of them just the Broward trees for instance or something similar.

use the Browar trees as index for a new constructor that could then branch over the Brower tree, so do their third Brower class. I think it's an indexing or might be off by one! So there is system of arithmetic that captures this. if you are doing proof theory its nice to have just very simple arithmetic system where we can have arithmetic axioms and analyze them.

but it would be equivalent to a kind of type theory that had one generalized inductive definition and That hadn't an ordinal analysis, But you of course the ordinal. You're now talking about has to be very complicated. So it's one of these slightly impredictive ordinals. It's called the Bachmann-Howard-Ordno And the way usually explain it is that you add in A name for an uncountable ordinal and then you build your usual predictive going from below ordinals, but using that as a new name.

And then you step back and say oh actually I had the language so it's-the whole result is gonna be accountable ordinal. go to a certain axiomatic system. So, for example in Piano Arithmetic you have the Axiom Scheme of Induction and that talks about all formulas in the language For any formula talking about natural number if it's true for zero And If its stable undergoing from A Number To Its Successor then It is True for All Natural Numbers.

so You Have The Schema That Quantifies Over Formulas. So if you're really accepting this schema, You should also accept it when you expand the language. Now we have new formulas so that you've got new instances of the axiom scheme of induction. This is an idea of schematic unfolding. and look at an axiomsystem that has a schematic axiomeschema.

And then what happens? If try to explain the language name new things talk about recursions basic things, maybe you want to talk about lambda calculus. So now that you expand the domain of discord and have new formulas for how much stronger does this system go? That should already be implicitly within your commitments because if I add some innocuous-looking extensions into a language like computer programs not just natural numbers it's going that if you do this for piano arithmetic, you end up at the limit of predicativity a system of strength gamma naught.

And then my thesis question was what happens? If we do this with one generalized inductive definition can talk about the ordinal again and there's kind mixture of gamma-naught in the Bachman-Howard ordinal which is like marriage between two and it's the strength the strength of type theory with an infinite hierarchy of universes and then one generalized inductive type.

Very good, thank you! That was very useful. I mean there are lots things which i know a little bit but you clarified that lot so... Thank You! Maybe we can move more closer to the present. I mean, you said already that in a way... ...hobotopy type theory was the combination of two of your interests. I mean this sort of proof theoretic analysis of logic and totology.

maybe can you say more. what do find exciting about hot? Right. So I remember doing my master's studies in undergrad and Copenhagen, kind of combinatorial structure where you have a set of points, then you have the set of oriented edges that connects pairs or points ordered pairs and points. Then we have a collection of triangles where say whenever you have three points and edges from zero to one and two in zero-to-two You can have a sets of triangle that fill into that boundary And than you will have same thing for higher simplicity.

so next would be tetrahedra given by four, vertices zero one two three. And then you have the triangular faces. whenever we have a whole boundary You can talk about all the tetrahedo that fit in there and then All the way up through the dimensions. That's a simplicial set. so it sort of originated or maybe already with at the time of Brower.

So Brower Of course was also interested In both foundations and logic and homotopy theory and topology maybe in the guys of simplicial complexes where you have some extra conditions on your simplicical set, but it turns out that when we actually just look at all simplical sets they have a nicer behavior than this simplicional complex.

There's sort-of thing if you're studying manifolds or to get a handle onto them to prove say one of those famous theorems about manifolds Gauss-Bornet whatever You triangulate your manifold and pick points carve up your manifold into these bits that are easier to handle and then you glue them back together.

Okay, yeah continue talking about hot... Right so often a lot of the things modern topology is doing it's getting at some universal properties of homotopy theory And they're not usual universal properties in one category. Instead of having limits and co-limits, pullbacks push out. And so on. you have homotopy limits in homotopic code limits.

The way that we used to do them with model category theory is You had make a lot choices. So for instance take the Homotopy Pushout of a span. A span has three types or spaces. One of those is an apex then two maps going into another spaces, and then to get the homotopy push-outs you have to replace these maps with cofibrations or at least one of them.

You have make some choice. how do we do this cofiberant replacement? And then take an ordinary push out. it's all very cumbersome! So what can be done in a homotopy type theory is that if your natural thing looks like So in a way, you could view your homotopy type theory already as sort of synthetic theory for homotropy theory.

Yes exactly. Synthetic and the sense that basic objects are the object's interest in Homotopy Theorem. Really? That is another thing I only came to appreciate when you study algebraic topology. At first you look at topological spaces, then maybe you'll get simplicial sets and they appear to be different ways of talking about the same thing.

And what is that thing you're talking about? It's something a little bit more ephemeral these homotopy types. Or spaces Yeah, homotopic type of space or now called anima sometimes because they are like ghosts in a topological space but have forgotten combinatorial sets of points and so on. And only remember the space-of-points, their symmetries... So homotopy type theory is really a synthetic theory that you're only struggling to point at from set theory.

now it's basic object. You are talking about real thing not some presentation or other indirect axis route. I mean infinity group is another And that's another name for it. Yeah, infinity group points. There is Groten-Dix homotopy hypothesis which somehow tries to indicate there are different ways of coming into this notion about a homotopy type either from topology or geometry and algebra.

A group point is the more algebraic point of view. Infinity group points yeah? But I mean sorry no Dennis please... No but just comment! When I got interested in it, maybe i told the story already. Martin Hofmann and Thomas when we looked at this group wheat model of type theory which was there to disprove a principle uniqueness of identity proofs.

We also realized that You should go up. I mean, you should not just have group weights on one level but group weights of group weights and so on. And then we didn't know how to define it here. So if you say omit infinity group weights are an algebraic notion But no, the algebra is... Nowadays there are ways making that more precise behavior.

I don't know, completion structure or opi-topic structure. But yes it was quite an open problem how to actually define this notion of infinity group by algebraic. And again because what you are in the end interested is slightly weaker notion of a homotopy type that doesn't have strict algebraic structures.

Yeah weak omega group. That's why i mean yeah exactly no right? So and then the synthetic view sort of relieves analytic depth by too many details, right? Too much boilerplate. Yeah. and then comes to what I found foundationally very exciting about this is that you can now ask some completely new questions about principles philosophical principles uh that appear if you have this point of view.

so if you had a point of The foundational structure and the collection of sets is naturally a one type, not set. There's no need to be any set that presents the collections of sets Then you have independent from some principles like what I just talked about That there was a set presenting group order sets or more generally for every group order type there are some surjection from elements presented.

So i thought it very interesting. But be careful, when you say the type of all sets is not a set then I find people always think about size. The same thing would hold if we look at the collection of all countable sets or something like that Maybe different depending on size. There's a little bit of danger if you put too many adjectives in them, then there are ways to present it no matter what your foundations have for the collection of finite sets is also good group void.

but we definitely know a set presentation about that because the very notion of finites builds in and has some standard finite sets so they get them all. I guess i wanted ask in a similar direction because you now mentioned fundamentality and what comes first. You can often think from one side about the other, there is some mathematical symmetry but sometimes we might feel a philosophical asymmetry where I wanted to talk about your very personal views because we had our day here... And then this dichotomy continues as discreet.

And what are your thoughts there? and make one tiny addition on that. you had constructed this representation of the whole numbers as fundamental group S-one, right? You made community aware. Yeah I think some more technical results due to Christian Satla and David Van. they have a nice article but maybe i mentioned it earlier.

Maybe at least because thats interesting with all. these. things are so continuous, but you get discrete structures out of it. And for me as a satirist the story is the other way around. I start screed... Yeah that comes back to this idea. there's two different routes to homotopy types either from something very combinatorial like simplicial sets or from topological spaces.

they're continuous and i think both intuitions. Homotopy types on paper, I draw potato-shaped blobs and I draw continuous arrows for the identifications of paths between points. But there's a sense in which even higher homotopy type are discrete because something happens everywhere without any extra spatial circuit.

you've forgotten all that continuous structures, but the thing that remains the anima. The infinity group is no longer a continuous thing But you can then Take the next step and add back in some continuous structure. get to these other models of constructive mathematics via Continuous topological infinity group or smooth infinity group boards.

You had worse on. we talked about some applications. have this I believe? Okay in hot still, right? Yes. So this is the question I mentioned earlier about the expressive power of homotopy type theory. so why didn't a homotopy-type thing take over the world? that's maybe a question. if it was so great Why did all mathematicians just adopt it immediately?

And that has to do with this coherence problem. So, in order to express these nice universal properties is infused throughout lots of higher mathematics. So algebraic geometry uses homotopy theory, even maybe a study of differential equations now would use some homotopy theories nice to have the space of all solutions as a homotopic type and you can prove things if um... You have contractability as uniqueness and so on.

Modern homotopia here's really everywhere! If you have a foundation that's based on homotope types why? Why isn't this everywhere? But we want to be able talk about general universal properties, and universal property is really the realm of category theory. So you need higher categories for the homotopical notion of categories which are usually called infinity category or infinity one category if you want it extra precise.

The open question is, can we define them and do the theory in hot? And it looks like we can't really with a way. We've set things up at least in the book on homotopy type here in the constructions that come out so far. So this was already an open problem. It's been asked by Vladimir Bovatsky. He made very specific.

he asks Can you define what we call semi-simplisher types? Yes I can read the books Simplisher sets but now Simi means we leave out the pesky identities, degenocies and just go for what's called face maps. And that seemed to be as far. defining it for sets is quite straightforward but now you wanted to define it for types.

so... And it's not because we want to have a simplicial or semisimplicial types for their own thing. It is, Because We Want To Do Higher Category Theory and that's just the way you can think of to get at higher category theory. If You Had A Theory Of Higher Categority You Would Immediately Get The Notion Of Simplicial And Semi-Simplicial Types Because They're The Functors From Some Small Indexing Category Into The Category Of Types.

So The Two Problems Are Interproducible. so Maybe Focus On What Looks More Concrete the problem of semisimplitial types. Yes, and that's- This is a problem. where you first look at it You think yes sure I can do this no problem yeah? And then realize No! It doesn't work. Yeah in everything you try Doesn't seem to work and you don't see any immediate obstacle either.

We have no idea how to construct some weird counter model Of homotopy type theory Where this does not happen. So its really wide open Right, so that leads to some of the work I've been doing in the last ten years maybe on Simplicial Type Theory. You had Emily talking about this and have done a lot more than trying push it forward or do an actual higher category in Simplicical Type Theory which is an extension to Homotopy Type Theory but still has all these nice properties where everything is invariant under equivalence.

you don't pick any presentations for anything unnecessarily. But you have this structure of simplicial types built in, and you can talk about higher categories. So the way you do is I think very reminiscent off like cubical type theory on a Cougouin other where we add this interval right? And the difference that's the interval which as in cubicle-type theory it not redirected whereas the interval a subficial type theory is really has the direction right and promises you get.

Yeah, there's definite similarity in that you add an interval object. The dissimilarity is that in cubicle type theory You're trying to explain homotopy type theory To this set theoretic mathematician or foundation doing it with foundational reduction of sort of univalent foundations choose combinatorial set theoretic foundations.

So you end up, look at cubical sets and You can also look at Cubicle spaces. And in fact in Simplicial type theory it's very useful to Look at cubicles basis as well. But we can't call it cubicle type theory because that is already taken for the other thing. so when We do simplicial types here via cubes be usually called a triangulated Instead.

but It's really the same kind of cubes That appear in cubicle Type. Theory just Can use it? Because then We'd look at spaces and not sets. Oh yeah, let's stop it for a moment because so the cubes are good like for symmetric version but the triangles easier to direct was always my impression. They're also directed cubes.

When you think of the interval in cubicle type theory as long as you don't add a reversal that forces everything goes forwards can go backwards then we still have a good notion. Okay, so that's not a problem. If you think of categories then composition naturally leads to triangles... So if we're representing a category in the composition of morphisms via like filled-in triangles and do this with in the cubicle style you have filled in squares?

You definitely want it. You can glue together a square from its two sub triangles on the lower and upper triangle. So that's why you're really interested in this triangulated structure on cubical basis. if your basic objects are cubes, we still want them to behave nicely. with respect to triangulations of cubes Yeah so I'm just saying If you look group leads then cubes fit in quite nicely Whereas if you do category theory, it seems to me that triads fit better.

Maybe there's a bit vague statement but... Yeah I think both fit well for infinity group boards and infinity one categories And both have some issues. when you try go higher or higher categories. so infinity two categories and beyond. There we need more complicated shapes. Maybe we could play what's infinity one is?

Yeah, no. Infinity One. in an infinity groupoid between any two points you have another infinity group void of isomorphisms or identifications at the point and In an infinity-one category when you had to have a collection of objects And then for any two objects You have a collectin infinity group voids.

so one dimension lower of morphism. So not necessarily invertible morphisms. do the next level up in infinity two categories. You can have your collection of objects, but then now between any two objects you have an infinity one category of morphisms and Then in the limit you just have Categories all the way And between any tube objects?

You have another category of Morphisms That will be infinity infinities In some sense. so I Just wanted to step like once that back and asking you How much of this is full constructive? because I mean if you ask a regular mathematician why he hasn't hot one Then they might say something like yeah, this is constructive math and then the hot person might say.

Yeah But you can add choice but it's not so clear as at real deal. Is that just a weaker reconstruction? Yes It comes to more sociological point perhaps that the development of mathematics depends on people involved and it so happened a lot who are interested in Homo Tobi type theory early on, maybe because there were a lot of computer scientists.

We're interested in constructive mathematics and I'm also interested in construction mathematics. but from our point-of view classical mathematics is the special case of constructive mathematics where you have some extra principles. so your very welcome to use our constructive systems. do classical mathematics.

The one classical principle that we lose in univalent foundations it's global choice that you cannot get. You can not pick for every set an act...you have to have a choice function, which picks up on each element of the set globally because it would not be invariant under the symmetries in sets. Even picking one element out of two elements is a no-go Because your choice will have to be invariate into symmetry over two elements That could swap the two elements so they wouldn't be invariated.

But otherwise, you can have the axiom of choice and anything else. You like large cardinal principles that's fine. but yes I'm interested in because i'm interested In this generalized Hilbert program. And what rests on what? What kind of parsimony Can we get away with? The weakest system That is suitable for a task?

uh...I Like to make sure that things are constructively meaningful. Actually had earlier said something that you had this crisis of foundational beliefs. It's interesting because recently we talked to Giovanni Sambino who told a very similar story, right? That there seem to be type people not just accept the mathematics they have thrown at them but want to dig deeper and really understand how it all fits together intuitively.

Is that a question? Maybe, comment on this! Okay yeah I think there's something about my personalities. other people are more happy to just solve the problem and then get on with it. i'm i'm happy when other people solve problems. i'd like to understand. uh structure build nice get proofs from the book.

But it seems to me that there is a relation between structural mathematics and constructive mathematics. They are not completely independent, so in particular that in instructional mathematics if you're systematic You can avoid doing these choices. I mean what's the origin? Why do people need action of choice?

The number of reasons. But one of them seems to me that they hide their choices and then later, if you want to restore them. That's right! If your work structurally... You're able never-to-hide-your-choices. This is where types theory will be. Maybe this something we can briefly mention about category theory.

in Univalent Foundation It becomes much more constructive And well behaved because Your categories have group points or one types of objects and not sets of objects, you can have some theorems that look very classical like every functor. That is essentially subjective and fully faithful has an inverse Functor.

if You do this with category theory in constructive set theory it doesn't work. But If you Do It In Category Theory and Univalent Foundations then it just becomes provable without any extra assumption. Yes I mean Like a univalent category where any isomorphic objects are equal. If you do this in classical category theories, there're very few categories which has this property being skeletal right?

But if we move into hot then all the natural categories visualize have this property. Exactly I think that's another instance where mathematicians were looking at a concept and they defined it as notion of category And it turns out what they were really interested in, that's actually defined with this notion of a strict category.

That has set or set-like collection of objects and sets of morphisms. but what we're very interested is something forgotten about the identity... ...of the object and district presentation of the objects. so they invented this notion equivalence categories. I like these two slogans of quine no entity without identity, right?

So if you have different criteria of identity then your really talking about a difference notion and it might well be that one is an abstraction or concretization the other. I think that exemplifies this. people were looking at strict categories but often they are interested in this thing abstract from the strict category where the notion criterion identity equivalent not isomorphism.

And because the criterion of identity has changed, it's a different notion. Now what do you call this new notion? One name is a univalent category or if your working inside Univalent Foundation we tend to just call them categories and then called other things strict categories. Oh yeah that was an argument we had always had.

A terminological disagreement But it mirrors this move in homotopy theory from looking at topological spaces as implicit sets and sometimes being interested for topological space's homeomorphism, so sameness-as-topological spaces. And Homotopy equivalence which is presenting the same homotopic type. It again indicates that there are two different concepts because they have a different criteria of identity.

For dummies its the same as difference between preorders or partial orders. In a pre-order, you may have things which are less or equal in those directions but not necessarily equal. But then you really want to say how if I cannot distinguish them by the order they must be equal. and this is one level lower...

One Level Lower Yes so every pre-ordered gives rise to a partial order. And same way Every strict category give rise To A Category As i would Say it In set theory, every partial comes from a pre-order. But then in univalent foundation not every category necessarily comes from strict categories. that's now philosophical principle.

you may adopt or not. it is the choice. Maybe this raises like second classical object question. I mean how much of your work is constructive? and now how many are univalents? really baked in or is it just turn on and off? So for the classical part, I tried to come up with a constructive proof. And i think that most classical theorems.

there are some very. you can tweak it a little bit then get a constructive formulation. yet they're constructed. hard of it. but of course first comes out. maybe allow yourself all tools. could we get away with something else? And maybe it's the same thing, if you get stuck. Maybe try to apply techniques of model categories similar and then later find a univalent proof.

but I tend so much easier to work just univalend all that time! Can I bring up like one other thing you mentioned? How is your relation to proof assistants, are still using them or even developing them? how's the back and forth. Yes! Or are you developing libraries for them? Yeah so as i mentioned i started playing around with coq now rock And then i learned actor and my actor matches very well in of thinking.

While I was at CMU with Steve Audi and Jeremy Avigat, we also played around with Lean-Leen II in the time when we had a hot library. so it's part of that but mostly its ACTA these days because ACTA has all the features that i need So like to do. modal type theories. you have modalities in ACTA. You can do cubical type theory if want compute with Univalence.

It is perfect playground for them. I am interested in also to eventually designing new type theories that could result a new proof assistance. So, i'm interested some programs about other kinds of synthetic mathematics maybe synthetic topos theory we can talk about for little bit. so in constructive mathematics we interpret Some of the miles you get from proving something constructively.

is now you can interpreted it more models Again foundationally goes back to Chrysler's program proof mining and figuring out. what more do you know than the mere truths of a statement when you've proven it in certain, very restricted means for example. In a constructive system where well if we prove something constructively You get realizability models?

You get topos models. that's on. And so okay now you can say Well let's not really milk this forward. It's worth an look at various toposes and What constructive mathematics looks like there and adapt add the axioms that are true their Okay, but now you have all these different interpretations of constructive mathematics and would like to relate them.

So what is the type theory that will allow us do this? I'm thinking about it a lot recently. And eventually we might as well have proof assistant who could really jump in between... For me its universes because i am thinking that way. It's perfectly concordant with the idea of multiverse theory Models of classical mathematics.

It's models of constructive mathematics includes. all the models are classical mathematics But many more as well. More variety in a way. yeah, I mean we also we have both interested In what you already mentioned this directed type theory? I mean so your approach is Violating just directed intervals and some official types theory when he did some impressive results there like proof that It's interesting, the category of categories is not a category.

I mean one category or two categories and so on. even two ones but you always move up. But then the category in infinity categories isn't an infinity category right? And you prove this Simplicial type theory. Yeah, we constructed an object that is the infinity one category of small infinity one categories.

You still have this size jump but now you know I have a structure difference. That's right. But just like in ordinary homotopy-type theory The universe of types Is another type and it perfectly fine with univalent foundations And same way you can have large infinity one Category. So I was more interested.

My original is a little bit less topological and most of type theoretic, And i'm keen on or would like to have a directed type theory in particular. so actually my motivation while ago was... I want the types theory where naturality principles come for free. So I mean, naturality is like this diagram.

If you reverse and map it's the same as if your first map and then reverse here. so that what called naturalty And its because in type theory we cannot look into representation of a type. so everything should be natural or polymorphic It shouldn't really depend on representation and there should reflected inside the types.

theory was my original motivation. And just to interject there, in homotopy type theory everything is natural. with respect to isomorphism? Exactly yeah sorry but thank you. so now we would like that also for the naturally with respect of morphisms when a directed version. because these two principles I mean univalent and naturality they are both should have the same conceptual basis, namely if you cannot look into this representation.

You can not define anything which is a representation independent so that it has to payback of this discipline here your very discipline. we never looked at the presentation though I want to get something from it and we got something. but we need more right? And i think both agree that we would like to have a type steel which exposes this principle, but yeah.

But you're not getting the money for it is? Not yet! We'll try again... pathways for the research funding because of all the computer application. I think there's a philosophical point about directed type theory versus undirected type theory and categories vs types, Because it seemed like they were such big foundational improvement to go from categorical foundations where you wanted to base everything on categories To univalent foundations with their homotopy types are the foundation objects because There is often choice in directed structure And not everything is natural with respect to directed morphisms, but every thing we do in mathematics should preserve equivalence and identification.

That's structuralism. so it seemed like such a big advance that could have the undirected homotopy types as foundational elements then build the direct structure on top. The infinity one category is out of the infinity group points. So now we're back and looking at categorical foundations where maybe you have to add an epsilon of directedness, back in the foundations?

Yeah I mean so. if you come from functional programming it seems to be very natural with everything that's natural because You cannot look into representations but then the theorems which prove this themselves are not directed with respect to their assumptions. So it's a bit more complicated... Yeah, that leads us the necessity of modality.

so one other modalities we often work with is something like looking at this discrete part. The discreet is very overloaded. but if you're looking at the direct things then the discrete parts will be ones where they don't see the directness and topological things and the discrete parts, that don't see the topology or whatever.

The discreet is very context dependent. but yeah then you need a modal operator to move from the directed to the undirected because some things just don't obey the directed naturality. so we have forget direction before it gets something natural. Yeah let's add to the complications exactly turn. So maybe since running out of time, is there something you really wanted to talk about?

I have one more question. We should maybe ask everybody now what's the impact on AI in your work and how would you recommend young researchers, mathematicians, computer scientists, philosophers... how to deal with this AI. Okay, I can talk about the first part. i'm not sure very comfortable with the recommendations because I don't have my crystal ball around here.

so no what's in future is like... I am using these tools because they are great at speeding up research and help explore problem space proof space by searching for proofs in very sophisticated ways. They're quite smart, so I can quickly get a formalization of something. Obviously these are stochastic entities even though they're intelligent and still non-deterministic compared with proof assistants because if you want to know whether some conjecture is true or not as an example just ask the model.

you know for sure that it's correct. You don't have to read a slop proof, so I do that a lot particularly since the last five months or four months because they've really gotten good at that sort of thing to write an article, because I think what we want is human understanding and human communication.

And human connection in a community of human mathematicians. but we can use these tools to help us understand better and see further. that's good. But we should have our own meetings and discuss like we do here without mediation by AI. So i would advise maybe other people to think about it the same way.

Do you use them for maybe considering also the ethical implications and behavior of a company sometimes. But hold on to the goal that we want human understanding, express ourselves and express our human mathematical understanding. Very good! Thank you. Dennis asked about if there's something we didn't talk.

We could talk a lot more about foundational choices and so on. I think one thing i like is Karnab's principle of tolerance, that you are free to pick whatever foundational language you'd like And then do your mathematics there? Then we figure out all the translations The proof theoretic interpretations have one into another for each instance of what we want to do, the pragmatically most suited language.

Maybe you have some thoughts on this and other matters related to choice or foundations in various settings? It's an interesting question I think from the perspective of non-foundationally interested person. they really wanted black box. that right. it is a different program than maybe large part But it shouldn't interfere, so Karnab's neutrality is somehow used to wish for.

but tolerance isn't really there. Just a descriptive point right? Not an normative one. That's right. One thing we can do now with these AIs reverse mathematics and we can work more towards getting the best proofs, understandable proofs. And that might involve switching foundations sometimes... Getting constructive content of a proof or interpreting it in some other topos for simpler argument.

then moving back. I think thats quite interesting possible approach. Another thought on AI and mathematics is that for this millennium, so between the year of two thousand we have the clay-millennium problems. And recently we had a solution by an AI of the Navier Stokes problem. And at the previous century, so in nineteen hundred we had Hilbert's problems.

One thing I liked about Hilbert problem is that they are more vague there. this acceptance criteria often completely vague and you can interpret them in many different ways. Maybe those kind of problems were fruitful. now machines could just burrow down a solution to very precise question something like Hilbert twenty-fourth problem which was not on original speech but he added his notes what is simple proof And what is the identity-approved?

The questions like that are very fruitful now. I mean, at some sense in your cars because you're really building the architecture of math so to speak and looking into relations there an oracle just helpful Because You know on top What can be put below. But if you have a pure problem solver Then a lot gets lost because then the oracle steals a lot of the fund.

Yeah, I mean it's still the same value to get there and It is great not to waste half your attempts Because you are trying to prove the wrong side. But again You aren't really wasting them Your understanding while doing that To get credit. And they're we need too...I guess We need be honest..It was never about truth Of arbitrary proposition.

if somebody came and said, I know for sure one hundred percent. And we all believe them that Navier-Stokes is true or it's wrong then nobody would have won something. There are some discussion whether this Navier Stokes which has now disproven actually really what you should use? Yeah so there many questions can be asked about the Navier stokes equations four variations.

that were precise questions you could ask. But maybe once we now know the solutions, what is it A and C or something like in this list? Maybe some of other questions about Navier-Stokes are actually more interesting but they won't have same status as having been a millennium problem. They're not there to look at.

Don't want to really say something. I guess the last thing we have to say is thank you very much for this lovely introduction and Amy, We skipped levels from clear basic introduction to very advanced topics. It was wide-ranging in fun. so Thank You very much For having me. Yeah, thank you. And having said that ,we also always need To thanks of course our audience and support us and commenters and all.

This would not Have been possible without All The interest and support we are getting here. Please ask questions and discussion is always encouraged. Maybe we find two better ways to encourage us, but if somebody comments or makes a proposal please do so!

aboutlogic #24 | Why Didn't Homotopy Type Theory Take Over the World? | Ulrik Buchholtz

Kapitelklicken springt direkt hin

Shownotes

Transkriptvom Podcast bereitgestellt · Zeitmarken springen hin