Pinned toot

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 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.

Show thread

@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?

Mathstodon

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