2018

[Oxford Internship] Final Report

My M1 internship report in pdf.

[Oxford Internship] The Category of Event Structures

Beginning of my M1 internship at Oxford University: it’ll have to do with Glynn Winskel’s event structures

2017

[Nottingham Internship] Final Report

My L3 internship report in pdf.

[Nottingham Internship] Brunerie Type Theory, or how to concisely sum up the mess about $𝜔$-groupoids

Let’s have a look at Brunerie Type Theory now!

[Nottingham Internship] Categories with Families: the true face of Type Theory

Categories with Families

Agda basics

[Nottingham Internship] strict $∞$-categories in a nutshell

$𝜔$-groupoids might be easier to grasp from a categorical point of view with $∞$-categories

[Nottingham Internship] weak $𝜔$-groupoids: the DIY way

Handmade partial construction of a weak $𝜔$-groupoid.

[Nottingham Internship] Globular sets and strict $𝜔$-groupoids: welcome to infinity land!

We’re beginning to talk about the crux of the matter: here are weak $𝜔$-groupoids!

[Nottingham Internship] Recursors put to the category theory test

How are we supposed to construct recursors and inductive constructors, generally speaking? And where do they even come from?