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?

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: https://jeslie0.github.io/mathematics/category%20theory/2021/03/06/Canonical-Model-Structure-on-Cat/

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

https://github.com/jeslie0/Univalent-Agda/blob/main/UniAgda/categories/examples/Set.lagda.org

@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