There's no such thing." How was your path to foundations at homotopy type theory if you-

Well, that's an interesting question.

I mean, uh, I've kind of always been interested in foundations a little bit.

I mean, when I, when I was an undergraduate, I, I took logic courses, and I, I did a summer project on, uh, on logic and, uh, sort of as a, a sideline for, for a little while, I was really interested in non-standard analysis, and I, I have a whole bunch of those books on my shelf.

And, um, and then, uh, and then I went to, to Cambridge for a year and took a category theory class from Eugenia Cheng, and I got sold on that.

And, uh, uh, and then, uh, uh, when I went to, uh, UChicago, uh, I wanted to do category theory, and, like, Peter May was the only person there who I could conceivably work with, so I ended up being a topologist.

Um, and I learned a lot of topology, but I was always sort of interested in this, um, foundational or, or logical direction also.

Mm-hmm