“Abstract The usual notion of propositional equality in intensional type-theory is restrictive. For instance it does not admit functional extensionality or univalence. This poses a severe limitation on both what is _provable_ and the _re-usability_ of proofs. Recent developments have, however, resulted in cubical type theory which permits a constructive proof of these two important notions. The programming language Agda has been extended with capabilities for working in such a cubical setting. This thesis will explore the usefulness of this extension in the context of category theory.The thesis will motivate and explain…”

Price: Free

Link: https://www.meetup.com/MoedegruppeFunktionelleKoebenhavnere/events/255020875/