Pinned toot

#introduction 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?

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

#introduction 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?

- Website
- https://jeslie0.github.io/

PhD Student in higher category theory and homotopy type theories.

Joined Oct 2020