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 why propositional equality in cubical Agda is more expressive than in standard Agda. Alternative approaches to Cubical Agda will be presented and their pros and cons will be explained. It will emphasize why it is useful to have a constructive interpretation of univalence. As an example of this two formulations of monads will be presented: Namely monaeds in the monoidal form an monads in the Kleisli form.
Finally the thesis will explain the challenges that a developer will face when working with cubical Agda and give some techniques to overcome these difficulties. It will also try to suggest how future work can help alleviate some of these challenges.
BIO:
Frederik Hanghøj Iversen
Work experience:
2018 | Haskell Developer | Gothenburg University. Maintainer of MULLE
2017 | Teachers Assistant | Chalmers University of Technology
2015 - 2016 | Netcompany A/S | Developer
2013 - 2015 | IT Minds | Developer
2014 - 2015 | Copenhagen University and DTU | Teachers Assistant
Education:
2016 - 2018 | Masters Degree, Computer Science | Chalmers University of Technology
2010 - 2014 | Bachelors Degree, Computer Science | Aarhus University
