Pinned post

Hello mathstodon! I'm a PhD student in Canada, and I am originally from the UK. I'm researching topics related to higher category theory and homotopy type theory, but I generally am interested in foundations of mathematics, topology and algebra.

I was getting tired of the barrage of adverts on Twitter and this seems like a nice alternative. Also, I like that we can use $$\LaTeX$$ here.

What I want to know is: what mathematical objects have you been thinking about recently?

I gave a talk earlier this week on constructing the canonical model structure on $$\mathbf{Cat}$$ and $$\mathbf{Gpd}$$, and now I have finished converting my notes into a blog post. You can read it here, if you are interested: jeslie0.github.io/mathematics/

Excuse the tikzcd diagram sizes, I'm still working on them.

My proof that the (pre)category of sets is univalent was pretty hard to parse. Now, it is written in Literate Agda, so it should hopefully be slightly more understandable! Shame that GitHub doesn't give "agda2" source blocks syntax highlighting like "agda" source blocks...

github.com/jeslie0/Univalent-A

After a week or so of proving technical lemma after technical lemma, I have FINALLY formally proven that the category of sets is a univalent category in Agda. That was a tremendous amount of effort for something which is just a sentence in the HoTT book...

Great start to marking calculus assignments. I thought the area of a circle of radius $$R$$ was $$2 \pi R^2$$ ...

I am definitely going to need a midweek weekend.

What do you do when a student uploads 42 pages for a simple calculus homework?

Remember to get some exercise! Drink water too.

From snow, to 15°C sun. Southern Ontario really can't make its mind up when it comes to weather.

I spent three days working on a problem in Agda. Surely, there is a better way work with path algebra?

Can we all agree that November 1st is too early to be putting Christmas decorations up?

Don't you just love it when the corollary is harder than the theorem?

@Jonoidal ... deduce the existence of Bool which can't be shown to be equal to 0 or 1. This doesn't happen in cubical type theory.

@Jonoidal Cool to know that people at Strathclyde are doing some type theory! Currently, I am trying to come up with a general notion of a model of cubical type theory. It's structure is different to, say, Martin Löf type theories as it deals with an object that isn't actually a type.

If you don't know anything about cubical type theory, one of the selling points is that you can prove the univalence axiom in it, which helps solve canonicity problems. For example, in ordinary HoTT, you can ...

I've really been enjoying using Agda, lately. It was strange to transition from Coq, but I feel there are some benefits to working with proof term directly. I do miss having a step-by-step construction of the proof term though.

Rainy days are wonderful opportunities to do research

Here are the results from a nice little survey asking how many holes certain objects have.coukd the difference between a topologist and a non-mathematician be how many holes they think a straw has?

reddit.com/r/dataisbeautiful/c

Conceptually, I find -2 and 0 homotopy types to be easier to think about than -1 types. In HoTT, this is fine as -1 types are just propositions; however, in Top I think they are just contractible spaces or the empty space. The two worlds *feel* different to me

Hello mathstodon! I'm a PhD student in Canada, and I am originally from the UK. I'm researching topics related to higher category theory and homotopy type theory, but I generally am interested in foundations of mathematics, topology and algebra.

I was getting tired of the barrage of adverts on Twitter and this seems like a nice alternative. Also, I like that we can use $$\LaTeX$$ here.

What I want to know is: what mathematical objects have you been thinking about recently?

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!