aboutlogic #19 | Homotopy Type Theory, Narya & the Future of Proof Assistants with Mike Shulman

00:00:00: and two of those can be too equivalent, then you have three levels.

00:00:07: so the collection is a free group wide.

00:00:09: At that point a mathematician says well we should go to infinity.

00:00:19: Hi!

00:00:20: Welcome everybody.

00:00:22: our guest today is Mike Schulman from San Diego.

00:00:26: he's known for his work on homotopy type theory category theory lots other things and more recently higher observation type theory, and scenario proof assistant.

00:00:39: I think he's played a major role in connecting abstract ideas from homotopy theories with practical computational side of proof systems.

00:00:49: So welcome!

00:00:50: Good to see you.

00:00:52: Thank You for the invitation.

00:00:54: When i may start asking about your academic path, so to speak.

00:00:59: In particular one thing is interesting because you are a proper mathematician and then you care about foundation right?

00:01:06: And often people say oh no this is divided there's no such thing.

00:01:10: how was your path?

00:01:11: two foundations at homotopy type T review

00:01:15: That that's an interesting question.

00:01:18: I mean uh i've kind of always been interested in foundations a little bit.

00:01:22: when I was an undergraduate I took logic courses sort of as a sideline.

00:01:30: For, for a little while I was really interested in non-standard analysis and have all bunch of those books on my shelf.

00:01:36: And then uh...and Then i went to Cambridge for year and took the category theory class from Eugene Yicheng and got sold on that!

00:01:43: ...And when I went to UChicago Uh..I wanted to do Category Theory like Peter May who is the only person there That could conceivably work with.

00:01:54: so ended up being a topologist and I learned a lot of topology, but i was always sort-of interested in this foundational or logical direction also.

00:02:04: And then the way it got... It's kind of perfect setup really for me to be recruited by Steve Audi when Homotopy type theory burst on scene because I had interest logic.

00:02:20: So yeah, and homotopy type theory really grabbed me at the beginning because partly of my background in category theory.

00:02:39: This sort of idea was in the air around that.

00:02:41: this is like back-in-the-oughts And John Baez people were making a big deal about doing things up to isomorphism or equivalence.

00:02:50: all homotopy type theory sort of had this promise, making everything... Yeah, it's morphism invariant or a homotope invariant that we could have foundation based on higher categories and higher group ways.

00:03:07: And Steve students and some other people like Michael Warren and Peter Lumsdain has been proving various things in that direction.

00:03:15: Then Steve invited me to come to the talk by Vavadsky Snowballs from there, I guess.

00:03:24: So you were recruited by Steve?

00:03:26: I didn't actually know this did your work in CMU or?

00:03:31: No um...I was never at CMU myself and i was a grad student.

00:03:36: And they post doc at UChicago.

00:03:39: Yeah which is..i mean i have to- i guess two european They're not very close but uh to an american that are pretty close together.

00:03:46: yeah they Were close enough meeting where we all came to see Hirvavadsky talk about Univalence for the first time and there was this big snowstorm.

00:03:56: I shut down all of the airplanes, uh... And eventually i was able to rent a car and drive back to Chicago in a day.

00:04:01: so that's pretty crazy.

00:04:03: Yeah maybe can you follow up on it?

00:04:07: For our audience We had Steve already here as guest but still would you be kinder give us run-down what is hot.

00:04:17: So what is homotopy type for those?

00:04:19: Yeah, absolutely.

00:04:24: So type theory—I mean I expect your listeners have heard Dorsten Ramble on about type theory a bunch.

00:04:31: so my type theory is sort of a theory that could be foundational like set theory but where the basic objects are types which are distinguished from sets among other things by not overlapping basically and every element comes with a type rather than it being question.

00:04:46: you can ask.

00:04:49: Dorsen will interrupt me if I say something he hates.

00:04:53: And the Homotopy type theory, The idea is that instead of treating types like sets we can treat types as some homotopical or categorical object.

00:05:04: That are some variously called spaces, homotopy spaces infinity group voids anima Various things have this sort where in addition to elements a one of these things has paths or homotopies, or equivalences, or isomorphisms.

00:05:21: Or identifications whatever we call them reasons why two of the points are the same and two points could be the same in more than one way if they're the same.

00:05:30: And then that gives a higher dimensional structure because you can iterate it.

00:05:33: Two paths can be the Same or not The same and so have those Can Be the same?

00:05:38: So this sort of structure has been studied by homotopy theorists and category theorist in various different ways.

00:05:44: And then there are various names for decades, but the idea of homotopic type theory is now that rather than defining these things in terms of sets we take them as a basic objects to study mathematics.

00:06:00: There have been several sort of waves maybe or homophonically type theory.

00:06:07: And I expect we'll get into that a little bit later, but this innovations of Stephen Owazki was the first beginnings of that idea which figure out how to make it work.

00:06:21: So why would somebody who doesn't was mainly interested in topology?

00:06:27: Or algebraic topology?

00:06:28: Why what's there care about hot?

00:06:30: That's

00:06:31: good question and

00:06:32: maybe they shouldn't.

00:06:34: Yeah, so I always like to start with that.

00:06:35: Right?

00:06:36: It's...I don't want to oversell it for somebody who is a combinatorialist or an analyst and someone interested in simple structures built out of sets which do not have much structure to them—it may be not THAT important!

00:07:01: where it starts to have benefits is when you start talking about structural mathematics and your studying not just numbers but groups or rings, vector spaces which is built out of sets or types and operations on them.

00:07:27: And then you start comparing various of these, very quickly run into this observation that different structures are essentially the same.

00:07:35: like there's really only one group with two elements any two of them are isomorphic in exactly one way.

00:07:43: so group theorists start quite freely talking about THE group from a classical set theoretic or even in non-homotopy type theory perspective, there are actually lots of different groups with two elements and they're all just isomorphic.

00:07:56: And so the nice thing about homotopy tech theories it... With univalence you can say that these groups are actually equal.

00:08:04: uh ...in the sense of.... In the only sense that makes any sense!

00:08:09: The only notion of equality that applies to them is the one that says that informally, say okay well anything we can say about a group of two elements is true but any other group with two elements.

00:08:22: But that's not literally true in sort-of a subtheoretic framework...but now it becomes literally true!

00:08:27: We have a way to automatically translate from something about one to another one and maybe not all that important for pencil & paper mathematics when you start just started working with groups But when you start formalizing things in a computer, then it can be helpful to have this automated way to translate so that we don't have to manually code up what means to transfer commutativity across an isomorphism every time they come with new property of groups.

00:08:53: And also... It's been observed many times different fields of mathematics, over time they start to get more categorified and homotobified.

00:09:04: when you started looking at structures.

00:09:06: And then eventually you're studying so many different structures that you start seeing structures as a structure is in this world where we have the deal with all sorts of homotopical hierarchical information.

00:09:16: So nice thing about homotopy type theory is it's there on the background automatically and appears whenever needed without You haven't go do anything to put it in.

00:09:26: As soon as you start talking about structures, you automatically have the right notion of sameness between them.

00:09:30: and as soon as we started talking About structures if structures?

00:09:33: You automatically Have The Right Notion Of Sameness Between Them.

00:09:35: And so

00:09:38: So Do you think that That using a hot changes the way you Think About Mathematics?

00:09:48: Yes I don't.

00:09:53: I don't know how big of a change it is.

00:09:55: It depends on how much of an impact that has on you, the average mathematician doesn't really care whether sets are ZF-sets or types of H level zero.

00:10:10: and so from that perspective even a mathematician who's thinking like that was sort of wasn't trained in logic.

00:10:15: its not going to maybe make huge difference.

00:10:17: I think it does sort of train you to think more in the structural way, i guess.

00:10:31: Thinking of sets as being defined not by collecting some pre-existing elements but like as a structure.

00:10:40: yeah i don't know.

00:10:40: maybe i'm not the best person to answer that because sort of...I always thought like that.

00:10:44: so It didn't really change the way.

00:10:46: i thought

00:10:48: Yeah for somebody else and there could be some education.

00:10:56: You mentioned like there are different waves of hot or off this foundations.

00:11:02: Would you be so kind and help us?

00:11:04: What was the OG version, what is... The newest one maybe yours but some steps in between.

00:11:13: So they're sort three general approaches maybe now to making this formal system work.

00:11:23: There's the original one that came from Steeves and Vovazkis, Michael and Peter and all those people building on a special year.

00:11:34: so it goes into The Book called Honotope Type Theory which we call The Book or Hot Book.

00:11:39: And so that version of the theory is sometimes called book-hot because it came from one we just did in a book.

00:11:45: The next one, what sort of came after that was cubicle type theories.

00:11:50: and there are different kinds of cubical type theories then more recent ones not fully realized yet but Thorsten and Amrush and I students working on higher observational type theory Recently, I've been thinking that when we talk about the differences between these three ways of doing hot.

00:12:13: We are emphasizing, maybe you're emphasizing the wrong thing?

00:12:17: That...we often talked about it as being-the difference is the smallest reflexive relation, or they're inductively generated by reflexivity.

00:12:31: And then in cubicle type theory there defined by paths mapping out of an interval some kind and than higher observational-type theory their define sort observationally based on what that we are looking at?

00:12:43: That's important but I'm starting to think it is almost downstream a more fundamental difference which which is sort of a grandiose thing to say, but in the way it's kind of like what all mathematics are about and dealing with infinity.

00:13:08: I don't know... maybe i should back up a little bit.

00:13:14: so The problem with trying to formulate a foundational theory infinity group voids, is that an infinite group void has infinity in it.

00:13:27: It sort of has an infinite tower or structure.

00:13:29: and how do you describe all the structures?

00:13:34: Maybe if I could say a little bit more for audience what an infinity group would look like intuitively.

00:13:40: Yeah yeah...I mentioned really briefly before.

00:13:42: but think about so.

00:13:46: example on ordinary group white is collection sets.

00:13:49: So you have sets, and then you have isomorphisms between sets or bijections between sets.

00:13:55: And structurally we consider two sets to be the same if they are related by a bijection because we can transfer the structure of a group across a bi-jection with everything that we want to do with it structurally.

00:14:07: Similarly like collection groups in group isomorphism's.

00:14:10: Now, the collection of isomorphisms between two groups... ...is just a set.

00:14:25: If I asked whether two isomorphism are the same they're not.

00:14:30: But if you talk about the collection of categories or the collection group-wise themselves, then one or two category is the same.

00:14:35: Two categories are when they're equivalent meaning there's a functor between them and going back to other way.

00:14:41: but composites are just isomorphic naturally isometric to the identities.

00:14:47: If I ask about the collections of equivalences between two categories that's a group weight itself because two equivalence could be iso morphic maybe in more than one way.

00:14:56: And so i have different levels notions of sameness.

00:15:00: And that forms what's called a two-groupoid, where I have objects and then I have equivalences or isomorphisms between them... ...and another layer of isomorphism in those.

00:15:10: Then you can say well what about the collection of two group oids?

00:15:15: Two of these can be equivalent to three levels.

00:15:20: so at this point a mathematician says we should go to infinity.

00:15:28: So an infinity group white, it has points and then equivalences between them.

00:15:32: And equivalence is between those in equivalence as between those and equivalence's between those on so-on all the way

00:15:40: up.

00:15:40: I noticed that you start with zero and i would stop at minus one.

00:15:46: yes well Yes, so I started with zero because that's the historical way of thinking about it.

00:15:54: and then you sort go downwards from zero also which John Baez called negative-thinking.

00:16:02: So in type theory we have a stratification for types representing infinity group whites.

00:16:15: two group-wise or one group-wides are zero group wise which I like sets and then the level below that is The minus one group ways, um Which are basically either.

00:16:24: well from a classical perspective.

00:16:26: They're either empty Or trivial.

00:16:28: from a constructive perspective you could say something Like if they have a point than their trivial

00:16:32: Yes But but what i'm what i wanted to refer To us?

00:16:35: it's a structure as a structure of an equivalence relation right?

00:16:40: So in a way to explain higher group rates, I mean people with maybe computer science.

00:16:50: They have no equivalence relations and then they say okay group rate is equivalent relation on steroids yeah?

00:16:55: Yeah that's the good

00:16:59: point.

00:17:00: definitely so.

00:17:03: if instead of starting from sets you start from equivalence in a veil on perspective, there's maybe no difference between that.

00:17:12: But if you think about like a collection of presentations of elements of a set and then have some equivalences between them than passing to group white is basically just saying Like You can have more than one sort of witness or reason why two things are equivalent.

00:17:30: But the thing that makes it complicated is, once you have these just extra structure and you really want to study those extra structures then you need coherence conditions on them.

00:17:38: You need be able say if A is equivalent of B or C or D than two different ways are making that a-equivalent to d are actually

00:17:48: equivalent

00:17:49: And put in this world where we have infinitely many coherent structures.

00:17:54: I

00:17:58: interrupted you, but it's an interesting point about this different view support in infinity.

00:18:06: Maybe we can continue...

00:18:07: So the question is sort of how do deal with all these infinite much structure?

00:18:11: In a formal system which means to be usable by human or implementable on computer has somehow been finitely coded before people?

00:18:27: People misunderstand what Vovatsky really brought to the subject.

00:18:34: It's this sort of people talk about Vovadsky contributing to univalence, is something like this big thing that made us a subject work?

00:18:41: but at that time, really, univalance was obvious.

00:18:45: At pre-Vovadski we knew that something like univalents would be true.

00:18:50: if had theory it wouldn't work.

00:18:52: What Vovadsky did?

00:18:53: He came up with a definition that made it possible to state univalence.

00:18:59: I mean, the idea of univalance was already there in this Hoffman-Stryker worldwide bottle paper.

00:19:04: they call the universe extensionality.

00:19:07: Univalence by the way actually probably say this right.

00:19:09: so In type theory we have among all the types We have types which are called universe types whose elements our other types.

00:19:18: So not all of them for like paradoxical reasons, but some collection small types form a universe.

00:19:26: And so we can talk about when two types are equal and univalence is the principle that says to type's or equal one their equivalent which is really just incarnating idea I was describing before.

00:19:38: the two sets are equal or the same when they're isomorphic into group ways in this aim on there.

00:19:45: So in a sense, that's obvious really to a category theorist or homotopy theorists.

00:19:48: But the problem was we didn't know how say equivalent before Vavatsky came along because priori it seems like it requires infinitely much data sort of some kind of code.

00:19:59: and Vovatsky come up with this clever way saying what is means for two types to be equivalent using finitely much data.

00:20:06: I remember after at that weekend CMU all came here to talk.

00:20:13: afterwards in the pub, we were all sitting around and weren't talking about univalence.

00:20:16: We're talking about his definition of equivalence because that was a really exciting thing relating it to other ideas or equivalents than people had thought about And if you are more familiar with homotopy theory stuff like That.

00:20:28: so In a sense though The idea for first wave was sort of use.

00:20:35: finite definitions produce all the higher structure in some sort of automatic way.

00:20:41: And like that, but the paradigm of that maybe is to say when we said a type was contractable... That Vivaldi's innovation wasn't it?

00:20:53: To say that a type is contractible and so the homotopical sense of having no higher information at any dimension.

00:21:00: All you have to say is there are points where everything else has equaled.

00:21:03: It's just sort of like the very naive, set-theoretic way of saying that it is a one element set or one element type.

00:21:12: And Erwadski realized if you write that definition directly and naively in the type theory actually tells not only to points are equal but also any two paths they're equal as well.

00:21:24: so all this higher stuff disappears.

00:21:27: So

00:21:30: here was point where some types theory were essential.

00:21:35: I think Włodski, you know in type theory because he wanted to formalize some results.

00:21:40: But then he realized that this is actually more than just the vehicle but it's also maybe way too express these ideas?

00:21:50: Yeah!

00:21:51: Um...I wouldn't claim that i really know exactly what sort of

00:21:54: path

00:21:55: we went through ...but i've definitely heard all right here.

00:21:57: That was where he came from.

00:21:59: By the way there are not so equivalent definition of equivalence.

00:22:03: Yes

00:22:04: Which one is your favorite?

00:22:07: My favorite, the higher co-inductive one that we use in home optimization.

00:22:14: We can get to that later!

00:22:17: This was an infinite one

00:22:18: right?!

00:22:20: In a way you're overcoming Wojcicki's idea which initially sort of excited him to have like a very finite territory difference.

00:22:34: Can you quickly say, what is the notion of equivalence?

00:22:40: You learned from Wojcicki.

00:22:42: Is it that fibers are contractable or...?

00:22:45: Yeah!

00:22:45: That was Wojcki's first version to say a map has an equivalent if its fibers were contractible.

00:22:51: in set-theoretic phrasing... ...to say that the preimage at every point is singleton and turns out tell you automatically that it has all the higher sort of coherent notions.

00:23:07: and then afterwards people came up with various other versions too.

00:23:11: Yeah, I always think... It's interesting to contest this notion of bijection where basically what users say is a unique existence.

00:23:21: but in type theory we use the notion of contractability which also applies actually to equality proof.

00:23:29: That's the trick.

00:23:32: grow at infinitum, right?

00:23:35: Yes.

00:23:35: Yeah you can definitely say that.

00:23:38: but one of the things I don't like about Fawcicki's definition is it's not symmetric.

00:23:43: That's true.

00:23:44: You have a map in one direction and then you'll see that its fibers are contractible And you could use to make an equivalence on any other directions.

00:23:50: But It's not the same thing.

00:23:53: Very few definitions are symmetrical

00:24:01: already, but the very naive question as somebody with hardly any topology or algebraic geometry background.

00:24:09: How symmetrical is the fruitfulness between the fields of type theory and homotopy theory?

00:24:16: Is it like really that you can get new topologically interesting work out of it ?

00:24:23: Is working in this way too ,or mostly?

00:24:26: we now used We enrich type theory and logic, foundation but look so to speak for a time.

00:24:34: For somebody only interested in topology nothing really new happens... ...but one weird

00:24:41: application.".

00:24:43: Yeah that's great question!

00:24:46: So far I would say the direct influence on hoentopy theory has been limited.. ..but not empty.

00:24:59: So certainly, a lot of it is the flowing from homotopy theory to type theory and importing these ideas into type theory.

00:25:08: And part of that is just because the homotopic theorists have such a big head start... I've been doing this for decades and we're sort of trying to catch up on basic things they can do.

00:25:22: And part of it is because there's some, I mean more them.

00:25:26: So It's hard for us to catch up cause that isn't the many of us working.

00:25:32: and also Part of it Is That We're sort of wearing a hair shirt Where we were doing things in A way that is More difficult In Some ways Because we get more out Of Thurston, you like to make this point about constructive mathematics somehow.

00:25:54: You can avoid axioms and get a more general theory where we're working in an axiomatic or formal system that limits what gives us better results because among other things, right?

00:26:18: It means that the theorems we prove are interpretable in any model of this theory.

00:26:24: But it also takes away some things classical non-authenticians can do which allows them to get into things quicker.

00:26:33: So I would say like... The influence thats gone the other way has been partly in the direction of inspiration and ideas.

00:26:44: So, learning to think type theoretically or homotopy-theoretically and then using ideas from that... ...to inspire work that's phrased in a more traditional context.

00:27:05: Which is sort of better or cleaner than it would have been otherwise but its not literally phrased using the type theory.

00:27:12: And then there have been some places, like.

00:27:16: the most famous of these applications is the Blakers-Massi theorem in higher topoi.

00:27:21: Which really wasn't a native proof of that used in higher Topos as before we had the proof in type theory and then... That type theoretic proof was later translated back into classical category theoretic language.

00:27:39: so

00:27:40: yeah I think I think over time there will be more of these sort of applications, but it feels like its going to an uphill battle for a long time because so many mathematicians are not really foundationally interested somehow.

00:27:56: They just care about using some tool and Jacob Lurie wrote this giant tome and they can say, okay, Luri did this in this.

00:28:05: And then I'm gonna do it this way.

00:28:07: that doesn't really matter to them That there's a cleaner or more elegant for general way of doing using the type theory.

00:28:13: So just one remark.

00:28:14: we had Emily real recently right?

00:28:18: She talked about synthetic mathematics very hard to write down in the classical framework, because you have too many conditions to check.

00:28:35: But if we do them in type T way like... You can do them synthetically as well.

00:28:42: so anyway your void lots of boilerplate right?

00:28:46: I mean i had a colleague.

00:28:50: he now moved on.. He moved to different place and And he was interested in mathematical physics.

00:29:02: He used actually higher categories to do this, and always complaining about having checked lots of conditions.

00:29:09: basically at the end they just said oh yeah we know it's true that you're not going to check us You know?

00:29:15: So I tried to convince him to do so more synthetically In type theory application or what you think of all this.

00:29:25: Yeah, and in a way that's kind of the problem really is that mathematicians want to do stuff.

00:29:34: everybody every mathematician has sort of a boundary within which they're willing to work right?

00:29:42: And when they get something outside their boundaries are not interested in it.

00:29:50: But when they're inside that boundary, then they want to do the work and maybe get disappointed if somebody else does it for them.

00:29:56: Or at least... That's sort of what I observed in my experience And for a lot people this category-theoretic combative theoretic thing is outside their little bubble of interest.

00:30:07: They wanna be able say by higher topos theory poof.

00:30:16: And if they can't find the Heritobus theory, six point two point four point eight They just say well clearly it's in there somewhere and sometimes It isn't.

00:30:26: but The people who go in later?

00:30:28: And sort of try to figure out whether it's their or not and prove it.

00:30:32: If it Isn't There that means somehow its Not as appreciated.

00:30:36: maybe you're a...and the People Who Come In like Us and Say Well Actually There'S A Better Way To Do It Where You don't even need to worry about whether it's there or not because you can.

00:30:45: just It's the sort of thing where you could really just check it yourself.

00:30:49: Or if you do this synthetically, then you'd have to do This.

00:30:52: I mean We come along and say that in.

00:30:55: people Say okay but i already did it.

00:30:57: I used six point two point four point eight And That was good enough for me.

00:31:02: So we now maybe talk About one particular tool at norm switching gears and Turning torsion into a gas Maybe as well Because your both are.

00:31:12: So let's record cubicle types.

00:31:14: for now, we will have a cubical type theory.

00:31:20: What is it?

00:31:20: Cubicle type theory or cubicle hot?

00:31:26: It's an implementation of HOT in a way I would say.

00:31:30: A mic made this nice sort of history right before the book HOT then chemical and now HOTT.

00:31:37: And you maybe wanted to say a bit more about this...

00:31:40: I don't want to say much about cubicle theory but just skip over it, because what i was going to say is that in book hot we sort of write finite definitions like contractability or velocity equivalence.

00:31:59: they generate all the higher structure or even the Martin-Luff definition of identity type is like that.

00:32:07: It's sort a finite definition, it generates all higher structure and I really love about it especially with last bit, that sort of... Martin-luff wrote down this definition of the identity type because he wasn't thinking about homotopy theory.

00:32:20: He was just thinkin' what equality means And somehow Higher topos theory, higher category theory and infinity group ways are implicit in notion of equality.

00:32:29: That one thing i loved most.

00:32:36: No,

00:32:37: go ahead.

00:32:37: I think...

00:32:38: I was just thinking we discussed this already with Steve.

00:32:42: and so the question whether... I mean Martin Lüft didn't formulate this uniqueness of equality proofs or a principle K like some K And we say this was maybe more or less an accident.

00:32:58: I mean, as you just said he wanted to formulate equality and... ...and i think that he had sort of one point in his mind which would be J&K.

00:33:10: for whatever reason He never included K, right?

00:33:15: Which Thomas Streicher observed much later.

00:33:19: So, do you agree that this is maybe more a historical accident or was Martin Luther so clear-voyant?

00:33:26: That he could see these consequences.

00:33:29: Well

00:33:29: I don't know...I'm not inside Martin Luther's head.

00:33:32: No!

00:33:33: Speculation.

00:33:36: But there in a way it certainly an accident but i think i certainly agree as for much far as i knew what he did were intended anything like a homotopy interpretation.

00:33:47: and No, I don't think I've ever read anything that he wrote that suggested that he was considering or aware of the possibility of having multiple proofs of identity.

00:33:58: But uh...I don't know if i would say it's completely an accident but never wrote down K because If you sort-of take a very abstract or I don' t know exactly like a principled viewpoint which is certainly does Then K is unnatural.

00:34:23: If you think about the identity types as generated by reflexivity, and in modern type theories you can write them as a special case of an indexed inductive family.

00:34:33: then the eliminator do get his J?

00:34:36: You don't get k!

00:34:39: So from that perspective

00:34:41: it

00:34:41: may just have been being principled.

00:34:43: Yeah, it's more so syntactic.

00:34:44: The structure of the definition type.

00:34:50: So that what I really liked about is you get all this higher structure from just a simple definition but has various problems like for instance one thing there are lot of things to be able do which can't access.

00:35:03: as far we know you cannot define a simplicial type coherently and talk categories defined in terms of affinity group ways.

00:35:13: And also it's, so the univalence is not computational.

00:35:15: this was a really big push towards other cubicle type theory you can't write to treat as their programming language or your execution gets stuck on Univalence when you write it as an axiom.

00:35:26: and so cubical type theory solved that last problem by destroying the thing I loved about book hot mathematicians way of doing things and sort of just putting in all the higher definitions by hand.

00:35:42: Saying like this is your one-dimensional composition, This Is Your Two Dimensional Composition, And That Sort Of Work To Make It Computational.

00:35:52: But I never liked it because its not what i wanted about The Theory.

00:35:56: Those are sort of two obvious ways dealing with infinity to have some finite thing that generates it then to have explicit definition.

00:36:07: But I would argue that in higher observational type theory, we found the third way of doing it which is to take a co-inductive perspective on infinity.

00:36:16: Which somehow was sort of between these two extremes and allows us write simple finite definition... ...which nevertheless actually includes all the higher stuff.. ..and allow's us to compute with it.

00:36:31: unlike the bookhead version.

00:36:36: We're gonna go on with this, we should probably say to the listeners what co-inductive means.

00:36:39: Yes that's a good idea.

00:36:41: yeah it was cool.

00:36:42: induction

00:36:43: yes

00:36:44: like

00:36:47: so The average mathematician is maybe familiar with induction May at least induction of natural numbers.

00:36:55: So something that's inductively defined Is sort of generated from nothing by applying operations?

00:37:04: starting by zero and by the successor operation.

00:37:07: And when you're programming, you write down a definition of an algebraic data type or something like that.

00:37:16: An element in that datatype is at least in strict language like ML as it's a finite structure built out putting together these constructor operations A ls or tree And then when you have an inductive structure, you can sort of traverse it and do things over it reductively and recursively.

00:37:38: A co-inductive structure or a definition is the opposite where something is defined not by how its built up but what you could with that.

00:37:47: So the classical example of a co-inductive definition which was almost too simple to really give idea list or an infinite stream where you say a stream of natural numbers is defined by saying, well every stream you can pull off the first element which has a number and then take the rest of it.

00:38:08: Which is another stream.

00:38:10: And if that's successively you could pull as many natural numbers out there but never have to deal with completed infinity.

00:38:21: in some sense from a programming perspective, you can one way to think about in co-inductive structure is that it's kind of a lazy data structure.

00:38:32: So like a Haskell programmer list and haskel as potentially an infinite stream where you can pull off elements that are sort being generated lazily But it's sort of an immutable object, maybe.

00:38:52: You can call different methods on that which are basically things you could do with them and some of those method will produce a changed version like pulling off the tail of stream produces another stream.

00:39:06: so in some sense as you apply these methods to But the potential behaviors of an object are infinite, whereas data contained in an algebraic data type is finite.

00:39:19: For my class I always show them co-natural numbers which...

00:39:26: Even simpler than this dream?

00:39:28: Yeah a bit more exotic but it's quite fun i think.

00:39:33: so first off you know the pre-decesary operation on natural numbers or if it's zero, for any other number is a predecessor.

00:39:44: And then I say okay in the co-natural number there something which you have pre-decessor operation and we'll start at that again define this actually quite fun to be fine with mathematical operations of in the mirror images actually not so completely easy those quit quite fun.

00:40:00: And as I said I give some definition of addition.

00:40:09: That sounds like a fun exercise.

00:40:12: So for the listeners, what is a co-natural number?

00:40:16: It turns out that it's either an ordinary natural number or its infinity at least classically speaking.

00:40:25: which infinity constructively.

00:40:33: It's also

00:40:33: interesting maybe to mention the equality of these infinite objects, I mean it is interesting.

00:40:40: and then you get The Principle which actually called Cool Induction right?

00:40:45: Yeah

00:40:46: Yeah, you know people

00:40:47: like that.

00:40:48: People call it that absolutely yeah.

00:40:50: I don't really like calling that co-induction because It seems like a very impoverished thing to give the overall name of Co induction.

00:40:57: i usually call That by simulation or something.

00:41:02: but yeah so Co inductive objects are equal when they have all the same behaviors co-inductively.

00:41:11: So two infinite lists are equal if their first elements are equal and they're tails are equal as infinite lists, yeah?

00:41:17: And so basically that means you can write a program which will sort of traverse the list and is guaranteed to check that these two elements are equals in.

00:41:25: then next two elements or equal on.

00:41:26: so one.

00:41:26: and

00:41:33: Dennis, maybe you can ask some question if it's because your the

00:41:36: yeah I would

00:41:38: know is

00:41:38: may be now skip it to whether even a think this part of conduction.

00:41:42: Is fine but at some point?

00:41:44: I would like to talk about the computer usage as a tool and Particularly on one aspect there or weather It's good to black box it.

00:41:53: so whether This is something we need to produce us ready-to use two mathematicians Or whether this is an impossible dream that we always need too Open up so to speak the program too fully understand what's there when we formalize it, but if that's Too much of a jump We don't need to do it now.

00:42:12: We can do in five minutes.

00:42:14: Yeah, maybe because I interrupted Mike and think you were just trying to explain What this news from infinity and co-induction how does is apply?

00:42:26: To the quality to those group?

00:42:28: Maybe continue with them.

00:42:29: then we go.

00:42:31: Maybe it was this question.

00:42:32: Yeah,

00:42:34: so when I say that in higher observational type theory we treat sort of as infinite group-wide structure co-inductively then the... In a way It's very natural to think about Higher Group-Wide or Higher Category because what is every space or every infinity group wide?

00:42:57: for any two elements, we have a notion of when they're equal and that notion the collection of isomorphisms as another space.

00:43:04: So it's very natural to say oh but by that definition of an infinity group white Is that?

00:43:11: It's a thing with has a bunch of points And then between any two them We Have Another Space Another Infinity Group.

00:43:16: White Of Ways in Which They're Equal isn't a sufficient definition because you have to give the higher operations and coherence, but it's sort of the first step towards seeing why this is co-induction as very natural way to approach this question.

00:43:30: And in one of things that we've done in Hars' rational type theory equivalence really, which was mentioned earlier.

00:43:45: There's this co-inductive notion of equivalent types.

00:43:48: basically we define the universe Of Types By saying where it says elements are types and then to say when two things these things are equal We see that they're equivalent And there is no should have equivalent sort of co inductively says two types are equivalent if there is a relation between them, which that generates all the higher structure because it tells us a little bit technical how it ends up happening.

00:44:50: This relation is dependent on points in A and B, so whenever I have equalities between these relations that can be translated or they get this cubicle box filling.

00:45:06: If you just think about a type being related to itself then auto-equivalence the self equivalents from something do itself.

00:45:15: You say well That's its identity types.

00:45:17: Then transport automatically becomes composition symmetry and all the higher operations of that group.

00:45:25: So just by saying what an equivalence is, basically it says we say two types are equivalent if there's a correspondence between them at also a correspondence thing.

00:45:41: that gets it started.

00:45:42: We have an equivalence here, which is sort of points mapped back and forth And then we have an equivalent at the next level Which then tells us that equality's mapped back-and-forth?

00:45:50: Then in equivalents to the next Level just like a stream we have a consequence Of things now with a sequence of sort of bijections That encapsulates an infinite amount of data.

00:45:59: but In this finite notion of this co induction It allows Us To compute With it because all the infinite stuff Is there But still comes out Naturally, so it still makes me happy to say now I understand like the all this higher structure comes out from finite Understandings of what?

00:46:19: It means for two things to be equivalent basically.

00:46:22: It's a little bit difficult.

00:46:24: Yeah mean that gets a little but technical.

00:46:25: So maybe

00:46:28: yeah may be.

00:46:29: a point here is That's equality or functions as a function the quality of inductive types inductive type uh, co-inductive repetition which is also important.

00:46:43: Yeah that sort of gets into the... even going back to what I was saying earlier We define a type by saying we have points and then between the two points, we have a type of equalities.

00:46:55: And so when you defined something in a co-inductive type You sort of say well like it's uh I have to give It an all of its sort of tails at the same time All of its other behaviors In some single notion.

00:47:07: So if i'm defining say inductive types I'd give all their identity types also.

00:47:11: Those are also instances of Inductive Types.

00:47:15: If im defining Function types, I give there identity types also and those are instances of function type.

00:47:21: Good then it says to come back through your question.

00:47:24: if you don't...

00:47:25: Yeah okay let now focus on how.

00:47:29: this is something that the sole hot movement had going forward like nice computational properties where theorem provers developed for it with it.

00:47:44: your approach, right?

00:47:45: Would you two mind telling a little bit about that work.

00:47:49: How is it going?

00:47:50: how much math have we formalized already as much or not yet?

00:47:58: I had the question to Mike especially because I mean Mike is a mathematician and... And i was quite impressed That he's sitting down and hacking in a proof system!

00:48:11: How did you end up doing

00:48:12: this?!

00:48:15: Create your own proof assistant.

00:48:17: Yeah,

00:48:18: well nobody else would make the one I wanted.

00:48:20: yeah, okay?

00:48:22: I mean II've always been a bit of a programmer on this side.

00:48:25: Okay III did.

00:48:28: some started programming in high school and when I was in college I considered double majoring in computer science.

00:48:35: But I decided to stop because I want it take more math classes.

00:48:38: but I was a volunteer assistant when I was in grad school for summer program and continued sort of being connected to computer stuff.

00:48:49: So, uh... And when i got interested category theory ,I started learning about monads and Haskell and ML things like this.

00:48:58: so it's not completely out-of the blue that without having programmed before instead And I've also had a lot of help from other people in the type theory, homo-wtype theory community.

00:49:11: Uh...I learned a huge amount from Dan Lakata about how to design of type theories and so moving towards implementation and Also from let me like John Sterling and Favonia and Other People that i'm certainly going To forget uh..to mention Give Me A Whole Lot Of Help In Sort Of Building an understanding of the way things are implemented.

00:49:32: But I really wanted a proof assistant that would implement high observational type theory, and for the last decade or more when you want something new implemented in a type theory... The thing is go ask the AGDA developers to implement it at AGDA but they didn't seem interested in implementing higher observational-type theories.

00:49:55: some people have asked me, well why didn't you go and implemented in Agda?

00:49:58: But first of all one answer is that I don't really like Agda.

00:50:03: It's great for many things.

00:50:05: it was...it's really innovative and can do a whole lot amazing thing And i've used myself very happy with what they could.

00:50:11: but as the proof assistant there are things That I want.

00:50:14: that doesn't happen.

00:50:15: I really liked tactics and sort of progressive evaluation Like we had in rock There other sorts words that annoy me about it.

00:50:28: And also, I think it would have taken even more time to understand the internals of Agda well enough than everything in it then actually just sit down and write a new one from scratch.

00:50:38: Also with more fun.

00:50:43: Narya is the new proof assistant that i've been writing for high observational type theory when build the candy shop.

00:50:56: I've always wanted a proper system that does this and now it's sort of like, ah!

00:50:59: i actually have one and i even made it.

00:51:02: so its been a lot fun really.

00:51:04: um...i just only wish had more time to suspend on it.

00:51:07: And where is standing right?

00:51:09: Is there prototype showing that idea works?

00:51:14: Could

00:51:14: i start from here?

00:51:16: Yeah uh..it doesn't quite show how observational type theory work because we haven't quite yet, we haven't quite figured out how to prove that the universe is vibrant sort of or kind of compute compositions and operations in the universe.

00:51:31: In a way they can be implemented but... We have some good ideas and were working on it.

00:51:34: I hope will be there soon But its already A Working Proof Assistant.

00:51:42: It's not as convenient.

00:51:43: use Industrial ones like rock and ag do in lean because it doesn't have implicit arguments And unification of things like that yet.

00:51:53: So you have to fill in all the arguments by hand.

00:51:55: But but it is a full-featured type theory, and it works.

00:51:59: You can use It A lot of higher observational type theories already implemented.

00:52:03: so we Have this sort of experimented with it on some Some basic multiplicative theoretic stuff.

00:52:08: We've checked for instance That we do have Univalence and Univalance computes in a way which it doesn't compute even in cubicle type theory.

00:52:15: It can compute little more strictly, than in cubical-type theory.

00:52:19: So I would say that's pretty convincing proof of concept and we're working towards making it usable.

00:52:28: Yes!

00:52:28: We are going to put the link for people who want to play with it.

00:52:32: But there is very nice documentation on some webpages.

00:52:38: The one thing i find really interesting that you in the same time define not just constructors or elements of a type, but also of equality and equality.

00:52:50: This is already implemented as I find quite beautiful.

00:52:54: if you say successor creates natural numbers... But it turns out successor also create the quality proofs that this is already the sort of co-inductive nature, or this co- inductive explanation.

00:53:11: It's already very natively built into Norea which I think it was really beautiful.

00:53:18: and there are these surprising things a bit like... That the proof of reflexivity of tides turned out to be equality etc.

00:53:26: so they're lots of strange loops which are really fascinating to observe.

00:53:33: I recommend to read this documentation and play around with Maria, despite all these... It's not completely finished.

00:53:45: So there are some back-and-forths?

00:53:47: You learn something about the theory as well by observing for instance that.

00:53:52: or would you say it is just a tiny stone that's curious but has no systematic value for developing the theory.

00:54:02: That didn't make sense

00:54:03: for you?

00:54:04: I've definitely learned a lot by doing the implementation.

00:54:09: I think we're making progress towards like say normalization proof or maybe actually proving that theory is computational and i never would have gotten there without trying to implement it, having something that computes what.

00:54:28: And if we think seven years into the future and one huge grant from whatever, the ERC, the Murray or what ever is there a kind of math that will work likely better here?

00:54:41: Is it taking... That's

00:54:43: good question.

00:54:44: I don't know.

00:54:45: We have to experiment and see what kind of difference it makes.

00:54:49: I feel like cubicle type theory hasn't completely lived up its promise And so recently, I would have felt a little bit uncomfortable saying that publicly.

00:55:01: But even some people who are maybe more authoritative than me like John Sterling and then sort of unhappy with it partly because its very difficult to implement unification in a cubical proof assistant you get all these sort of weird boundary conditions that you have to deal with.

00:55:27: And also I think partly because univalence doesn't compute as nicely as he would like it too, right?

00:55:32: In cubicle type theory computes and if has univalance but is sort of has unvalence.

00:55:37: Because you put in within axiom what they call a glue-type and then just figured out the way To make that axium compute.

00:55:43: But in high observational types theory i think we can argue That even evalances really true by definition.

00:55:49: for a suitable definition of equivalence, equality of types really is decouvelance by definition.

00:55:56: Maybe that's the sort of circular thing to say but I have some hopes it will make working with structures more convenient so we can actually use equality as our notion.

00:56:13: I would really like to have that be the case and not actually pass back-and forth between equivalences, and equalities of types.

00:56:21: The way we do when formalizing book hot even in cubicle type theory.

00:56:24: so In terms what kinds of math will make possible or easier?

00:56:31: Again going back before at the average mathematician maybe this doesn't make much difference but i'd love see doing synthetic homotopy theories like whether it makes something's easy harder.

00:56:43: how the efficiency of computation compares to cubicle type theory.

00:56:47: Narja is not at all tuned to compute efficiently, but when we do try to tune it efficiently?

00:56:52: Is there any faster computing things in cubical type theory or no?

00:56:56: But isn't another point which was important for me as a sub-conceptual simplicity?

00:57:02: so I find that if you're teachers and students then they have to explain them quite hard.

00:57:15: Really, you can only understand it by understanding the cubicle model whereas I find in higher observational type theories there is a more conceptual way to explain these things.

00:57:28: You could also use this cubical explanation but you can also explain them in its own terms.

00:57:34: so-to say what do agree with that?

00:57:37: Yes!

00:57:37: I agree definitely and i hope helpful sort of pedagogically also, that it provides maybe a bridge to formalization and understanding higher homotopies in categories for students.

00:57:55: This is one other thing.

00:57:56: we have already observed this kind.

00:58:00: The people like me came from classical homotopy theory, and we sort of import our intuitions from that.

00:58:08: And learn to do the same sorts things in type-theory.

00:58:10: but then there are other people like Egbert who grew up with type-Theory.

00:58:14: so they learned Homotopy Theory by doing Type-Theorie.

00:58:17: They end up with slightly different intuitions and they're able think about ways of doing things that never would have occurred to us.

00:58:26: I think over time maybe this may sort of transform mathematics more noticeably in the pedagogical way.

00:58:34: Yeah, so I normally just ask whether there's anything else you would love to share.

00:58:40: but maybe Thorsten has a specific question first?

00:58:44: No that's fine

00:58:45: then because we are already at one hour and it is our new target time.

00:58:52: But if you have something, we would like to share some advertisement or whatever.

00:58:57: We have time for that of course.

00:58:59: I think i said everything i wanted to say.

00:59:02: Thank You very much for the invitation.

00:59:03: it was fun.

00:59:05: Yeah thank you all.

00:59:06: I learned a lot and will look into that proof assistant.

00:59:12: I will give my humble feedback as what an up-told outsider can make out of it.

00:59:20: Maybe one thing to say, for people who are looking into Tenarya... It's experimental in a lot ways and that means there is going change And also very open to feedback.

00:59:34: So maybe i'm an outlier here but like talking about syntax I sort of made various choices in designing the syntax of Naia, which are a little bit different than other proof assistants.

00:59:46: And I only want to know what people think about them.

00:59:47: but hardly anybody seems to wanna think about syntax and any sort feedback at all.

00:59:53: please let me know or put comments on GitHub issues Or there's a channel on the homotopy type theory Zulip server For questions and comments some thoughts about.

01:00:05: now you're happy to hear anything that people think.

01:00:10: Then let me say once again, thank you very much for being here and to the audience.

01:00:16: Thank you for listening and feel free to comment where we will try to reply to every single content.

01:00:24: comments.

01:00:24: so far We can do that.

01:00:26: Let's see who is there in a year maybe today?

01:00:29: We will overlook some comments but For now I think it's quite A nice discussion forum great.

01:00:34: So thank you again Mike.

01:00:36: You're welcome And have a great day.